Title :
A system for modelling and proving circuits
Author :
Allemand, Michel ; Coupet-Grimal, Solange ; Jakubiec, Line ; Paillet, Jean-Luc
Author_Institution :
Lab. d´´Inf., CNRS, Marseille, France
Abstract :
We present the architecture of FORMATH, a system for modelling and proving circuits. Its core is a formal system, the P-calculus which allows one to accurately describe structures and behaviours of circuits. In order to perform verifications, the P-calculus is implemented into proof assistants
Keywords :
calculus; circuit CAD; formal verification; logic CAD; sequential circuits; theorem proving; CAD; FORMATH; P-calculus; circuit behaviour; circuit modelling; formal system; formal verification; proof assistants; sequential circuits; synchronous circuits; theorem provers; Algebra; Calculus; Circuit simulation; Circuit synthesis; Coupling circuits; Digital circuits; Electronic mail; Formal languages; Formal verification; Hardware design languages;
Conference_Titel :
European Design and Test Conference, 1996. ED&TC 96. Proceedings
Conference_Location :
Paris
Print_ISBN :
0-8186-7424-5
DOI :
10.1109/EDTC.1996.494369
