Title :
Verification of parameterized asynchronous circuits: a case study
Author :
Yoneda, Tomohiro ; Ohtsuka, Yutaka ; Saarepera, Mart
Author_Institution :
Dept. of Comput. Sci., Tokyo Inst. of Technol., Japan
Abstract :
We demonstrate the normal verification of a parameterized asynchronous circuit which has request and acknowledgment controls through data paths. We propose a new encoding technique of the data path and construct a finite abstracted model. The properties expressed by ACTL formulas are model checked in the abstracted model, and then the correctness of the abstraction is mechanically proven using PVS
Keywords :
asynchronous circuits; formal verification; logic CAD; logic testing; parallel programming; ACTL formulas; PVS; abstracted model; acknowledgment controls; correctness; data path; data paths; encoding technique; finite abstracted model; model checking; normal verification; parameterized asynchronous circuit verification; Asynchronous circuits; Computer aided software engineering;
Conference_Titel :
Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on
Conference_Location :
Fukushima
Print_ISBN :
0-8186-8350-3
DOI :
10.1109/CSD.1998.657540
