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

CRC-16 and CRC-32 algorithms are widely used in diverse communication protocols for robustness. The basic idea behind CRC is that the transmitter computes a string of bits called frame check sequence (or checksum) for each frame based on it’s contents and appends it to the end of the message before sending it to the receiver. The receiver then performs a similar computation and checks the checksum for any induced errors.

To detect burst errors (an error burst begins and ends with an error bit while the intermediate bits are correct), polynomial codes are more reliable than parity calculation. Polynomial codes exploit the modulo-2 arithmetic properties of binary numbers (i.e. binary arithmetic operations without any carries).

CRC computation involves appending a string of zeros to the frame equal in number to the number of FCS bits and modulo-2 divide by using a generator polynomial containing one more bit than the FCS to be generated. This division is similar to performing a bit-wise XOR opertation in the frame - the remainder is the checksum (FCS) that is transmitted. Similarly, the receiver divides the received frame using the same polynomial and checks if the remainder is zero. If the remainder is non-zero, the message has been corrupted.

We can cover CRC generation using an example - consider the message 11100110 that needs to be appended with 4-bit FCS using a generator polynomial of 11001. We need to append four 0’s to the message and modulo-2 divide it by generator polynomial.

Checksum computation

At the receiver end, the message 1 1 1 0 0 1 1 0 0 1 1 0 is modulo-2 divided by 1 1 0 0 1 to check if the remainder is zero.

The schematic is shown below for the four bit checksum computation, the FCS shift register is cleared and first octet is parallel-loaded into the parallel-in serial out shift register. This data is now shifted out MSB first and the shifted out data is XORed with X^3 and passed via feedback path to the selected inputs of FCS shift register. After the entire message has been transmitted, the fcs_ctrl changes from 1 -> 0 so that the current contents of FCS register (the remainder) follows the frame contents.

4-bit CRC schematic

Similarly on the Rx side for checking, the data is shifted into the serial-in parallel-out shift register and the serial data is XORed with X^3 and feedback path drives the FCS shift register. Once the entire message is received, the four bits of FCS register are checked to see if they hold 0s.

The choice of generator polynomial is important since it determines the number of errors it detects. A generator polynomial of N bits will detect single-bit, double-bit errors, all error bursts < N and all odd number of bit errors. The CRC-16 algorithm uses the polynomial X^16 + X^15 + X^2 + 1.

Tanenbaum goes into detail of choosing CRC polynomials in Computer Networks.

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