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/jaspergold-6.1/setup

and then start QuestaSim using

vsim

If you have a PC with Windows, you can use the free version of ModelSim available from Xilinx.

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

Jasper Gold

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

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

source /chalmers/sw/sup/jaspergold-6.1/setup

and 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-6.1/jaspergold_6.1p001.1/doc

Chalmers has 20 licenses that are available until 30 May 2011 to students who are registered to this cource (technically, to members of the unix group jasper_sw, you can check with the command id which groups you belong to).

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

You can do that on your on computer too, if you install the Haskell Platform first. It should work on Mac, Windows & Linux.

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.

SMV

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 on Mac and Linux, maybe Windows too?):

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, but something like export Lava2000_SMV=smv (for bash) or setenv Lava2000_SMV smv (for tsch) should be enough.

Using SMV on the Linux computers at Chalmers:

Emil Axelsson has installed a copy of SMV. To use his copy, download this setup_smv.sh (for bash) and do

source setup_smv.sh

to setup the environment so that Lava can find smv. (Note: the last line in setup_smv.sh is there to work around a permission bug in the chalmers-lava2000 package, and assumes that it has been installed in your account as shown in the Lava section above.)