THE VLSI HOMEPAGE

Formal Verification is categorized into Equivalence Checking that checks whether the implementation has been preserved during the entire ASIC flow and Model checking that checks whether the implementation satisfies the properties of the design specification.

Proving equality between high level description of a design and it’s physical implementation is very difficult - running RTL and gate level regressions to compare functionality is very arduous and time consuming. A more desirable approach is to use mathematical reasoning techniques by partitioning the design into smaller components and verifying the Boolean logic equivalency between the reference model (RTL) and the implementation model (netlist). This is categorized under formal verification as Equivalency Checking.

In a typical ASIC flow, the RTL is the reference golden model and the equivalence checking is run on the synthesized netlist v/s RTL. The tool breaks the pipelined design into smaller logic cones (also referred to as cutpoints) and maps the RTL registers to the netlist flop instances (apart from mapping the IO ports). The tool stimulates the design using mathematical algorithms and compares the output of each logic cone for equivalency. Equivalency checking is faster as the entire verification is static and also run to check equivalency between a synthesized netlist and a routed netlist (with DFT inserted).

In addition to equivalency checking, mathematical techniques ( such as state space exploration for FSM using Ordered Binary Decision Diagrams OBDD) are being devised to prove the functionality of the design known as Model checking. Model checking can help uncover bugs in a design that are intricate and difficult to detect in a verification suite due to complex interactions between design modules.

Several vendors offer property specification semantics that can be inserted as comments in RTL for model checking. Using these languages, it is possible to define static and temporal event assertions, property and constraints in the design. The design engineer uses these semantics to embed assertions/event monitors in RTL while the verification engineer develops the assertion library for model checking.

Assertion checkers are very useful in design phase in putting down the design assumptions and constraints and capturing undesirable behavior. Event monitors are useful in flagging corner case events that a designer is concerned about.

While equivalency checking has found widespread use in the industry, model checking has very minor acceptance in the community, mainly because of designer’s resistance to change and maturity of the tools/languages. Formal Verification increases productivity of a design and is likely to play a major role in ASIC flow in the future.

Share This

Traditional verification strategies involve writing directed testcases to exercise all known features of the Design under Test (DUT) and the environment is often written in HDL or ‘C’. This method has proved very tedious and inadequate in addressing all possible scenarios, not to mention the effort/time taken.

A solution to this productivity issue has been to raise the level of abstraction and use constrained random stimulus to stress the design - Hardware verification languages (HVL) like ‘e’ or Vera use Object Oriented Programming (OOP) features, complex data types for higher abstractions, automated configurable tasks and also understand the hardware concepts of time and concurrency.

A typical transaction level verification environment is shown below comprising of two major components - Test functions and Test Harness (from Janick Bergeron’s Writing Testbenches). The Test harness integrates all the transaction layer components necessary to exercise the DUV and is self-contained. Test functions use procedures from the test harness to generate data items and configuration constraints.

Self-checking scoreboards with data extractors, reference models and checkers are also critical parts of Test functions. The coverage analyzer with functional coverage items and cross coverage items also gathers statistics from the generator/monitor to track the verification progress.

Transaction layer verification environment

Traffic generator - As the name implies, the traffic generator generates data items (packets, cells, frames) using OOP cencepts to stimulate the design. These data items are generated randomly but with proper hard and soft constraints so that no illegal data types are generated.

Bus Functional Model (BFM) - BFMs also known as Drivers, model the physical interface of a standard protocol like PCI, SATA to exercise the DUT at one end and at the other end, offer a transaction layer level inteface to the Test functions using procedures.

Protocol Monitors - do not drive any signals, monitor the DUT outputs, identifies all the transactions and report any protocol violations.

Scoreboards - Self-checking, integrates a reference model that dynamically processes the input stimulus to generate the expected output. The transformation is purely functional and does not include any latency and physical interface behavior. The Scoreboard records all transfer function outputs and compares them against Rx BFM outputs for integrity.

Coverage - Random testcase environments are coverage driven - only coverage can track the progress of verification to check if all the possible scenarios have been covered.

Two types of coverage - functional coverage that answers if functionality of the design has been verified and code coverage that answers if particular piece of code has been exercised.

Code coverage includes FSM coverage (if all transitions from one state to another are covered), line coverage (if all the lines in a module are covered), toggle coverage (if all signals are toggling from 0 -> 1 and 1 -> 0) and conditonal coverage (cover all conditions like in a if-else statement).

We will revisit each of these modules in detail with examples in ‘e’ or Vera in another post.

Share This

Verification consumes more than 70% of the effort and is on the critical path to tapeout in today’s complex, multimillion gate ASICs. To expedite the time-to-market duration, current methodologies focus on parallelizing verification effort with design, automate the verification process partly and also verify at higher abstraction layers.

A typical verification flow is shown in the figure below.

Design Verification Flow

The architecture spec details the chip functional requirements and features to be supported and is the starting point for both design and verification. The Verification plan clearly defines the features that will be verified in the design and prioritize testcases based on the schedule and critical features. The entire testsuite will be covered in the plan and both the design/verification teams review this VP to ensure that there are no holes in verification and that all features will be verified.

The verification environment can be a black-box model with no knowledge of implementation details - it applies the appropriate stimulus at the design inputs and checks the outputs against expected behavior. The entire design is black-boxed and advantages is reusability of generic verification IPs. Alternatively, it can be a white-box model with full controllability and observability in the design.

The verification environment integrates the stimulus generators, bus functional models, checkers and scoreboards usually written in a high level verification language (HVL) like specman ‘e’ or Vera. We will cover these modules in detail in another post.

Testcases can be either random or directed - directed testcases as the name indicates stimulate only one particular feature in the design and observe the response. Random testcases exercise the design within bound but random constraints. The VP determines the number of testcases to be written and the regression suite covers all these testcases.

Coverage metrics track the progress of verification and help in identifying the holes in verification. Any bug uncovered in the regression suite is filed in a bug-tracking database and fedback to the design team for correcting the design. Verification is said to be 100% done when the coverage metrics meet the goals defined in the verification plan.

Janick Bergeron’s “Writing Testbenches” covers the entire verification cycle in detail and is highly recommended for any newbie/experienced verification engineer.

Share This