Functional Verification of MOS Circuits

This report describes the ideas behind Silica Pithecus, a program which verifies synchronous digital MOS VLSI circuits. Silica Pithecus accepts the schematic of an MOS VLSI circuit, declarations of the logical relationships between the inputs signals (e.g., which inputs are mutually exclusive), and a specification of the intended digital behavior of the circuit. If the circuit fails to meet its specification Silica Pithecus returns to the designer the precise reason it fails to do so. Unlike previous verification systems, Silica Pithecus employs a realistic electrical model. It also automatically generates the constraints on the inputs of a circuit which ensure the circuit will exhibit its intended digital behavior. These constraints are necessary for hierarchical verification. Silica Pithecus operates hierarchically, interactively, and incrementally.