Show simple item record

dc.contributor.authorLi, Xiaoshan
dc.contributor.authorCau, A. (Antonio)
dc.contributor.authorMoszkowski, B. C.
dc.contributor.authorColeman, Nick
dc.contributor.authorZedan, Hussein
dc.date.accessioned2005-09-05T19:19:28Z
dc.date.available2005-09-05T19:19:28Z
dc.date.issued1997
dc.identifier.citationLi, 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.isbn0412813300
dc.identifier.otherIR/2005/20
dc.identifier.urihttp://hdl.handle.net/2086/43
dc.description.abstractIn 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.statementofresponsibilityNick Coleman - full name J. Nick Coleman
dc.format.extent146210 bytes
dc.format.extent197640 bytes
dc.format.mimetypeapplication/pdf
dc.format.mimetypeapplication/postscript
dc.language.isoenen
dc.publisherChapman & Hall on behalf of the International Federation for Information Processing (IFIP)en
dc.relation.ispartofseriesSTRLen
dc.relation.ispartofseries1997-3en
dc.subjectinterval temporal logicen
dc.subjectprocessor verificationen
dc.subjectexecutable specificationen
dc.subjectcompositionalityen
dc.titleProving the correctness of the interlock mechanism in processor design.en
dc.typeBook chapteren
dc.identifier.doihttp://dx.doi.org/10.1007/978-0-387-35190-2_2
dc.researchgroupSoftware Technology Research Laboratory (STRL)


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record