Extracting Behaviour from Synthesized Verilog
The verification of implemented algorithms can be decomposed into (i)
showing properties of an abstract representation of the algorithm and
(ii) showing the abstract representation is correctly implemented. In
this paper we discuss an approach to (ii) based on automatically
extracting formal logical models from the output of the CV3 Verilog
compiler. CV3 output is processed by inference using Hol98, but the use
of Hol98 is completely hidden from the user. The model extraction is
packaged as a Unix tool that reads a Verilog source file and creates a
Hol98 theory file. Command line options are used to select the kind of
model produced and the form in which it is represented. This work
illustrates the approach being explored by the PROSPER project, in which
user level tools make use of an internal proof engine.
Contact Mike Gordon (mjcg@cl.cam.ac.uk) for more details.