Cell Library Verification Using Symbolic Simulation

Standard cell libraries have been a mainstay of chip design for many decades since the inception of logic synthesis and composition methodologies. Cell library IP typically contains Verilog models describing the cell functionality, schematic derived transistor level netlists, place and route views, physical layout views, post-layout extracted netlists as well as characterized timing and power models. Chip design teams invoke various cell views within the Electronic Design Automation (EDA) tool chains they employ at different stages of their chip design, verification and power-performance-area (PPA) optimization project timeline.

Cell library teams maintain a rich infrastructure that interlocks cell design, characterization, model generation and validation to provide cell library IP with the high quality and consistency required by their customer design teams. Foundational to this infrastructure is the methodology of utilizing binary vector-based simulation both for verifying cell functionality and performing timing and power characterization. For the typical standard cell offerings, such as multi-input logic gates or latches and flip-flops, binary vector simulation has traditionally provided sufficient logic coverage completeness.

However, in the last 10 years, two industry trends have strained binary vector simulation methodology. First, as chip complexity has increased, so too has the commensurate need for more sophisticated cell functionality to be added to cell libraries. In addition to standard cell offerings, libraries now contain complex macros such as retention flops, multi-bit storage elements, synchronizers and counters, to name a few. For these kinds of cells, functional verification completeness extends beyond applying an extensive set of binary input vectors. These vector combinations must also account for dependencies upon the storage node logic values in these complex state elements. This verification challenge of convolving internal state node dependency with binary input vector combinations is exacerbated if the cells have any feedback or pipelined depth.

Next, the industry trend toward low-power designs resulted in chip designs featuring multiple power domains, each containing separate voltage supplies whose value can be independently adjusted or even turned off entirely. Such a consequential feature has to be integrated into every component and representative model through the entire design hierarchy, rippling down to the individual cell library models. In this case, the cell Verilog model must account for all kinds of on/off power state conditions, including catching the possibility that the supply and ground connections are incorrectly reversed.

The task of fully verifying power-aware library cell models, while also accounting for internal state dependencies and all possible input vector combinations becomes protractedly more challenging and increases the risk of test escapes. As such, cell library teams have explored formal verification techniques to achieve full functional verification coverage.

For almost two decades, formal verification techniques have been an innate part of chip design verification as the problem of test coverage completeness was encountered on much larger designs with higher pin count and more complex logic cones and state dependencies long before the need manifested for cell library verification.

Most standard formal techniques infer correct register mapping between design representations in order to determine state point logical equivalence, a task achievable within a synthesis-based flow intended for gate level designs where these registers are represented by discrete cell library flops or latches, but not for flattened designs consisting of transistor level circuits. More advanced techniques such as model checking and property proving are also limited by the fact that they cannot work directly with full custom circuit designs containing transistor elements.

The one formal method that has been proven to work well with transistor level netlists is symbolic simulation. This technique can also support both behavioral and synthesizable RTL, so it is ideally suited to verify custom designs which often contain circuits not typically modeled with synthesizable RTL.

Symbolic simulation involves replacing the binary value applied to each design input pin with a symbolic variable.

Image 1: Symbolic Simulation Delivers High Coverage Functional Verification

The input pin symbols propagate through the design, generating Boolean logic min-terms at the output of each local channel connected transistor circuit topology along the way, culminating in a final Boolean logic equation at each cell output pin. Since each symbol contains all possibilities of 0, 1, X or even tristate Z, formal verification completeness requires the number of simulation cycles to be at least equal to the pipeline depth of the design. As such, symbolic simulation is commonly used to verify memories which typically have low sequential depth such as SRAMs, multi-port register files, CAMs and ROMs.

Image 2: Symbolic Simulation Propagation Example

When both the reference RTL model and the implemented cell schematic netlist undergo symbolic simulation, the resulting logic equations at their respective cell output pins can be checked against each other via formal equivalence logic proofs. If there is a mismatch, a counter example is automatically generated via binary vector simulation for the user to debug via waveforms. If the reference and implementation design views are equivalent, there will be no associated waveforms to review so coverage analysis is used to complement the symbolic simulation to provide metrics of design verification completeness. Coverage metrics include verifying all the input symbols manifested in the output equations, all the design internal nets are symbolic and full code coverage in both design representations.

Symbolic simulation technology can be used to expand the scope of cell verification beyond logic functional equivalence. While input pin symbols are coded with the full set of binary or even quaternary logic values, other properties can be attached to these symbols as well. Most pertinent for power-aware verification would be embedding each pin’s power domain information into its respective symbol. With this facility, circuits containing multiple power domains can be dynamically checked to see if there are electrical hazards at the power domain interfaces. Such checks include detecting missing voltage level shifters, incorrect isolation between power domains due to power gating, multi-transition glitches or unwanted sneak paths between different supply voltage sources bearing the same logic value.

Image 3: Symbolic Simulation for Electrical Hazard Checks

While this category of circuit electrical verification has been explored with static netlist checkers or vector-based simulation, the former can only catch connectivity based electrical rule violations and the vector set limits the latter’s ability to detect transient violations. Neither of these limitations apply to dynamic symbolic simulation which invariably exposes electrical rule violation test escapes inherent with the other techniques.

Symbolic simulation is a proven technique for custom circuit formal verification. Historically, it has been used to verify large designs, such as SRAMs, but the complexity of some library cells combined with the power-aware verification completeness requirements to check all logic conditions on both input and power supply pins, as well as the internal state node dependency, has now made symbolic simulation an attractive solution for cell library functional verification. Furthermore, this formal technique expands the scope of power-aware verification beyond logic purely verification to also include formal circuit checks for electrical hazard detection.

The Synopsys ESP tool has been the industry standard solution for custom circuit formal verification. It employs symbolic simulation for both formal equivalence check and electrical hazard detection.