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

Volume

1

fYear

1995

fDate

15-16 May 1995

Firstpage

74

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;

fLanguage

English

Publisher

ieee

Conference_Titel

WESCANEX 95. Communications, Power, and Computing. Conference Proceedings., IEEE

Conference_Location

Winnipeg, Man.

Print_ISBN

0-7803-2725-X

Type

conf

DOI

10.1109/WESCAN.1995.493948

Filename

493948