When designing a system-on-chip (SoC) using a platform FPGA for mobile, wireless, networking, or media applications, designers typically integrate many IP components within a short period of time. By offering advanced Xilinx® MicroBlaze™ and onchip PowerPC™ processors, platform FPGAs such as the Virtex™-II Pro and Virtex-4 families give you a head start on integrating processor IP.

Regardless of your IP choice, market requirements are driving the need for more features, such that processor-based platform designs are becoming more complex – incorporating multiple processor cores and multi-layered bus architectures. This spiraling increase in complexity drives the need for new approaches to platform FPGA design and verification. The simple, push-button flow of synthesis logic mapping, with verification as an afterthought, just doesn’t cut it.

Just as design flows for platform FPGAs have come to more closely resemble those adopted by ASIC SoC designers – where synthesis is closely linked to verification at every step – so too have FPGA developers begun to see the benefits of leveraging the convergent synthesis and verification strategies developed for complex ASIC SoCs.

Assertion-based verification (ABV) has emerged as a major player within this convergent design and verification flow. Assertions have been used successfully for more than a decade in microprocessor design. But only recently has their full potential been realized. The payoff is big for large, complex designs, including platform- based designs that contain a growing amount of third-party and in-house IP. As FPGAs approach the complexity and size of larger ASICs, assertions have become particularly useful to FPGA designers.

With the goal of examining the value of ABV within a convergent flow that encourages early discovery of design deficiencies (hereafter referred to as defects), we’ll recommended a few strategies for successful design closure and explore ABV at greater length.

Essential Strategies for Success
Defect discovery must be consciously pursued earlier in the design cycle, where the overall pain and cost of fixing errors is much less. Here are some recommended best practices for accelerating design closure:

• Do more timing and performance analysis up-front. Are you willing to wait until after your design is functionally verified, synthesized, and placed and routed to find out whether your chosen arbitration scheme can keep up with incoming traffic? Early discovery of throughput issues requires more indepth analysis of performance and timing issues throughout the synthesis process. Before burning cycles trying to meet timing constraints in place and route, you must ensure that constraints are complete. Early discovery of timing issues also requires constraint coverage analysis during synthesis.
• Use interactive synthesis techniques for greater predictability. An indispensable weapon in your FPGA design toolkit is a capable, interactive synthesis and analysis environment that goes from RTL to physical implementation. Interactive synthesis techniques allow you to perform “what-if ” explorations earlier in the design cycle. A robust synthesis environment also provides several design representations such as high-level operators and architecturespecific technology cells. Interactive synthesis capabilities give you an earlier understanding of the nature of the design and indicate whether it will meet specifications.
• Check HDL code early and often. Today’s design-management tools assist in checking code against an established set of agreed-upon (by the design team or silicon vendor) coding style rules. Before burning simulation cycles, you can use these coding style rule checkers to catch actual defects and flag potential defects, thus bringing defect discovery up-front in the design cycle.
• Implement a more effective functional verification strategy. Synthesis tools for platform FPGAs do more than simply generate a technology-mapped netlist. Best-of-breed synthesis tools contain important analysis capabilities that provide more insight into your design at every stage in the cycle. These capabilities can identify potential problem areas, such as clock domain crossing points, where you need to handle functional verification delicately. Moreover, when applying a traditional functional verification approach (using VHDL or Verilog test benches) to platform FPGAs, modeling random or pseudorandom stimuli and checking circuit response against designer intent becomes increasingly tedious. This is where ABV can play a significant role.

Because ABV creates an unlimited number of observation points (assertions) throughout the design, it speeds debugging by identifying errors close to or at their source. Assertions also identify problems that do not propagate to a primary output; thus ABV improves design quality by exposing bugs that might otherwise go undetected.

Assertions provide a set of properties as targets for FMC. They also enable simulation test vectors to be used by dynamic formal verification (which we will explain later) to find potential violations of a module’s assertions.

The basic ABV methodology compares the implementation of a design against its specified assertions. Therefore, the quality and comprehensiveness of a design’s assertions are critical. These assertions originate from the following sources:

• Using proprietary or standard assertion languages, such as SystemVerilog Assertions (SVA) and the Property Specification Language (PSL), design engineers can write assertions as you implement various structures. They may sometimes make an inadvertent mistake in their implementations; assertions provide critical cross-checks between intended and actual behaviors. For example, suppose the intended maximum value of a pointer is 48. An assertion might detect that a coding mistake exists that allows the pointer to go beyond 48 in otherwise legal situations.
• Verification engineers can write assertions from a specification of the design, a design document, or from their personal understanding of the design. Normally these assertions address concerns at a high level and cover critical behaviors of the design. For example, suppose a particular DMA controller has a channel configured to do 10 memory transfers. Before the channel is de-allocated, the total number of transfers must be exactly 10, or a serious problem will occur. The verification engineer can add an assertion to check for such an event.
• Both design and verification engineers insert protocol assertion monitors to check for violations of the corresponding interface protocols. These monitors ensure that transactions between components are properly generated and handled correctly. EDA vendors have developed off-the-shelf protocol assertion monitors for common standard interfaces (such as Mentor Graphics CheckerWare protocol monitors). These monitors come with all of their protocols’ rules encapsulated, and are kept up-to-date to account for protocol standards revisions. Used with simulation, protocol assertion monitors collect useful statistical information. For formal verification, they act as constraints.
• Some verification tools insert assertions into the design by analyzing the RTL source-code structure. Solutions for many common design problems provide the basis for this analysis, allowing automation of the instrumentation process. Many problems are discovered statically, either by the tool itself (using netlist analysis) or with formal analysis. Other problems are detected only with dynamic verification methods, such as functional simulation or dynamic formal verification. Examples of problems analyzed by automatic assertion insertion include synthesis-to-simulation mismatch problems, unreachable code or FSM states, clock domain crossing (CDC) errors, X-semantic problems, and CDC clock jitter.

