Assertion-based verification streamlines design outsourcing

Assertions provide a clear, concise way to document and clarify design specifications, assumptions, and decisions. They also detect any discrepancies between you and the outsourcing team when they are simulated or formally verified.

Your team catches many bugs by simulating the module in the context of the larger chip. Outsourced design is usually done out of context. This forces the contractor to test against the interface specif ication - amplifying the importance of clarity and accuracy in that specification. Thorough interface testing requires validating response to input stimulus - correct and incorrect. ABV supports formal verification and meaningful metrics to ensure that a component design can successfully be verified separately from the design in which it will be used, reducing the number of issues found during integration.

At the end of the project, contract staff is often reassigned to other projects, possibly for other companies. The original designer may be unavailable later to perform design maintenance or to develop derivatives designs for you. Assertions document the design in an executable way so that you and others can understand the design, properly modify it, and thoroughly verify design changes.

The sections below highlight a number of practices using ABV to make outsourcing more efficient and successful.

Clarify interfaces, document features
Assertions enable you to clearly and concisely specify interfaces for outsourced design components. The interface specification forms a contract between your company and the contractor. Changes to the specification increase effort, time, and the possibility that a bug can sneak through if all parties do not properly implement the change.

Using assertions to specify interfaces is far superior to natural language and waveforms because assertions are unambiguous and executable. The clarity of assertions comes from having well-defined syntax and semantics. Any uncertainty about what an interface checker means can easily be resolved by looking at the reference manual.

Assertion languages enable you to clearly specify any interface, but often require significant coding to describe complex interfaces and RTL components. Using a library of predefined templates for common inter-block communications not only speeds specification, it also clarifies communication by acting as a shorthand notation. For example, when designers see a data-ready or request-ack nowledge handshake assertion on a port, they quickly know what is required. This increased clarity is especially valuable as interfaces get more complex and include multiple clock domain synchronization, data buffering, queuing, and arbitration.

Figure 1 provides an example of an interface documented with four assertions from the 0-In Design Automation CheckerWare Library. The contractor is able to refer to the CheckerWare documentation for more details on the requirements.

Figure 1 - Assertions document interface

Assertion-based interface specification can also be used to constrain pseudo-random simulation and formal analysis. This ensures that the circuit will work properly under all legal input stimuli, and characterizes behavior in the presence of illegal input sequences.

For industry standard protocols, you can easily specify an assertion protocol monitor to back up the requirement that an interface on an outsourced module meets the specification. Using the same monitor as you will use in-house further ensures that the outsourced module will work properly with your design tools and modules developed in-house. These assertion protocol monitors can be developed in-house and given to the contractor as part of the specification, or can be purchased from third party sources. Third party monitors save development time and have the advantage of providing yet another independent interpretation of the protocol specification.

The biggest advantage of assertions is that they become a part of the design. Modern assertion methods enable you to specify assertions and monitors inline with the HDL code for the module. Placing assertions inline is key because inline assertions cannot get lost. The correctness of the interface can then be verified in simulation, formal verification, and with other tools.

All tools that work on the HDL module will see these assertions and chec k to make sure they are obeyed. Anyone reading the HDL code benefits from the documentation provided by the inline assertions. This benefits both the contractor designing a component and other design teams designing circuitry around the outsourced module.

Assertions are also invaluable when it is necessary to change an interface specification. Not only does the assertion document these interface changes for the design teams, but the changes automatically propagate to the design and verification environment where they get checked in simulation and formal verification.

During design, assertions enable the contractor to document key RTL structures easily, design assumptions, and implementation corner cases in an executable form. This documentation enables you to understand the design architecture and have confidence both in the design quality and in your ability to integrate and maintain it.

Mandating that key RTL structures such as register files, FIFOs, and arbiters are identified and documente d with RTL checkers is highly efficient. These high-level checkers typically translate to multiple assertions and represent the most meaningful way to instrument and document the design with assertions. In addition, all design assumptions (such as one hot state encoding) and design corner cases (such as max value) should be documented with assertions. These assertions help you understand the RTL code you get back much better than English comments or custom checking logic, and can be constantly monitored during verification. Finally, RTL assertions often include coverage metrics and statistics that help measure test coverage.

