An introduction to symbolic simulation

Paul Hoxey from ARM, Clayton McDonald and David Guinther from Synopsys
(12/19/2005 8:30 PM EST)
EE Times

Three methods for testing functional equivalence are currently available to designers — conventional simulation, cone-based equivalence checking, and symbolic simulation. Most designers are familiar with the first two, while symbolic simulation is newer and has only been commercially available for a few years. Each method has its strengths, and the most effective approach depends on the specific application.

Symbolic simulation has been quietly gaining adoption among the world’s leading full-custom memory design teams over the last few years. In symbolic simulation, symbols such as data1, addr7, or w_enable, rather than binary 1s and 0s, are used as input vectors to simulate an RTL or Spice-level circuit. The simulator propagates symbols, rather than binary values, from inputs to outputs. The resulting output equations for the two designs are then compared and verified to be equivalent for all possible input combinations.

The use of symbolic simulation removes the RTL restrictions and circuit limitations inherent with today’s cone-based equivalence checking tools. This production-proven technology offers circuit designers the ability to directly verify the functionality of large complex memories and macro cells without having to re-code their RTL or modify their circuits as with other approaches.

Another key advantage is that designers can verify their RTL vs. Spice models much sooner in the design flow. Today’s symbolic simulation tools automatically create test benches, so designers can begin design verification earlier without waiting until RTL test benches and Spice test vectors are developed.

These new techniques can handle the complex netlists typically found in today’s gigabit memories because one symbolic vector can replace 2n binary vectors, where n is the number of inputs. Huge capacity, coupled with the ability to directly read Verilog RTL and Spice netlists, makes this approach ideal for memory verification applications.

This article outlines the key challenges of memory verification, and goes on to describe how symbolic simulation and its underlying technologies offer advantages for verifying full-custom circuit designs, such as memories and macro-cells. Application examples are provided along with a few examples of the types of problems that are often uncovered by using symbolic simulation early in the design flow.

Click here to read more ...