Main page -> Formal verification -> Translation VHDL to SMV

Translation VHDL to Verilog and Cadence SMV

For translation LeonardoSpectrum or Precision tools for VHDL synthesis is used. We use UNIX like operating systems.

Local informations for Liberouter team only

Translation for Liberouter team supports sirah.ics.muni.cz with Solaris. Verunka script is not functional at sirah.ics.muni.cz (this is only a translation machine). Verification for Liberouter team supports porto.liberouter.org, rioja.liberouter.org and chianti.liberouter.org with Linux and 4 GB of memory. Additional environment varibles for these machines is:
export PATH=$PATH:/usr/local/verif/bin
Please check whether there is a free computational capacity before your verification starts.

Global informations for all

Environment varibles for both synthesis and further verification:
export LIBEROUTER_PATH=your local CVS copy/liberouter
export PATH=$PATH:$LIBEROUTER_PATH/ver/scripts
export PATH=$PATH:$LIBEROUTER_PATH/ver/scripts/verunka
export PERL5LIB=$PERL5LIB:$LIBEROUTER_PATH/ver/scripts/verunka

Local copy of Liberouter CVS have to by created in $LIBEROUTER_PATH/liberouter.

VHDL source files are in directory $LIBEROUTER_PATH/liberouter/vhdl_design.

The components under verification mainly contains subdirectories:

comp/ - directory with subcomponents
doc/ - directory with component documentation
sim/ - directory with date for simulations
ver/ - directory with the following structure:
Makefile - Main Makefile
name_of_component_ver.xml - Verification Report, contains informations about synthesis, preconditions, formulas and its results.
<time_stamp>/ directories - for each version of verified component. Name of directory <time_stamp> corresponds with the value of exportdate attribute in Verification Report. This directory should contain:
- substs_source/ - directory with files that contain parts of Cadence SMV source. When is that part of source matched it should be substituted by the corresponding file in substs_target/ directory.
- substs_target/ - directory with files, which contain will be included to Cadence SMV source file instead of the previous matched content.

Command gmake gives you additional help for translation. For example command "gmake vhd_cvs v smv" in directory <some_component>/ver/<time_stamp> exports VHDL files from CVS (from date corresponding to <time_stamp>). And than it creates SMV file for future verification.

Command cp $LIBEROUTER_PATH/ver/reports/verification.dtd <some_component>/ver/ supports DTD file for Verunka script (temporary solution).

You should verify properties using command verunka.pl name_of_component in directory ver and pressing key "v".

The possible results of each formula:

none - The property is not yet verified.
true - The property is satisfied.
false - The property is not satisfied.
unfinished - The verification takes much time or memory. The official limit for unfinished formulas is 1 day or 2GB of memory exeeded.

The software for Verification and its dependencies

Cadence SMV for model checking.

tix (Tk Interface eXtension) for running vw (viewer for smv).

java for XSLT transformations (verification reports).

libxml for validation XML documents (verification reports).

saxon for XSLT transformations (verification reports).

g++, ntpdate general purpose.

LaTeX and prosper for creating presentations.

Translation of project Scampi (phase 1)

Working directory: $LIBEROUTER_PATH/vhdl_design/combo6/projects/scampi_ph1

In this working directory the file Modules.tcl determines which modules will be included in translation.

Translation top_level.vhd to top_level.v and than to top_level.smv:
gmake top_level.smv

This translation uses the following files:
$LIBEROUTER_PATH/vhdl_design/combo6/projects/scampi_ph1/Makefile
$LIBEROUTER_PATH/vhdl_design/base/Makefile.fpga.inc (included)

Leonardo spectrum depends on the following files:
$LIBEROUTER_PATH/vhdl_design/combo6/projects/scampi_ph1/Leonardo.ver.tcl
$LIBEROUTER_PATH/vhdl_design/combo6/projects/scampi_ph1/Modules.tcl (included)
$LIBEROUTER_PATH/vhdl_design/base/Leonardo.inc.tcl (included)

There are 7 from 83 modules empty:
MULT18X18, RAMB16_S18_S36, RAM64X1D, DCM, RAMB16_S18_S18, RAM16X1D, RAMB16_S9_S18