Proving the correctness of the interlock mechanism in processor design.

De Montfort University Open Research Archive

Show simple item record

dc.contributor.author Li, Xiaoshan
dc.contributor.author Cau, A. (Antonio)
dc.contributor.author Moszkowski, B. C.
dc.contributor.author Coleman, Nick
dc.contributor.author Zedan, Hussein
dc.date.accessioned 2005-09-05T19:19:28Z
dc.date.available 2005-09-05T19:19:28Z
dc.date.issued 1997
dc.identifier.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? en
dc.identifier.isbn 0412813300
dc.identifier.other IR/2005/20
dc.identifier.uri http://hdl.handle.net/2086/43
dc.description.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. en
dc.description.statementofresponsibility Nick Coleman - full name J. Nick Coleman
dc.format.extent 146210 bytes
dc.format.extent 197640 bytes
dc.format.mimetype application/pdf
dc.format.mimetype application/postscript
dc.language.iso en en
dc.publisher Chapman & Hall on behalf of the International Federation for Information Processing (IFIP) en
dc.relation.ispartofseries STRL en
dc.relation.ispartofseries 1997-3 en
dc.subject interval temporal logic en
dc.subject processor verification en
dc.subject executable specification en
dc.subject compositionality en
dc.title Proving the correctness of the interlock mechanism in processor design. en
dc.type Book chapter en
dc.researchgroup Software Technology Research Laboratory (STRL)


Files in this item

This item appears in the following Collection(s)

Show simple item record