Formal Multilevel Hierarchical Verification of Synchronous MOS Circuits

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.

Thermal Noise Behavior of the Bridge Circuit

This paper considers a connection between the deterministic and noisy behavior of nonlinear networks. Specifically, a particular bridge circuit is examined which has two possibly nonlinear energy storage elements. By proper choice of the constitutive relations for the network elements, the deterministic terminal behavior reduces to that of a single linear resistor. This reduction of the deterministic terminal behavior, in which a natural frequency of a linear circuit does not appear in the driving-point impedance, has been shown in classical circuit theory books (e.g. [1, 2]). The paper shows that, in addition to the reduction of the deterministic behavior, the thermal noise at the terminals of the network, arising from the usual Nyquist-Johnson noise model associated with each resistor in the network, is also exactly that of a single linear resistor. While this result for the linear time-invariant (LTI) case is a direct consequence of a well-known result for RLC circuits, the nonlinear result is novel. We show that the terminal noise current is precisely that predicted by the Nyquist-Johnson model for R if the driving voltage is zero or constant, but not if the driving voltage is time-dependent or the inductor and capacitor are time-varying