Restricted symbolic evaluation is fast and useful

Abstract

A method is presented for simulation with two zillion and three values. The values that are propagated by the simulation include the familiar 0, 1, and X and also a collection of named unknowns and their formal negations. Each value fits into a single computer word. Applications of this restricted symbolic evaluation include design rule checking for circuits with embedded arrays and timing verification. The authors explore these two applications briefly. By carefully choosing rules for combining the two zillion and three values, and the representations of the values, it is possible to make simulation surprisingly efficient. The authors present two variants and an implementation of each. Both are fast; the faster one sometimes yields less information.