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