Design and verification of a multichip coherence protocol

Patent metadata

Field	Value
Publication number	US-2016267209-A1
Application number	US-201615065799-A
Country	US
Kind code	A1
Filing date	Mar 9, 2016
Priority date	Mar 12, 2015
Publication date	Sep 15, 2016
Grant date	—

Abstract

A system includes a formal verification engine running on a host and a protocol checking engine. The formal verification engine automatically generates and formally verifies a reference specification that includes a plurality of extended state tables for an integrated circuit (IC) design protocol of a chip at architectural level. The formal verification engine is further configured to automatically generate a plurality of self-contained services from the plurality of extended state tables. A self-contained service of the plurality of self-contained services is randomly and atomically executable. The self-contained service of the plurality of self-contained services changes responsive to the IC design protocol changing. The protocol checking engine checks and validates completeness and correctness of the self-contained service of the reference specification.

First claim

What is claimed is:

1 . A system comprising:
a formal verification engine running on a host, which in operation, automatically generates and formally verifies a reference specification that includes a plurality of extended state tables for an integrated circuit (IC) design protocol of a chip at architectural level, wherein the formal verification engine is further configured to automatically generate a plurality of self-contained services from the plurality of extended state tables, wherein a self-contained service of the plurality of self-contained services is randomly and atomically executable, and wherein the self-contained service of the plurality of self-contained services changes responsive to the IC design protocol changing; and a protocol checking engine running on a host, which in operation, checks and validates completeness and correctness of the self-contained service of the reference specification.

2 . The system of claim 1 , wherein the reference specification further includes a list of valid non-transient states.

3 . The system of claim 2 , wherein a coherent interconnect is within a valid non-transient state of the list of valid non-transient states.

4 . The system of claim 2 , wherein the protocol checking engine is configured to select a valid non-transient state from the list of valid non-transient states as a starting state for the check and validation of completeness and correctness of the self-contained service of the reference specification.

5 . The system of claim 1 , wherein the IC design protocol is a directory-based multichip coherence interconnect (OCI) protocol.

6 . The system of claim 5 , wherein the plurality of self-contained services is a model associated with the coherence protocol, and wherein the model is parameterized based on addressees, nodes, and channel depths.

7 . The system of claim 1 further comprising:
a micro architect engine running on a host, which in operation, implements the IC design protocol at the micro-architectural level using a synthesizable package generated from the formally verified reference specification; and
a dynamic verification (DV) engine running on a host, which in operation, dynamically verifies the implementation of the IC design protocol at the micro-architectural level and incorporates all incremental changes to the IC design protocol in real time based on a DV reference model generated from the extended state tables of the reference specification,
and wherein the micro architect engine and the DV engine are configured to operate responsive to a determination that the self-contained service of the reference specification is complete and correct.

8 . The system of claim 7 , wherein:
the synthesizable package captures behaviors, functions, and interactions among gates and transistors within each components in the reference specification at the architectural level.

9 . The system of claim 7 , wherein:
the synthesizable package includes state transitions at the micro-architectural level for resistor-transistor level (RTL) implementation of the chip using the same underlying protocol representation in the reference specification used for formal verification to reduce chances of introduction of new errors during the RTL implementation.

10 . The system of claim 7 , wherein:
the micro architect engine enforces a plurality of implementation constraints at the micro architect level to ensure no assumption of the protocol is violated.

11 . The system of claim 10 , wherein:
the formal verification engine incorporates micro architect level implementation details into the plurality of extended state tables of the reference specification to reflect the implementation constraints at the micro architect level.

12 . The system of claim 7 , wherein:
the IC design protocol includes the reference specification used for formal verification of the protocol at the architectural level and the synthesizable package used for implementation of the protocol at the micro-architectural level.

13 . The system of claim 1 , wherein:
each extended state table of the plurality of extended state tables of the reference specification is in parsable ASCII format without having any hidden states, assumptions, redundancy, or dead-ends.

14 . The system of claim 1 , wherein:
the IC design protocol is a directory-based cache coherence protocol, which connects a plurality of System-on-Chips (SOCs) as a single multicore processor via connections among the SOCs.

15 . The system of claim 14 , wherein:
each connection under the cache coherence protocol implements a plurality types of virtual channels for cache coherent memory traffic among the SOCs of the chip.

16 . The system of claim 1 , wherein:
the formal verification engine automatically incorporates and validates incremental changes to the protocol to support maintainability of the protocol.

17 . The system of claim 16 , wherein:
the formal verification engine manages the protocol in a programmable way and provides a uniform consistent output of the reference specification for the incremental changes to the protocol.

18 . The system of claim 1 , wherein:
the protocol checking engine checks the reference specification for one or more of under-specification, over-specification, and missing or hidden assumptions in the specification.

19 . The system of claim 1 , wherein:
the protocol checking engine checks the reference specification for one or more of deadlocks, cache coherence, and data consistency.

20 . A computer-implemented method, the method comprising:
automatically generating and formally verifying a reference specification that includes a plurality of extended state tables for an integrated circuit (IC) design protocol of a chip at architectural level via a processor; automatically generating a plurality of self-contained services from the plurality of extended state tables, wherein a self-contained service of the plurality of self-contained services is randomly and atomically executable, and wherein the self-contained service of the plurality of self-contained services changes responsive to the IC design protocol changing; and checking and validating completeness and correctness of the self-contained service of the reference specification.

21 . The computer-implemented method of claim 20 , wherein the method further comprises:
providing a list of valid non-transient states.

22 . The computer-implemented method of claim 21 , wherein a coherent interconnect is within a valid non-transient state of the list of valid non-transient states.

23 . The computer-implemented method of claim 21 , wherein the method further comprises:
randomly selecting a valid non-transient state from the list of valid non-transient states as a starting state for the check and validation of completeness and correctness of the self-contained service of the reference specification.

24 . The computer-implemented method of claim 20 , wherein the IC design protocol is a directory-based multichip coherence interconnect (OCI) protocol for communication requests among a plurality of System-on-Chips (SOCs) of the chip.

25 . The computer-implemented method of claim 24 , wherein the plurality of self-contained services is a model associated with the coherence protocol, and wherein the model is parameterized based on addressees, nodes, and channel depths.

26 . The co

Assignees

• Cavium Inc

Inventors

• Ikram Shahid
• Akkawi Isam
• Kessler Richard Eugene
• Ellis James
• Asher David

Classifications

• G06F12/0817

  using directory methods · CPC title

• G06F30/30 Primary

  Circuit design · CPC title

• G06F2212/622

  State-only directory, i.e. not recording identity of sharing or owning nodes · CPC title

• G06F17/5045 Primary

  Physics · mapped topic