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
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;
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
DOI :
10.1109/ASYNC.1994.656286
