DocumentCode
2700334
Title
Retargeting a hardware compiler proof using protocol converters
Author
Brown, Geoffrey ; Luk, Wayne ; O´Leary, John
Author_Institution
Dept. of Electr. Eng., Cornell Univ., Ithaca, NY, USA
fYear
1994
fDate
3-5 Nov 1994
Firstpage
54
Lastpage
63
Abstract
We show how to retarget the correctness proof of a hardware compiler generating two-phase delay-insensitive circuits to a compiler generating four-phase speed-independent circuits. We use protocol converters to convert the specifications of our compiler´s two-phase circuit elements into equivalent specifications for four-phase elements. The processes of converting the specifications and verifying their implementations are automated
Keywords
asynchronous circuits; correctness proof; equivalent specifications; four-phase elements; four-phase speed-independent circuits; hardware compiler proof; protocol converters; specifications; two-phase circuit elements; two-phase delay-insensitive circuits; Asynchronous circuits; Buildings; Delay; Europe; Hardware; Laboratories; Production; Program processors; Protocols; System recovery;
fLanguage
English
Publisher
ieee
Conference_Titel
Advanced Research in Asynchronous Circuits and Systems, 1994., Proceedings of the International Symposium on
Conference_Location
Salt Lake City, UT
Print_ISBN
0-8186-6210-7
Type
conf
DOI
10.1109/ASYNC.1994.656286
Filename
656286
Link To Document