< retour aux publications

Automatic generation of a provable circuit model: from VHDL to PVS

Auteur(s) : K. Morin-Allory, D. Borrione

Doc. Source: 8ème International Mathematica Symposium (IMS'06)

Publisher : IEEE

Pages : 12

A compiler and a simulator have been implemented in Mathematica The symbolic simulation of a clocked synchronized sequential circuit is used to compute the state transition function and the output function of the circuit underlying Mealy finite state machine, under the form of a normalized IF-THEN-ELSE expression. From that point, we automatically produce the mathematical formulation of the FSM, either as recurrence equations, or as a set of step functions. Finally, the post-processing part of the tool produces the model in the input syntax of a theorem prover, for further reasoning on the model properties. Currently, we implemented the flow for ACL2 and for PVS.