Verisym: Verifying circuits by symbolic simulation

Abstract

Verisym is used to check the functional behavior of circuit designs. It was initially targeted at verifying custom memory designs, which present major difficulties for current production tools, but it is a general-purpose system that has also been applied to arithmetic and control circuits. Verisym has been used to validate custom memory array designs containing up to four million transistors in a few hours on standard hardware. Verisym symbolically simulates the execution of a circuit, given as either a transistor-level schematic or an RTL description, to check a property, given as the stimulus to the circuit and the expected response. It can also simulate two circuit descriptions (of the same or different types), applying the same stimulus to each, and checking that the responses are the same. Simulation is performed by executing a finite-state machine model extracted from the circuit description. A property is checked with a single run of the model (one run of each model for dual simulation). Execution is symbolic, so properties can assert properties about all possible values on particular nodes, and complete coverage of a circuit's behavior is possible. Concrete counter-example runs can be generated as a debugging aid if a property check fails. Verisym is integrated into IBM's Nutshell EDA environment, which provides a common user interface and scripting language across IBM's EDA tools, and allows interoperation between them.