Hardware Description and Verification
AvailabilityThe 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 simulatorsModelSim (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
and then start QuestaSim using
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 GoldJasper 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
and then start Jasper Gold using
The Help tab in the tools bar isn't working, but you can use acroread to read the manuals installed in
Chalmers has 20 licenses that are available until 30 May 2011
to students who are registered to this cource (technically, to members of the
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
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.
SMVSMV is a CTL model checker (originally from CMU), that can be used to verify properties of Lava circuits.
|[ Home | News | Schedule | Literature | Assignments | Tools | Links | Course ]||TH, April 2010|