For today's chip designers, integrating many different functions within a wireless device poses a severe challenge. The difficulty is not so much the design part. After all, the intellectual-property (IP) blocks that implement wireless functions are readily available from many commercial sources. The true challenge is the verification of these IP blocks as an integrated system.
You may have noticed that designers of wireless systems worldwide are quickly catching and riding the assertion-based design wave. They've learned that an assertion-based methodology offers them increased functional-verification coverage and a shortened means to verify integrated system-on-a-chip (SoC) designs. Recently, the formal-verification tools that exhaustively verify assertions have become increasingly popular. Such tools give designers a more thorough means of verifying their work.
Powering this wave is an open-source library of Verilog assertion monitors, called the Open Verification Library (OVL). It offers project teams the quick and easy adoption of a formal-verification methodology into simulation-based design flows. The library is available for free download from the Internet at www.verificationlib.org.
The OVL is indeed powerful. It provides a standard way to capture design behaviors that need to be verified. The library of assertions is composed entirely of standard VHDL and Verilog hardware description languages (HDLs). It is the only assertion method available today that works with all of the commercial electronic-design-automation (EDA) tools supporting these languages.
The most obvious advantage—and the reason that OVL has caught on—is that assertions only need to be specified once. They can then be verified with formal verification and software, including HDL-based simulators.
The assertion wave, while dramatic and fast moving, is hardly a surprising phenomenon. As wireless-design complexity explodes and design cycles shrink, functional verification has become more difficult. Assertions help by increasing the observability of complex designs. They make it easier to find bugs that might otherwise be missed due to incomplete vector sets. In other words, assertions serve as watchdogs in the design. They immediately alert designers when simulation triggers undesirable functional behavior.
Embedded assertions also provide a way to verify reusable IP. In an IP block, they create a permanent and portable record of design intent. They also help consumers verify that the IP has been used in the manner for which it was intended. By using input assertions or constraints, it's possible to verify that the blocks driving those inputs satisfy the IP-block input requirements. Output assertions, in turn, ensure that IP blocks produce outputs that meet the requirements of other blocks—the ones that are receiving these signals as inputs.
The formal verification of assertions offers even more advantages. When used with simulation, assertions catch bugs only when a designer happens to write a vector that triggers it. Formal techniques alleviate this problem because no test vectors or testbenches are required. On top of that, they provide exhaustive coverage for each assertion that is proven.
Essentially, formal verification increases the controllability of complex designs. To find every case in which an assertion could potentially be triggered, it sequentially analyzes the entire state space and all potential inputs. No test vectors are needed, so debug can start even earlier in the design cycle. As we all know, the earlier bugs are found, the easier they are to fix.
Assertions can either be used as targets for formal proof or as constraints. When used as constraints, assertions define the legal input behavior for the design under verification. Formal-verification tools then exhaust all of the possible inputs that satisfy the constraints during the process, thereby verifying assertions.
Formally verifying assertions reduces the time and effort required for simulation. Time spent on testbench development and actual simulation run time can be reduced too. This is crucial, as project teams are now beginning to understand that they need better verification methodologies in order to achieve functional closure on large wireless designs. Formal-verification tools can help find more bugs in less time while reducing the verification effort.
Until the recent introduction of standardized assertion-based techniques, such as OVL, it had been more difficult to implement formal-assertion checking into verification flows. Now, OVL has provided a standard set of assertion modules. These modules enhance simulation and ease the adoption of formal-assertion checking tools. Best of all, the library's assertion modules are written in a standard hardware description language. Designers no longer need to learn a proprietary language just to specify the design behaviors needing to be verified.
The bottom line here is that if your project team has yet to adopt an assertion-based design methodology, encourage them to jump in now. There's no better time to catch the wave!