Accession Number : ADA187532

Title :   Formal Multilevel Hierarchical Verification of Synchronous MOS VLSI Circuits.

Descriptive Note : Technical rept.,

Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE ARTIFICIAL INTELLIGENCE LAB

Personal Author(s) : Weise, Daniel W

PDF Url : ADA187532

Report Date : Jun 1987

Pagination or Media Count : 170

Abstract : I have designed and implemented a system for the multilevel verification of synchronous MOS VLSI circuits. The system, called Silica Pithecus, accepts the schematic of an MOS circuit and a specification of the circuit's intended digital behavior. Silica Pithecus determines if the circuit meets its specification. If the circuit fails to meet its specification Silica Pithecus returns to the designer the reason for the failure. Unlike earlier verifiers which modelled primitives(e.g., transistors) as unidirectional digital devices, Silica Pithecus models primitives more realistically. Transistors are modelled as bidirectional devices of varying resistances, adn nodes are modelled as capacitors. Silica Pithecus operates hierarchically, interactively, and incrementally. Major contributions of this research include a formal understanding of the relationship between different behavioral descriptions (e.g., signal, boolean, and arithmetic descriptions) of the same device, and a formalization of the relationship between the structure, behavior, and a context of a device. Given these formal structures, my methods find sufficient conditions on the inputs of circuits which guarantee the correct operation of the circuit in the desired descriptive domain. These methods are algorithmic and complete. They also handle complex phenomena such as races and charge sharing. Informal notions such as races and hazards are shown to be derivable from the correctness conditions used by my methods.

Descriptors :   *DIGITAL SYSTEMS, *SILICON DIOXIDE, *TRANSISTORS, ARITHMETIC, BEHAVIOR, CAPACITORS, CIRCUITS, HAZARDS, OPERATION, SPECIFICATIONS, UNIDIRECTIONAL

Subject Categories : Electrical and Electronic Equipment
      Solid State Physics

Distribution Statement : APPROVED FOR PUBLIC RELEASE