Citation:Li, X., Cau, A., Moszkowski, B., Coleman, N. and Zedan, H. (1997) Proving the correctness of the interlock mechanism in processor design. In: Advances in hardware design and verification: IFIP TC10 WG10.5 International Conference on Correct Hardware and Verification Methods, 16-18 October 1997, Montreal Canada, edited by Hon F. Li and David K. Probst, London: Chapman & Hall, on behalf of the International Federation for Information Processing (IFIP), 1997, pp?
Abstract:
In this paper, Interval Temporal Logic (ITL) us used to specify and verify the event processor EP/3, which is a multi-threaded pipeline processor capable of executing parallel programs. We first give the high level specification of the EP/3 with emphasis on the interlock mechanism. The interlock mechanism is used in processor design especially for dealing with pipeline conflict problems. We prove that the specification satisfies certain safety and liveness properties. An advantage of ITL is that it has an executable part, i.e., we can simulate a specification before proving properties about it. This will help us to get the right specification.
