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.