EDITORIAL

 

 

Changing Paradigms in Functional Verification

Carl Pixley

                 Synopsys, Inc.

 

Functional verification concerns what a design is supposed to do.  It is not concerned with power, speed, manufacturability and the like. Examples of functional verification include the following.  Does an AMBA interface macro respect the AMBA protocol?  Does a cache protocol preserve cache coherency?  Does a pipelined microprocessor produce the same results as an un-pipelined one? Is a Register Transfer (RT) design model equivalent to a gate-level model?

It is important to remember that when we speak of a ¡°design,¡± we probably mean a model of the design.  Of course, silicon is the ultimate reality of a design ¨C it does what it does.  However, to control the design process, we create numerous models of the design first and then analyze the models with EDA tools. For example, we may start with a transaction level model of the design in, say, the C language.  Then we may somehow derive an RT-model of the design, and then a gate model, a switch model, a Spice model, and finally a layout.  The point is that there are many models that represent various aspects of the ¡°design.¡± Models that are machine-readable can be refined with EDA tools. The kind of verification one needs to do is very dependent upon the kind of model one is dealing with.

All of what I have said so far should be pretty familiar to the reader. The questions are, ¡°What is new?¡± and ¡°What are the trends in functional verification?¡±  My thesis is that there are paradigm changes occurring in our industry.

Paradigm change one: The last few years have seen a rise in Assertion (or Constraint) Based Verification (ABV). There are now several standard languages used to express assertions, with System Verilog Assertions (SVA) and PSL being two examples.  All major EDA vendors support one or both of these languages in their tools.  ABV has become popular because embedding assertions (especially temporal assertions) in a design has enabled a new set of methodologies and tools to be used. For example, one can use assertions as monitors during simulation of the design to immediately flag aberrant behavior, and to localize its cause! Assertions on inputs can also be used to generate constrained random inputs automatically. Several commercial test bench tools have this capability. Assertions can be used with Formal Verification (FV) tools, which are designed to (a) prove an assertion, or (b) show a counterexample trace from a valid initial state.  Assertions can be used to constrain the inputs of the design being verified; that is, assertions define the environment of the design for FV. Assertions can also be used to define coverage, that is, was a sequence of events ever simulated or not? A more subtle benefit of assertions is that, unlike directed (ad hoc) simulations, designers must think about the general properties that are preserved by their designs.  This leads to a whole new way of thinking about designs, one which involves designing to assertions rather than to point-by-point behaviors. Assertions can be organized so that they actually capture all of the intended functional behavior of a block or unit, and thus, sets of assertions can become functional specifications for the design unit. When I worked at Motorola, we organized assertions in this way.

Paradigm change two:  There seems to be another move toward high-level (HL) design. Several semiconductor companies, for example NEC [see K. Wakabayashi and T. Okamoto, C-based SoC Design Flow and EDA Tools: an ASIC and System Vendor Perspective. IEEE TCAD Dec, 2000], seem to be putting serious effort into raising the level of design to at least a transaction level. Several years ago, the conventional wisdom in EDA was that high-level design was all about high-level synthesis. That turned out not to be the case.  However, there are still good reasons for designers to design at a high level (such as, C, C++ or SystemC).  One reason is that it is good to have HL designs to give to customers, so customers can run them, and see whether the designs are doing what is expected.   In addition, they can use HL designs to begin developing software drivers for applications well before silicon is ready. Semiconductor companies can try out new algorithms and architectures to see if they are worth implementing in silicon.  My contention has been that HL design will not really succeed until there is HL-to-RTL (or gate level) verification.  For any design model to be useful, we must guarantee that the resulting silicon will match the model.  HL-to-RTL verification is a link in a long chain connecting the HL model to the silicon. I believe that we will begin to see formal tools being developed and used to compare transaction level designs to RTL. This will just be an extension of the existing trend towards using formal tools to compare RTL designs to gate level design, which is already well established.  However, make no mistake about it, HL-to-RTL is a much more challenging problem than RTL to gate.  [Alfred Koelbl and I wrote paper that will appear in the International Journal of Parallel Programming about how to create efficient formal models for HL programs.] This brings me to paradigm change three.

Recently, I have been greatly impressed by the work at Intel reported by Zyad Hanna, Zurab Khasidashvili, and their colleagues at ICCAD. They described a compositional theory about how to verify the sequential equivalence of two complex designs incrementally.  They used the theory of alignability and, by adding constraints, managed to prove two very large but sequentially different designs equivalent (i.e., alignable). It has long been recognized that sequential optimization would greatly benefit synthesis, for