A System for Modelling and Proving Circuits
Michel Allemand, Solange Coupet-Grimal, Line Jakubiec, J.-L. Paillet · 1996
rmations. We modify an already de#ned functional algebra that we called P-Calculus and enrich it with new operators. In addition we couple it with a formal system involving a typed formal language and a rewriting system. In order to get reliable devices it is crucial to have proof processes validated by proof-assistants. Various provers are already used for the formal hardware veri #cation such as Nqthm, hol, Nuprl. In fact, it is of interest to use several complementary provers in order to face the problems raised by such or such devices. Wechose to explore the capabilities of two provers lp #3# and Coq #2# presenting rather di#erent features. An interface executes the P-calculus expressions processing and translates them into the syntax of the provers. We carried out several proofs of sequential circuits in both provers lp and Coq #1#, investigating their potentials and taking advantage of their particular features in order to get processes