Global Sources
EE Times-Asia
Stay in touch with EE Times Asia
EE Times-Asia > EDA/IP

Use system models for better verification

Posted: 02 Jun 2008 ?? ?Print Version ?Bookmark and Share

Keywords:functional verification? improve debugging efficiency? sequential logic equivalence checking?

RTL verification remains the bottleneck in digital hardware design. Industry surveys show that functional verification accounts for 70 percent of the total design effort. Yet, despite the emphasis on verification, more than 60 percent of all design tape-outs require a respin. The predominant cause is logic or functional flaws, defects that could have been caught by functional verification. Clearly, improved verification techniques are needed.

Design teams commonly use system models for verification. System models have advantages over RTL for verification: namely, ease of development and runtime performance. The challenge is bridging the gap between system-level verification and creating functionally correct RTL. A methodology known as sequential logic equivalence checking has the ability to bridge this gap by formally verifying RTL implementations against a specification written in C/C++ or SystemC.

This article describes the system-level to RTL design and verification flow of a commercial graphics processing chip. In this flow, system models were developed to validate the arithmetic computation of video instructions and were then used to verify the RTL implementation using sequential logic equivalence checking.

Using C/C++, SystemC
The design complexity associated with functional partitioning, block interfaces and hardware/software co-design expands exponentially, making system verification mandatory. Today, C/C++ and SystemC are used commonly for system-level design and verification.

For this project, C/C++ was used to model the video processing arithmetic block. Once the system model was refined and verified, RTL designers wrote the Verilog code.

High-level synthesis tools can generate RTL from system code. However, it is more common for engineers to manually recode the design in RTL. This is an interpretation, rather than a transformation, of the design. Even if the RTL implementation is verified with numerous verification test benches, it is impossible to test all possible conditions with simulation-based methods.

Many verification tools and methods are used in a design flow, including assertion-based verification, random stimulus generation and coverage-driven verification. None of them leverage system models, even though they are functionally trustworthy. Sequential logic equivalence checking transfers the confidence of system models directly to the RTL implementation.

Arithmetic-block verification
The graphics processor market is driven by image quality, rendering performance and consumer buying seasons. For project teams creating the latest graphics processor chips, this mandates rapid development of new algorithms and designs. To meet this requirement, system models are used to close the gap between initial specification and tape-out. When this project started, directed random RTL simulation was running for days but still left the verification engineer in fear of a missed bug. The RTL design under test implemented both video and non-video instructions and was the arithmetic block of an ongoing project to create next-generation video processing chips.

The verification effort focused on 21 video instructions ranging from "parallel shift" to "absolute difference with reduction" operations. The goal of using sequential logic equivalence checking was the leveraging of the original system models written in C/C++ to improve RTL verification prior to chip-level regressions. Sequential equivalence checking was used to find bugs that simulation missed and to improve debugging of the RTL design.

A system model of the arithmetic block was implemented in 2,391 lines of C++ code. The first step in this project consisted of amending the C++ code to make it readable by the sequential logic equivalence checker. Because this model was not originally written for equivalence checking, some of the design constructs did not fit the sequential tools language subset. The project team used the statement to filter out constructs that did not have clear hardware concepts, such as reinterpret cast and static cast. These were changed in the C++ code.

In the future, it is expected that coding guidelines during C++ development will eliminate the need for modification in design blocks.

The team then set up the verification environment. Sequential logic equivalence checking requires that reset states and sequential differencessuch as timing and interface differences be specified before verification. Sequential differences are specified as I/O mappings and design latency.

For the C/C++ system model, a thin SystemC wrapper was added to introduce a reset and clock without changing the C++ model.

The RTL implementation of the video processor arithmetic block was 4,559 lines of RTL code with a latency of seven clock cycles. The C++ system model had a latency of one cycle, which was added by the SystemC wrapper. The team specified how often a new set of input data was sent to each design. Because the RTL was pipelined, new data was input every clock cycle. Thus, the throughput for both C++ and RTL was one.

Sequential logic equivalence checking uses sequential analysis and mathematical formal algorithms to verify that all input combinations result in the same output over all time for both models. Unlike simulation, it verifies all input conditions in parallel. Here, that translates into verifying all instructions simultaneously. The team decided to verify one video instruction at a time to improve debugging efficiency.

By knowing the instruction that was being tested, it was easier to identify the logic associated with any bug rather than to debug all instructions at the same time.

While verifying the first instruction (VEC4ADD), nine design bugs were found in the RTL model and one in the system model. The bug in the system model showed the designer how to remove ambiguity in the C++ code for future designs.

Sequential logic equivalence checking identified design differences in short counterexamples of 10 clock cycles or less. For each counterexample waveform, a waveform is generated to show the precise sequence of inputs that caused the design difference.

Test bench reuse
For each instruction, sequential logic equivalence found the difference and created the counterexample in less than 5mins. Sequential logic equivalence checking will also generate counterexamples in the form of test benches that can be run in simulation with the original C and RTL design. Test benches contain monitors to expose the same design bug shown in waveforms.

Counterexample test benches were reused as a unit-level regression test suite.

After fixing the code for the VEC4ADD instruction, the sequential logic equivalence checker proved equivalency between the system models and RTL in 361s using 52Mbytes. That compares with running 3.7 x 1,034 test vectors for exhaustive simulation of this instruction, which even on a 1 million-cycle/second emulator would take more than a lifetime to verify.

SystemC wrapper was used for the C/C++ system mode: introduced a reset and clock without changing the C++ model.

The total effort to verify the first instruction (VEC4ADD) was four days. The second instruction used the same setup scripts as the first instruction, allowing designers to focus on debugging immediately. They were able to find, fix and confirm fixes on 10 bugs for the second instruction (VEC2ADD) in less than two days. By extrapolating these results, it would take five to seven weeks, depending on the number of bugs found, to verify all 21 instructions. That compares with the six months the team spent to accomplish the same task for previous designs when using simulation-based methods.

The RTL verification of graphics instructions using system models was a success. A total of 19 functional bugs were found. Sequential logic equivalence checking improved the quality of verification and shortened the debug cycle with concise counterexamples. Bugs found included incorrect sign extension, missing clamping logic and initialization errors that would have led to reduced image quality, software workarounds or a respin of the silicon.

Sequential logic equivalence checking has the ability to find bugs and verify RTL implementations using system models written in C/C++ or SystemC. It improves functional verification effectiveness without requiring additional test benches or assertions. It minimizes design risk by identifying difficult-to-find bugs and those missed by traditional simulation methods.

- Jerome Bortolami
Senior Field Applications Engineer
Calypto Design Systems Inc.

Article Comments - Use system models for better verific...
*? You can enter [0] more charecters.
*Verify code:


Visit Asia Webinars to learn about the latest in technology and get practical design tips.

Back to Top