IP Verification : Method backs block-to-SoC verification

Over the past five years, Motorola's engineers have developed a methodology and the supporting tools that accomplish those tasks. The methodology and tools are centered on the CBV (clock-based verification) formal property language but could potentially be implemented by other formal property languages.

Our approach begins with the recording of assumptions-typically by the designer-about a unit's environment in the form of logic constraints. With traditional unit verification, those assumptions are built into the testben ch and possibly documented in code comments.

A Motorola internal tool, Stimulus Engine, then uses formal verification techniques to analyze the constraints and generate legal random stimulus. Input probability weightings can be used to bias the stimulus generation within the range permitted by the constraints. Beginning with just a few constraints, the designer is able to generate a stimulus, "animate" the design and view the output with a waveform viewer of the designer's choice.

Predicting behavior
The first input sequences may include illegal sequences until the designer iteratively refines the constraints into a set that accurately describes the unit's full legal environment. In practice, the ability to animate the design quickly from just a few constraints has been very popular among design and verification engineers.

As the constraints become more mature, the designer begins writing CBV properties (specifications) describing the unit's expected behavior. The proper ties described can vary from protocol checks on an interface up to a complete behavioral model of the unit. Like constraints, properties are developed incrementally.

New properties and edits to existing properties can be tested against an existing constrained-random simulation output trace until the desired outcome of the property checking is observed. The constraints and properties can then be used to generate and check new simulation traces.

Once the constraints and specifications are producing the desired type of stimulus and behavior checking, respectively, attention is shifted to functional coverage, expressed in terms of exercised properties. Input probability weightings are then adjusted to steer the constrained-random stimulus toward the unexercised properties. Temporary constraints are sometimes created to focus on specific operating modes.

The property language and functional coverage mechanism are convenient enough that some groups use it extensively just to monitor for events corresponding to items in their verification plan. When constrained-random simulation is no longer discovering new bugs, the same constraints and properties can be used by formal verification tools to model check the properties. Model checking statically analyzes the design and returns the result of:

• Property is always true.
• Property is false and an error trace is provided.
• The portion of the design needed to analyze the property is too large for the tool's capacity.

Bounded model checking can work with much larger designs. It is primarily used to search for property violations (bugs) within a specified number of clock cycles, rather than for proving correctness. Even without running formal verification, the act of writing explicit, mathematically precise constraints and specifications uncovers ambiguities and, often, errors in both the design and its documentation.

When the unit is integrated into an SoC, the specs go with it and can be used for checking during simulations. They also provide a form of functional coverage that can more meaningfully reflect the interblock communication in an SoC.

While traditional unit testbenches are discarded after unit verification, unit constraints can be reused as monitors for the integration without modification. The assumptions at the unit level are monitored for violations at the integration level. The constraints and specifications can also be used for formal verification in the integration, but capacity often limits their use to that of simulation monitors.

Familiar environment
One of the keys to this methodology is the use of constraints: They enable effective hierarchical verification and are reusable from unit to SoC level. The use of constraints for both stimulus generation and integration monitoring, without modification, appears to be unique in the industry.

Also, designers, not specialists, are doing formal property checking on their designs. The CBV language uses a syntax similar to Verilog's that designers pick up quickly. Since the constraints and specs are developed in the familiar context of simulation, the transition to formal verification is more understood and automated.