For example, Figure 2 shows that adding four lines can document key RTL components in a module. In addition to documentation efficiency, these four lines specify over 20 assertion checkers and more than 10 structural coverage points.

Figure 2 - Documenting RTL components

To ensure p roper instrumentation, you can specify an assertion density metric that the contractor must meet. 0-In has found that one RTL checker for every 1,000 gates is usually sufficient. If low-level assertions are used (such as state transition checks, or "known driven"), you'll need a higher density of assertions to attain adequate assertion density. This further highlights the importance of using high-level, high-value checkers.

Formal verification stress test interfaces
Simulation alone misses bugs because relatively few input sequences are tested. If you make formal verification a contract requirement, you'll know the design will work for the full range of legal input values and sequences. The assertions specified on the inputs of a design serve to define all legal input sequences, and hence specify the constraints for formal analysis. Assertions on the outputs of the module act as targets for formal analysis and are used to ensure that the module will not generate any illegal output sequences.

Formal verification also enables "bad model" testing. Applying formal verification with input constraints removed confirms that bad input will not cause issues. For example, bad model testing confirms that a component on a bus will behave properly if there is bad traffic on the bus.

Formal property checking also can be used to catch many simple circuit properties. Many ABV tools offer "lint-like" automated assertion checks so the RTL meets your design standards, and safe design practices such as synchronization rules for signals crossing clock domains. Such capabilities help validate the design and let you easily confirm that the contractor adheres to your recommended design practices.

Metrics improve efficiency
Assertions detect bugs locally in simulation, finding bugs that are not propagated for checking in the test bench. Further, ABV users have repeatedly reported that they find as many bugs just by writing assertions as they find by simulating and formally verifying these assert ions. The rigorous process of writing the assertion often leads designers to see that the implementation does not properly cover the corner case behaviors. (This benefit applies equally whether the design is done in-house or outsourced.)

ABV metrics help your contractor identify sections of the design and specific corner cases that have not been tested. This provides focus for writing additional tests and reduces the number of redundant tests that waste both development effort and simulation time.

ABV metrics let you confirm that the contractor has properly verified the design and increase your confidence that the design will work properly. These metrics let you determine that there are sufficient assertions specified (assertion density) and that each assertion has been adequately tested (structural coverage). Finally, each ABV metric highlights where the design has been verified formally and where only simulation has been used.

Figure 3 demonstrates the effectiveness of ABV metrics. The structur al coverage report shows that the arbiter in this module has not been completely tested because none of the 304 requests has been asserted on channel 'b.' Such reports let you know the level of testing more effectively than line coverage metrics. These metrics also help the contractor by highlighting where additional tests are needed.

Figure 3 - Structural coverage report

Simplify integration and design maintenance
Assertions become part of the design, not the test harness. They continue to be active and detect bugs during full chip simulation and verification. When an externally developed design is properly instrumented with assertions, verifying its integration and operation as part of the full system is significantly simplified.

Assertions on the interface of the block continue to check behavior during and after integration and will rapidly identify any remaining errors. This will highlight when other circuitry does not obey a specified interface, and helps to localize bug detection to the module or to the circuitry surrounding the module. In addition, you can formally verify the module interface in context, which helps diagnose issues that arise from incomplete or incorrect interface specification.

High-level assertions that document major features of the RTL structure help you understand the implementation, analyze issues, and resolve issues more quickly and correctly. During integration, understanding the design implementation is necessary to debug issues and modify the design (if required). Equally, it helps the contractor work with you to resolve issues or specification changes that arise after the design is delivered.

One of the risks you face with outsourcing is that you don't directly control the design resources. These resources may be reassigned or leave the contractor's employ. Assertions are great documentation: they are concise and unambiguous. When you mandate the adequat e use of assertions, issues can be resolved and derivative designs can be created even if the original designer is no longer available.

Summary
Assertion-based verification delivers effective and thorough design verification. For design outsourcing, ABV clarifies design specification and documentation and provides metrics to confirm that the design has been fully verified. Demanding ABV helps you manage the outsourcing process, ensuring that the design meets your specification, and will work as a component in your system.

Emil Girczyc is president and CEO of 0-In Design Automation, Inc.