An approach to the introduction of formal validation in an asynchronous circuit design flow

Author

Borrione, Dominique ; Boubekeur, Menouer ; Dumitrescu, Emil ; Renaudin, Marc ; Rigaud, Jean-Baptiste ; Sirianni, Antoine

Author_Institution

VDS group, TIMA Lab., Grenoble, France

fYear

2003

fDate

6-9 Jan. 2003

Abstract

This paper discusses the integration of model-checking inside a design flow for quasi-delay insensitive circuits. Both the formal validation of an asynchronous behavioral specification and the formal verification of the asynchronous synthesis result are considered. The method follows several steps: formal model extraction, model simplification, environment modeling, writing temporal properties and proof. The approach is illustrated on a small, yet characteristic, asynchronous selection circuit.

Keywords

asynchronous circuits; formal specification; formal verification; high level synthesis; integrated circuit design; integrated circuit modelling; asynchronous behavioral specification; asynchronous circuit design; asynchronous selection circuit; asynchronous synthesis; environment modeling; formal model extraction; formal validation; formal verification; model simplification; model-checking; quasidelay insensitive circuits; temporal properties; Asynchronous circuits; Circuit simulation; Circuit synthesis; Clocks; Cogeneration; Computational Intelligence Society; Formal verification; Registers; Wire; Writing;

fLanguage

English

Publisher

ieee

Conference_Titel

System Sciences, 2003. Proceedings of the 36th Annual Hawaii International Conference on

Print_ISBN

0-7695-1874-5

Type

conf

DOI

10.1109/HICSS.2003.1174811

Filename

1174811