ON THE FORMAL SPECIFICATION AND VERIFICATION OF DIGITAL CIRCUITS

This paper presents a design technique for digital circuits at register-transfer level (RTL). The two most important notions within the design trajectory are the formal specification of the circuit and the formal verification of an implementation, that a designer comes up with, against this specification. A mathematical description formalism is presented that can be used to describe both the specification and the implementation of RTL circuits and, furthermore, to formally verify the implementation against the specification. As an example, the design of an n-th order infinite impulse response (IIR) filter is presented. It is shown that several different implementations are possible and that the trade-off between speed and chip area can be made very precisely. © 1989.