A prototype of a compiler from VHDL to counter automata.

Developed by:
  1. Ales Smrcka
  2. Tomas Vojnar
  1. A. Smrcka, T. Vojnar. Verifying Parameterised Hardware Designs via Counter Automata. In Proc. of Haifa Verification Conference, LNCS vol. 4899, Springer-Verlag, p. 51-68, 2007. [pdf]

1. Requirements

POSIX OS, Python>=2.3. Check the version of python:
$ python -V
Python 2.3.4
To analyze the generated counter automata, you can use:
  1. ARMC: Abstract Refinement Model Checker
  2. Blast: Berkeley Lazy Abstraction Software Verification Tool
  3. Graphviz, dot for graphic representation of counter automata

2. Download and Installation

License GNU GPL v2.1 or any later, see http://www.gnu.org/licenses/gpl.html for more details.

Download vhd2ca-1.0.tar.gz:
$ wget http://www.fit.vutbr.cz/~smrcka/projects/vhd2ca/vhd2ca-1.0.tar.gz
Install: There is no installation, just unpack it and it works :-).
$ tar xzf vhd2ca-1.0.tar.gz
$ cd vhd2ca-1.0/
$ ./vhd2ca.py
./vhd2ca.py:no input file specified
for help: ./vhd2ca.py -h
syntax: vhd2ca.py [options] file(s)

3. Options + Usage

-b variable Mark variable as bad (go to the bad state if it equals to one).
-c v=value  Make a constant from the variable (a comma separated list of
            a value assignments, e.g., -c reset=1,wr=0,oe=1).
-x v:v1,v2  Create an exclude list for variable v. List is comma separated
            list of variable names, e.g., -x reset:clk1,clk2 means that
            reset can change only if both clk1 and clk2 are stable.
-i v=value  The initial evaluation over state variables (a comma separated
            of evaluations).
-t type     The output type of the automaton (see -l for the list of
            available types).
-l          List available automaton output types and exit.
-o file     Save the generated counter automaton to file.
--noca      Do not generate a counter automaton (try with -v3).
-m size     Set the maximum resident memory usage (in megabytes).
-p option1=value1,option2=value2
            Output plugin options.
-v level    Verbosity level:
    0       be quiet (except errors and warnings),
    1       progress and statistics (default),
    2       level 1 + nonstate/unused variables,
    3       print the intermediate model,
    4+      more debug information.
$ ./vhd2ca.py component.vhd
Show the list of variables, which initial evaluation is unknown.

$ ./vhd2ca.py -i v1=0,v2=1 --noca -v3 -b bad component.vhd
Show the intermediate behavioural model of component.vhd + some statistics of the model.

$ ./vhd2ca.py -i v1=0,v2=1 -t armc -b bad component.vhd
Does the following: You can find some more examples in the vhdl2ca-1.0/examples directory). The directory contains simple examples and a real-life component - asynchronous FIFO (OpenIP license) from the Liberouter project.

3. Supported VHDL Constructs

Supported syntax: Unsupported:

4. Acknowledgement

This project was developped with support coming from:
  1. Liberouter project.
  2. VeriFIT research group.
  3. The project 102/07/0322 of the Czech Grant Agency.
  4. The project CEZ MSM 0021630528 of the Czech Ministry of Education.
Ales Smrcka, smrcka@fit.vutbr.cz, FIT BUT, Oct 2007.