Reasoning About The VHDL Standard Logic Package Signal Data Type

Formal verification methods provide a way to prove that a circuit structure correctly implements its specification. Low level gate and transistor logic circuits can be verified using methods such as symbolic simulation. Higher level circuits can be verified using theorem--proving methods, providing a multi-leveled approach to complex device verification. Correct modeling of many VLSI circuits requires a signal value data type that includes some degree of strength indeterminacy. The VHDL Standard Logic Package includes such a signal value data type, t wlogic, that includes 46 unique values. In this paper we provide a foundation for the t wlogic values and their resolution function that provides a possible link between simulation and theorem-proving. A formalization of the low level signal values used by design tools also facilitates reasoning about CAD tools. Keyword Codes: Keywords: 1 Motivation Many VLSI design techniques involve the use of varying sized transistors for interconnecte..