Digital Model for Level-Clocked Circuitry.

摘要

This thesis presents the formal background for a mathematical model for level-clocked circuitry, in which latches are controlled by the levels (high or low) of clock signals rather that transitions (edges) of the clocks. Such level-clocked circuits are frequently used in MOS VSLI design. Our model maps continuous data-domains, such as voltage, into discrete, or digital, data domains, while retaining a continuous notion of time. A level-clocked circuit is represented as a graph G = (V,E) where V consists of digital components--latches and functional elements--and E represents inter-component connections. The majority of this thesis concentrates on developing lemmas and theorems that can serve as a set of 'axioms' when analyzing algorithms based on the model. Key axioms include the fact that circuits in our model generate only well defined digital signals, and the fact that components in our model support and accurately handle the 'undefined' values that electrical signals must take on when they make a transition between valid logic levels. In order to facilitate proofs for circuit properties, the class of computational predicates is defined. A circuit property can be provided by simply casting the property as a computational predicate. (RH)