Title :
Higher order logic in reasoning about asynchronous circuits
Author :
Peters, J.F. ; Rahardjo, B.
Author_Institution :
Dept. of Electr. & Comput. Eng., Manitoba Univ., Winnipeg, Man., Canada
Abstract :
A formal process description of a delay insensitive asynchronous circuit (DIAC) in real time CSP mechanized in the higher order logic proof system (RTCSP-HOL) is presented. The syntax, process definitions, ontimeness, and deductions over time in RTCS-HOL are given. The delay caused by a wire in a DIAC is modeled using the wait process in RTCSP-HOL. The delay insensitivity of two gates in a C element is proved in terms of the timeliness of the processing of input signals by the two gates. The paper presents an illustration of how a DIAC designer might mechanize the formal specification and analysis of the behavior of DIACs and prove the delay insensitivity of a particular configuration of a DIAC
Keywords :
asynchronous circuits; formal logic; formal specification; inference mechanisms; logic CAD; C element; DIAC; RTCSP-HOL; delay insensitive asynchronous circuit; delay insensitivity; formal process description; formal specification; higher order logic; higher order logic proof system; input signals; ontimeness; process definitions; real time CSP; reasoning; wait process; Asynchronous circuits; Delay; Formal specifications; Hazards; Logic circuits; Real time systems; Safety; Silicon carbide; Thyristors; Wire;
Conference_Titel :
WESCANEX 95. Communications, Power, and Computing. Conference Proceedings., IEEE
Conference_Location :
Winnipeg, Man.
Print_ISBN :
0-7803-2725-X
DOI :
10.1109/WESCAN.1995.493948
