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 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, Ubuntu 12.04, Fedora 30). 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 containing a pre-installed version of Hades tool. The virtual machine can be run, e.g., in Virtual Box. 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 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.

CompAcc

CompAcc is an 8-bit processor based on an accumulator 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). Lecture Notes in Computer Science, vol 9520, pp. 605-614. Springer, Cham, 2015. ISBN 978-3-319-27339-6.
[4]
Lukas Charvat, Ales Smrcka, and Tomas Vojnar. Hades: Microprocessor Hazard Analysis via Formal Verification of Parameterized Systems. In: Proceedings of the Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2016). Electronic Proceedings in Theoretical Computer Science, vol 233, pp. 87-93. Open Publishing Association, 2016.

License

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