HADES (Hazard Detection System)

Hades et Cerberus III
  1. About
  2. Download
  3. Installation
  4. Usage
  5. Examples
  6. Contact
  7. Related Papers
  8. License

About

Hades is a verification tool, currently aimed at detection of RAW hazards in single pipelined microprocessors. It combines several approaches including data-flow analysis, static detection of possible hazards, and dynamic analysis using parameterised systems. As its input, the tool expects a processor described in the form of processor structure graph PSG (see [1] for details) using VAM file format.

Download

For successful installation, you will require:

Installation

Currently, installation is available only for Linux OS (tested on Fedora 20 and Ubuntu 12.04). Extract, configure, compile, and install SMT Solver, RTLManip, and ARTMC as usual. Check installation instructions of particular tool for further details. Please, make sure that binaries (z3, rtlmanip and ARTMC directory) are accessible in hades/bin directory or through PATH variable. The last step can be done by using script install.sh found in hades root directory as well.

Alternatively, you may download a virtual machine with Fedora 20 containing a pre-installed version of Hades tool. The virtual machine can be run, e.g., in Virtual Box. Enter username hades with password hades for login. The installation can then be found in directory ~/hades.

Usage

The simplest way to analyse a CPU written in VAM format is to use script analyze-vam.sh

  analyse-vam.sh <vam-file> <program counter>

  <vam-file>          A path to the VAM file without *.vam extension.
  <program counter>   A name of VAM variable representing the program counter
                      (use "v8" for example models).
  

When a flaw is found, the tool informs a user by error message with its description. Otherwise, the verified processor is absent of RAW hazards.

Examples

TinyCPU

TinyCPU is a small 8-bit processor ipcore (IP) with 3 pipeline stages developed mainly for testing of new verification methods. Examples below include several variants of this IP.

DLX5

DLX5 is a 5-staged 32-bit processor able to execute a subset of the instruction set of the DLX architecture.

Contact

If you have further questions, do not hesitate to contact authors (Lukas Charvat, Ales Smrcka, Tomas Vojnar).

Related Papers

[1]
Lukas Charvat, Ales Smrcka, and Tomas Vojnar. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. In: Proceedings of 15th International Workshop on Microprocessor Test and Verification (MTV'14). Austin, TX: IEEE Computer Society, 2014, s. 83-89. ISBN 978-1-4673-6858-2. DOI: 10.1109/MTV.2014.21.
[2]
Lukas Charvat, Ales Smrcka, and Tomas Vojnar. Using Formal Verification of Parameterized Systems in RAW Hazard Analysis in Microprocessors. Technical Report no. FIT-TR-2014-04. Brno, CZ: Brno University of Technology, 2014.
[3]
Lukas Charvat, Ales Smrcka, and Tomas Vojnar. Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the 15th International Conference on Computer Aided Systems Theory (EUROCAST 2015). Las Palmas de Grand Canaria: Universidad de Las Palmas de Gran Canaria, 2015, s. 193-194. ISBN 978-84-606-5438-4.

License

Hades tool can be freely copied, distributed and modified under the terms and conditions of GNU GPL v3.