Simulation-Based Verification with Assertions
During functional simulation, a design’s assertions monitor activities both inside the design and on its interfaces (Figure 1). Assertion violations are reported immediately; the problem need not propagate to the design’s output ports to be detected by the test bench. This high observability simplifies bug triage and increases the understanding of potential causes of discovered problems.

Formal Model Checking with Assertions FMC is a complementary technology to simulation and an integral part of an ABV methodology. FMC uses mathematical techniques to prove some assertions true (given a set of assumptions provided by the assertion library) and other assertions false (by discovering counterexamples). A proof means that FMC has explored all possible behavior with respect to the assertion and has determined it cannot be violated. A counterexample shows the circumstances under which the assertion is not satisfied. FMC examines all possible states of a design to determine if any of them violate a specified set of properties.

Dynamic formal verification, a new FMC technique pioneered by the 0-In business unit of Mentor Graphics, overcomes the memory and computational limitations of static formal verification by amplifying a given simulation trace. This enhances ABV by enabling FMC at both the sub-block and chip levels, using static and dynamic formal techniques, respectively (Figure 2).

Given a set of target behaviors, expressed as assertions or coverage points, dynamic formal verification uses formal analysis of “interesting states” along the simulation trace to determine if it is possible to reach any of the coverage points or violate any assertion. For functional verification, an “interesting state” is one where a new or rare design behavior has occurred.

Consider a bug that occurs many cycles deep into a simulation. This particular bug might occur only if a particular FIFO in the design is full and a particular FSM is in state FOO. With simulation, it is possible that a test will manage to fill up the FIFO, while the same or another test can also get the FSM into state FOO. To get exactly the right combination of random stimuli for both events to occur may be a low-probability event.

With dynamic formal verification, from a simulation state where the FIFO is full, formal analysis examines all possible states leading up to and beyond that point in time, identifying and reporting the particular sequence that leads to the state that manifests the bug. Thus, dynamic formal verification coupled with constrained random stimuli uncovers a bug that would have otherwise required additional test bench code to detect.

Without dynamic formal verification, you would have to know that a potential bug is lurking and modify the stimulus constraints in an attempt to guide the test to the right set of states. In actuality, dynamic formal verification can amplify any single scenario into 10,000 or more effective tests. With this in mind, the actual set of constraints for the test bench can be much simpler because the constraints do not need to accommodate the fine-grained tweaking discussed above, saving the substantial time it takes to conceive and code such elaborate constraint environments.

Interface Protocol Monitors
Interface protocol monitors allow devices in platform-based designs to be isolated and verified. In any good processor-based design, every component must communicate correctly with the available interfaces. Protocol monitors check for violations of the corresponding interfaces at the block or chip level.

A protocol monitor includes assertions to enforce the protocol rules. It ensures that transactions between components are properly generated and handled correctly. During simulation or formal verification, incorrect protocol transactions will be identified at the source.

For hardware-related issues, an ABV methodology using the CheckerWare assertion library can improve defect discovery in processor-based platform FPGA designs. Besides checking for violations during simulation, CheckerWare protocol monitors collect functional coverage and statistical information and act as constraints for formal functional verification. Monitors affirm the transactions performed, highlight “holes” in the regression suite, and audit the quality of pseudo-random stimulus generation environments.

Hard-to-Verify Structures
As processor-based designs become more complex, components become buried so deeply in designs that it is difficult to control and test them effectively. For example, in any multi-layered bus architecture, multiple masters can talk to multiple slaves concurrently. This capability increases overall system bandwidth, but it also increases verification complexity.

To tackle these hard-to-verify structures, you can capture design intent with assertions and checkers and embed them in the RTL code. The embedded assertions automatically check for incorrect behavior resulting from errors in the RTL code itself, catching design problems locally without manual intervention by the designer or verification engineer.

Embedded assertions also allow you to locate the source of problems faster. In a traditional verification flow, errors detected during simulation are time-consuming to trace to the originating problem because there are many possible causes for each failure symptom. For instance, if multiple DMA channels are set up to transfer data from several interfaces to memory, you may detect an error in the memory data at the end of the test, but it is difficult to track down the exact transaction that produced the data error. Using assertions, you can quickly identify the exact time of the data corruption and the hardware resources involved with the problem.

Conclusion
The higher capacity and complexity of modern platform FPGAs has opened up unprecedented opportunities for companies, but it has also created increasingly tough challenges for designers. Adopting – and adapting to – strategies that leverage a convergent design, synthesis, and verification flow for earlier defect discovery can prove beneficial for FPGA engineering teams in terms of reduced iterations and faster design closure.

ABV accelerates debugging by finding and fixing bugs early, at or near their source, and improves design quality while reducing development costs by discovering errors that would otherwise go undetected until after tape-out.

For more information on advanced verification methodologies from Mentor Graphics, visit www.mentor.com/fv.

Printable PDF version of this article with graphics.  (12/1/05) 425 KB