VHD2CA

A prototype of a compiler from VHDL to counter automata.

Developed by:

Publications:

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:

ARMC: Abstract Refinement Model Checker
Blast: Berkeley Lazy Abstraction Software Verification Tool
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

Options:

-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.

Example:

$ ./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:

Create a model from component.vhd,
set the initial state by setting v1=0 and v2=1,
set the output type as an ARMC model,
mark variable 'bad' as a variable representing the bad state (bad state: b=1).

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:

entity
generic
architecture
signals of std_logic and std_logic_vector type
direct assignments:
```
x <= func(y,z);
```
process
if statements

Unsupported:

library
package
for, case, with
choices in expressions:
```
x <= (0|1, 2|1, others=>0);
```
structural or user defined types
constants
variables

4. Acknowledgement

This project was developped with support coming from:

Liberouter project.
VeriFIT research group.
The project 102/07/0322 of the Czech Grant Agency.
The project CEZ MSM 0021630528 of the Czech Ministry of Education.