Formal Multilevel Hierarchical Verification of Synchronous MOS Circuits
Item
-
Title
-
en_US
Formal Multilevel Hierarchical Verification of Synchronous MOS Circuits
-
Creator
-
en_US
Weise, Daniel Wayne
-
Date
-
2004-10-20T20:10:37Z
-
Date Available
-
2004-10-20T20:10:37Z
-
Date Issued
-
en_US
1987-06-01
-
Identifier
-
en_US
AITR-978
-
Abstract
-
en_US
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, and 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 context of 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.
-
Extent
-
29323851 bytes
-
10323223 bytes
-
Format
-
application/postscript
-
application/pdf
-
Language
-
en_US
-
Relation
-
en_US
AITR-978