An Interface-Oriented H/W Specification and Verification Method


The complexity of digital hardware systems and the consistent pressure to shorten the time-to-market period of a design leads to increasing reuse of existing blocks. These so-called Intellectual Property Blocks (IPB) may come from various sources. To verify systems designed using IPB, it is desirable that the blocks be described by behavioral models to hide and protect the implementation (structure) of the block, and to permit system-level verification that could be too costly at a low level of abstraction. Yet, the description must preserve correct interface behavior, synchronous (clock true) or even asynchronous (in terms of actual delays), to allow the verification of correct interactions between blocks.

Over the last 6 years and with the help of Nortel Ltd., we developed such a modeling and verification methodology - Hierarchical Annotated Action Diagrams (HAAD). The elementary objects resemble classical timing diagrams, however, they can be hierarchically composed to form more complex behaviors using parallel, sequential, choice, loop, and exception operators. While this structure describes well timing and protocol of the interface interactions, we can also add annotation of signal events (transitions) by VHDL variables and procedures to introduce function to the model.

System verification can proceed by simulation, in which case we automatically produce a behavioral VHDL model corresponding to the HAAD specification (it can be instantiated in another model). Or, we can statically verify (without simulation) on finite segments of the timing diagrams (partially unrolling the HAAD hierarchy) whether the timing and protocol part is well-formed (causal), and if two or more components of which we know only the interface specifications will correctly interact when interconnected. This static verification is efficiently carried out using algorithms employing Relational Interval Arithmetic, as implemented in CLP (BNR) Prolog from Nortel (a commercial version is distributed by ALS Inc., Cambridge, MA).

In the talk we shall illustrate HAAD on a simple example, and then concentrate on the static interface verification using CLP.


The transparencies in Postscript format

©2002-2018 U.C. Regents