DocumentCode
3442200
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
fYear
1996
fDate
11-14 Mar 1996
Firstpage
605
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;
fLanguage
English
Publisher
ieee
Conference_Titel
European Design and Test Conference, 1996. ED&TC 96. Proceedings
Conference_Location
Paris
ISSN
1066-1409
Print_ISBN
0-8186-7424-5
Type
conf
DOI
10.1109/EDTC.1996.494369
Filename
494369
Link To Document