daptive functional verification, a technology developed by startup @HDL in its @Verifier tool, was created to facilitate the melding of model checking into existing flows. The technology has been tested by Amber Networks, a communications company designing multimillion-gate ASICs.

Adaptive functional verification (AFV) detects the toughest bugs by providing a hybrid solution that automatically combines the benefits of static model checking and dynamic simulation techniques. It overcomes the limitations of current model-checking tools and eases integration into the mainstream verification flow in a number of ways.

One of the classic model-checking problems is state-space explosion. The state of any system is defined as the set of values on all the nodes (registers) in the system. A transition is defined as a change from one state to another and is a function of the current state and legal values of the input variables. As the number of registers in the system grows, the potential number of such transitions, or state space, grows exponentially, thus causing what is known as state-space explosion, which makes further computations very difficult and slow.

AFV uses several new algorithms to reduce the state space and allow model checking for intellectual-property (IP) blocks. Based on design analysis, AFV algorithms trim the logic to leave only the portion of the design that is relevant to the particular property being verified. The algorithms identify the cones of logic relevant to the variables affected by the properties. Further, the algorithms eliminate data-path elements from the logic and perform iterative logic reduction through stages of flip-flops until a property can be proved.

Even with more efficient logic-reduction techniques, AFV model-checking algorithms eventually run into the state-space-explosion problem for very large IP blocks. While the user may have spent considerable effort creating properties and constraints to augment the automatically created properties, all of that effort would be wasted if the model checking algorithms were unable to verify the property.

To validate properties that run into state-space explosion and reach a user-specified time-out for model checking, AFV automatically switches to intelligent-random Verilog simulation. AFV algorithms automatically create intelligent-random vectors and Verilog simulation testbenches that drive the logic through as many coverage steps as possible to make the given property fail. This hybrid approach-driving both static and dynamic verification using the same user-generated or automatically derived properties or both-overcomes a serious model-checking limitation and minimizes the risk of using model checking in existing functional verification flows.

A better method would be to apply the clock and reset appropriately, followed by the load signal and then holding load and reset low for n cycles. Random data should be applied only to the ParallelIn and SerialIn signals to guarantee optimum verification coverage. AFV extracts many such constraints from the design by analyzing objects such as finite-state machines (FSMs) and FIFOs. It then merges those constraints with the user-specified constraints on the inputs and generates the intelligent-random vectors.

Traditional model-checking tools rely on complex mathematical specification languages or proprietary assertion languages, adding the burden of learning yet another language on design engineers. While debugging the results of model checking, especially at the block level, a clear need emerges for specifying constraints at the inputs.

Consider the example of a decimal counter, shown in the accompanying figure. A simple property for the counter specifies that the count will always be between 0 and 9. However, this property would fail if the value driven from the "loadVal" input port is greater than 9. Thus, this input port needs to be constrained as further shown in the listing.

AFV features a unified language that allows the user to write properties and constraints in Verilog with a few PLI extensions ($calls). This helps designers make the migration from writing vectors to writing properties much smoother. This language can also be used to convert constraints to properties and assertions for the next level of hierarchy.

The constraint on loadVal in the listing can easily be converted to an assertion on the signal-driving loadVal. Such a simple property language can also be used widely in the system for various tasks such as specifying transactions and bus protocols, generating timing diagrams and creating assertions for higher-level system simulation languages.

The team used AFV on a complex logic block with six FSMs that were all interacting through a semaphore. Using AFV with no user intervention and effort, the automatic property-extraction technology created 27 complex properties to verify deadlocks among the six FSMs in Amber Network's design.

When the team ran model checking with those 27 properties, eight properties failed. The waveforms resulting from the failed properties were analyzed, and two of the failures were attributed to input changes that were not possible and were fixed by applying appropriate constraints to the inputs. The remaining six failures were caused by a genuine bug in the design that was not detected by simulation. If left undetected, this bug would not have been found until the silicon was produced.