We present the architecture of Formath: a system for modelling and proving circuits. Its core is a formal system, the P-calculus which allows to accurately describe structures and behaviours of circuits. In order to perform verifications, the P-calculus is implemented into proof assistants (LP and COQ). Different aspects of the system are depicted and illustrated by several examples.
['Michel Allemand', 'Solange Coupet-Grimal', 'Line Jakubiec', 'Jean-Luc Paillet']
A system for modelling and proving circuits