BIDS: A Method for Specifying and Verifying Bidirectional Hardware Devices

Previous methods of formally verifying hardware designs have been highly simplified in comparison to the physical operation of the hardware devices themselves, which is appropriate for many kinds of circuit design but not for others. In particular, the register-transfer model and the state-transition model have not been able to handle bidirectionality (allowing lines sometimes to be used for input and at other times for output). The predicate model can handle simple cases of bidirectionality, but breaks down in others, particularly when gate capacitance and/or charge sharing are involved. In this paper we describe BIDS (BIdirectional Device Specification), a more elaborate model of hardware devices for formal verification, which we believe will be adequate for most techniques that designers commonly use, including bidirectionality, gate capacitance, and charge-sharing.