Retrascope: static analysis of hdl descriptions

Retrascope: static analysis of hdl descriptions

Retrascope is a functional verification toolkit for digital hardware designs. Retrascope provides automated engines for code analysis, formal model extraction and functional test generation. The toolkit accepts digital hardware module descriptions as inputs, written on the synthesizable subset of Verilog and VHDL languages, as well as their behavioral specifications.

Features and advantages

Retrascope is an open source toolkit for functional verification of digital hardware modules. The toolkit implements formal model extraction and analysis methods and functional test generation methods. A component-based architecture of Retrascope allows developing hybrid formal model verification techniques by combining various analysis methods. Retrascope is available at https://forge.ispras.ru/projects/retrascope.

Retrascope provides:

• Formal model extraction from source code:
  • control flow graph;
  • guarded actions decision diagram;
  • high-level decision diagram;
  • extended finite state machine.
• Functional test generation:
  • random tests;
  • dead code detection;
  • typical read-write error detection;
  • user-defined property checking.
• Formal model analysis (model checking) that verifies specification conformance via:
  • PSL;
  • SystemVerilog Assertions.
• Graphical user interface based on Eclipse IDE (command line interface is also available):
  • running the tool with specified parameters;
  • model visualization (Zest, GraphML).
• Open source (Apache License Version 2.0).
• Extensibility at the source code level:
  • new models;
  • new engines for analysis and test generation.
• Open APIs and formats allow using various tools for analysis and verification:
  • SMT solvers via the SMT-LIB v2 language;
  • Model checkers via the SMV language;
  • Functional tests via Verilog/VHDL languages and the VCD format.

Who is Retrascope target audience?

• Companies working in the area of digital hardware design.
• Research groups in the field of digital hardware verification.

Retrascope deployment stories

Retrascope is at the research prototype stage with active development.

System requirements

Windows or GNU/Linux-based OS, Java Runtime Environment 8.

Retrascope workflow

Developer/Participant

Software Engineering