THE VLSI HOMEPAGE

Need for SystemVerilog

As ASIC designs get complex and grow larger in size, the modeling of these designs using register transfer level languages like Verilog also scale accordingly. In addition to verify these designs, use of Hardware Verification Languages (HVL) like ‘e’ to with new semantics/concepts pose a steep learning curve. To overcome these limitations, a unified language for both design and verification based on existing Verilog standard (and backward compatible to Verilog) was conceived.

SystemVerilog (Standard IEEE 1800-2005) is based on Verilog-2005 standard and includes new, effective and useful constructs for both design and verification. It integrates high-level hardware modeling extensions to Verilog with Hardware verification language (HVL like OpenVERA, ‘e’) constructs to create a unified design and verification language - Hardware Description and Verification Language (HDVL).

Key SystemVerilog Enhancements for Design

• New hierarchical structure (interface - endinterface) for modeling at higher levels of abstraction. It encapsulates communication and protocol checking within the design eliminating any conection errors.

• Datatype extensions - SystemVerilog supports the four state (0,1,x,z) Verilog datatypes and extends it to four/two state logic, bit, int, longint datatypes. Usage of two state (0,1) datatypes like bit, int make the simulations run faster. User defined datatypes using typedef, enumerateddatatypes using enum are also supported.

• Supports static variables that are initialized at time 0, global variables that are accessible from any scope (for example, const is a global constant), local variables that are available locally (for example, localparam).

• Supports packages for sharing across different modules using package - endpackage, derived from VHDL

• Supports structures and unions similar to C to confine multiple bus signals within one structure. Also add object-oriented features from C++ like classes. Classes can be public or private and are used to define methods and properties of the object.

• Verilog task and function enhancements such as arguments can be passed by reference, functions can be void etc.

• C features like for and do loops, continue, break etc. Unpacked arrays where all or part elements of an array can copied to another array unlike Verilog that allows only one element of array to be accessible at a time.

Key SystemVerilog Enhancements for Verification

• Supports built-in class objects (semaphore and mailbox) for synchronizing parallel activities in a testbench. semaphore is arbitration of shared resources (keys) among different processes - if no key is available to a process, it can wait until required number of keys are returned to the bucket. mailbox helps in exchanging messages between processes. The message queue behaves like a FIFO.

• Supports dynamic arrays that can be restricted to a particular size during runtime and associative arrays that can be referenced using enum types as values.

• Two random number classes rand and randc that aid in constraining the random values generated for verification.

• Supports assertions conforming to Property Specification Language (PSL) standard.

Share This

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