Formal Verification of a Real-Time Hardware Design

As hardware systems continue to grow more complex, formal methods for their design and verification become increasingly important. In this paper, we develop the design and formal specifications for the receiver section of an Universal Asynchronous Receiver/Transmitter. Though no mechanical verification has been done, such a development methodology is essential for formal verification. The emphasis here is on transforming informal specifications into formal ones, and showing how these formal specifications impact the design. The specification process helps us in formulating bounds on the relative drift between the receiver and transmitter clocks. We then develop the design in a top-down manner using a hardware description language which borrows from both APL and PASCAL.