Hardware Description and Verification

Tools

Availability

The software tools used in this course should be available on all Linux computers at Chalmers. This includes remoteX.student.chalmers.se (where X = 1-5), which you can access with SSH over the network.

You can also run some of the tools on your own computer.

VHDL circuit simulators

ModelSim (actually QuestaSim) is the VHDL simulator available on Chalmers computers. There is an introduction to modelsim available.

To use QuestaSim you have to use the bash shell, which you normally do. First setup the environment with

source /chalmers/sw/sup/cse/courses/TDA956

(If you get errors like "declare: Command not found.", try running bash before.) Then start QuestaSim using

vsim

If you have a PC with Windows, you can use the free student version of ModelSim available from Mentor Graphics. This should be sufficient as we are only doing small examples. (Xilinx used to distribute a heftier version of ModelSim, but they stopped doing so late in 2010.)

There are also various other free simulators that can be downloaded for Linux...

JasperGold

Jasper Gold is a commercial formal verification tool from Jasper Design Automation. There is a short introduction to the tool.

To use JasperGold you have to use the bash shell, which you normally do. First setup the environment with

source /chalmers/sw/sup/cse/courses/TDA956

(If you get errors like "declare: Command not found.", try running bash before.) Then start Jasper Gold using

jg

The Help tab in the tools bar isn't working, but you can use acroread to read the manuals installed in

/chalmers/sw/sup/jaspergold/7.1p003/jaspergold_7.1p003/doc

Chalmers has 30 licenses that are available until 30 May 2011 to students who are registered on this course (technically, to members of the unix group jasper_sw; you can check with the command id which groups you belong to). We will use JasperGold only for formal verification of very small blocks. To get an idea of how JasperGold is used in reality, you might like to look at their demo aimed at potential customers on Demos on Demand. (I don't know if Demos on Demand allows students to join, but I hope so! There are all kinds of interesting video demos there, about many different aspects of hardware design and verification.)

Lava

Lava is the circuit description language we use in the second half of the course. Since Lava essentially is a library for writing circuit descriptions in Haskell, it can be used on any computer where the Haskell Platform is installed.

The Haskell Platform is installed on the Linux computers at Chalmers, but the Lava libraries are not. You can download and install them in your own account by doing

cabal update
cabal install chalmers-lava2000

Next, you should set up the connections to the verification tools by doing the following (in bash):

wget http://www.cse.chalmers.se/edu/course/TDA956/Tools/setup_lava.sh
chmod u+x setup_lava.sh
source setup_lava.sh

You can install Lava using cabal on your own computer too, if you install the Haskell Platform first. This should work on Mac & Linux. (Lava doesn't work perfectly on Windows in how it connects to external tools like SMV, see below. There are workarounds, so installing on Windows is still worthwhile.)

Once you have Lava installed, have a look at Introduction to the Lava system to get started.

The Lava system can also call external tools to formally verify properties of Lava circuits. We will use SMV for this, and the SAT solver Satzoo is also available on the Chalmers Linux compueters (once you have done the above setup).

SMV

Cadence SMV is a CTL model checker (originally from CMU), that can be used to verify properties of Lava circuits.

Using SMV on your own computer (works for Linux and hopefully also Mac):

You can get Cadence SMV from this download page at Cadence. You need to register to get download and installation instructions. You also need to tell Lava where to find SMV, with something like export Lava2000_SMV=smv (for bash) or setenv Lava2000_SMV smv (for tsch). You will also need to correct permission on a script file in the Chalmers Lava package with chmod +x $HOME/.cabal/share/chalmers-lava2000-1.1.2/Scripts/smv.wrapper (see the setup_lava.sh file mentioned above).

Using Lava with SMV on your Windows PC works less well as the Lava implementation of system calls is Linux specific. However, it can be helpful to use the following file, WinSmv.hs, which solves some of the problems and allows you to use Lava and SMV on your Windows PC. It is not a slick connection to SMV, but allows you to produce input that can be loaded manually into the Windows version of SMV. This works quite nicely as it allows you to see the SMV input and also to see counter-examples if your property is false. To use this hack, import WinSmv.hs in your example file and replace calls of smv with calls of winsmv. Then, you will get a file ciruit.smv in the Verify directory, and this can be opened from the SMV GUI. If you're a Windows hacker who knows how to make this work completely, do let us know!