The structure of circuits is specified with Prolog; their function and timing behaviour is specified with interval temporal logic. These structural and behavioural specifications are used to formally verify the functionality of circuit elements as well as their timing characteristics. A circuit is verified by deriving its behaviour from the behaviour of its components. The derived results can be abstracted to functional descriptions with timing constraints. The functional descriptions can then be used in proofs of more complex hardware circuits. Verification is done hierarchically, with transistors as primitive elements. Transistors are modeled as switch-level devices with delay. In order to model delay, the direction of signal flow through each transistor must be assigned. This is done automatically by a set of Prolog routines which also determine the inputs and outputs of each circuit component. Interval temporal logic descriptions are expressed in Prolog and manipulated using PALM: Prolog Assistant for Logic Manipulation. With PALM, the user specifies rewrite rules and uses these rules to manipulate logical terms. In the case of reasoning about circuits, PALM is used to manipulate the temporal logic descriptions of the components to derive a temporal logic description of the circuit. These techniques are demonstrated by applying them to several commonly used complementary metal oxide semiconductor (CMOS) structures. Examples include a fully complementary dynamic latch and a 1-bit adder. Both these circuits are implemented with transistors and exploit 2-phase clocking and charge sharing. The 1-bit adder is a sophisticated full adder implemented with a dynamic CMOS design style. The derived timing and functional behaviour of the 1-bit adder is abstracted to a purely functional behaviour which can be used to derive the behaviour of an arbitrary n-bit adder.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:232797 |
| Date | January 1987 |
| Creators | Leeser, Miriam Ellen |
| Publisher | University of Cambridge |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
Page generated in 0.0016 seconds