Project

General

Profile

News

Retrascope 1.1.2 released

Added by Sergey Smolov 2 months ago

The new release includes the following changes:

  • CFG-to-GraphML printer: mark branch values with italic;
  • CFG-to-GraphML printer: use dotted arrows for hierarchy dependencies;
  • Dependencies: does not use commons-lang library;
  • Tool: bug fixes and general improvements.

The list of resolved issues is available here

The tool can be downloaded from here

Retrascope 1.1.1 released

Added by Sergey Smolov 4 months ago

The new release includes the following changes:
  • Assertion: renamed to Property;
  • CFG Model: CFG model processes do not have their own internal variables: variable space is flattened at parent module's level;
  • CFG-to-GADD transformer: backend that implements clock detection is moved here;
  • CFG-to-GADD transformer: cmdline option that specifies clock variable;
  • CFG-to-GADD transformer: elaborate ranged assignments for bit vector target variables;
  • CFG-to-GADD transformer: one more auxiliary path in GADD model for terminal endings;
  • CFG-to-GADD transformer: reuse variables' versions upon CGAA model building;
  • CFG-to-GADD transformer: support for designs that assign to variable more than once;
  • CGAA model: renamed to GADD;
  • Engines: '--no-backends' cmdline option;
  • Engines: new cgaa-assert-extractor engine that extracts 'is-def' and 'is-use' constraints for every variable of every process of the design;
  • Engines: debug output file for engines and their back-ends;
  • Engines: enable\disable backend option by name for all engines;
  • HDL Parser: init_process backend that transforms initial blocks;
  • Models: support for 'BVEXTRACT(x y (SELECT z w))' constructions in left hand sides of assignments;
  • Model Checker Launcher: nuXmv 1.1.1 is in use;
  • Model Checker Launcher: pass Retrascope debug option to the model checker as well;
  • Model Checker Launcher: pass model checker error msg to the Retrascope output;
  • Refactoring: Range class is moved to Castle library;
  • Refactoring: RetrascopeException.makeException -> RetrascopeException.exception;
  • Refactoring: use StringTemplate facilities to generate HDL testbenches;
  • SAT Solver wrapper: z3 4.7.1 is in use;
  • Test suite: check variables\switches\basic blocks number at HDL parser test cases;
  • Test suite: jUnit test cases for CFG-GADD transformer that check path number;
  • Test suite: separate jUnit test cases for EfsmGraphMlPrinter engine;
  • Tool: bug fixes and general improvements;
  • Tool: renamed from "HDL Retrascope" to "Retrascope";
  • Utility: 'BVEXTRACT( ... BVEXTRACT (j i x))' expression transformation rule to the tool ruleset;
  • Utility: check BVEXTRACT operation's parameter order;
  • Utility: substitute SMT-LIB variables those names are equal to builtin commands;
  • VHDL parser: VHDL record support (non-aggregate case);
  • VHDL parser: ZamiaCAD 0.11.3 is in use.

The list of resolved issues can be found here

The tool can be downloaded from here

Retrascope 1.0.1 released

Added by Sergey Smolov about 2 years ago

The new release contains the following changes:

  • CGAA model: phase variable based representation;
  • CGAA model: process as a collection of sub-paths;
  • CGAA-to-EFSM transformer: cmdline parameter for EFSM state number limit;
  • EFSM model: phase variable based representation;
  • HLDD model: phase variable based representation support;
  • HLDD-based test generator: phase variable based representation support;
  • Tests: miniMIPS & Plasma projects are partially in use;
  • Tool Functions: Bug fixes & general improvements;
  • Utilities: separately solve independent sub-expressions of AND expression;
  • VHDL parser: flatten module instances;
  • VHDL parser: enum support;
  • VHDL parser: support for 'others' attr upon bitvector\array initialization;
  • VHDL parser: limited support for functions (BV_INC6);
  • VHDL\Verilog parsers: backend that merges "neighbour ranged" sequential "if" statements;
  • VHDL\Verilog parsers: backend that merges empty event-free cases.

The list of resolved issues can be found here

The tool can be downloaded from here

HDL Retrascope 0.2.2 released

Added by Sergey Smolov about 3 years ago

The new release contains the following changes:

  • Verilog testbench printer;
  • EfsmSimulatorUtils: utility methods for EFSM state/transition coverage printing;
  • VHDL/Verilog: support for non-0 starting bit vectors;
  • Verilog parser: merge 'assign' processes in CFG model if it is possible;
  • CGAA-to-EFSM: EFSM stabilization upon possible non-determinism;
  • Print tool execution time in command line mode;
  • HLDD-to-SMV printer that does not use assertions;
  • Bug fixes & general improvements.

The list of resolved issues can be found at the following link

The tool can be downloaded from here

HDL Retrascope was presented at DATE 2016

Added by Sergey Smolov over 3 years ago

The HDL Retrascope toolkit was presented at the Univeristy Booth of the Design, Automation & Test in Europe conference. The conference took place on March 14-18 in Dresden, Germany.
The DATE conference addresses all aspects of research into technologies for electronic and embedded system engineering. It covers the design process, test, and automation tools for electronics ranging from integrated circuits to distributed embedded systems. Read more...

HDL Retrascope 0.2.1 released

Added by Sergey Smolov over 3 years ago

The new release contains the following changes:

- High-Level Decision Diagram (HLDD) model;
- Printer engine for HLDD models to NuSMV model checker format;
- Wrapper engine around NuSMV model checker that is able to transmit tool output to other engines;
- Transformer engine from GADD model to HLDD model;
- Parser engine for NuSMV logs that produces tests;
- Hierarchical (at statement and variable declaration levels) CFG\EFSM models;
- Internal SAT-solver for trivial constraints that is used prior to the external one;
- Assertion (specification) hierarchical model;
- EFSM-based transition assertion generator engine;
- GADD models now contain only concurrent (non-blocking) non-ranged assignments;
- Support for non-loop\non-recursion functions in VHDL\Verilog designs;
- Descriptors for HDL variables;
- HDL parser optimization (sequential switch statements grouping);
- Random test generator for CFG model ;
- Several bug fixes and general improvements were made.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

HDL Retrascope 0.1.3 released

Added by Sergey Smolov over 4 years ago

The new release includes the following changes:

  • Support for process variable declarations;
  • Support for VHDL testbench generation (tests cover all the EFSM transitions);
  • Enhanced EFSM test generation scheme has been implemented (pre-init state + init action);
  • Exception subsystem has been implemented;
  • The "tool-debug-file" command line option has been implemented;
  • A number of bugs was fixed.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

HDL Retrascope was presented at DATE 2015

Added by Sergey Smolov over 4 years ago

The HDL Retrascope tool was presented at the University Booth of the Design, Automation & Test in Europe (DATE). The conference took place on March 9-13 in Grenoble, France.

The DATE conference addresses all aspects of research into technologies for electronic and embedded system engineering. It covers the design process, test, and automation tools for electronics ranging from integrated circuits to distributed embedded systems. Read more...

HDL Retrascope v0.1.2 released

Added by Sergey Smolov over 4 years ago

The new release includes the following changes:

  • Support for loops in VHDL/Verilog designs;
  • Support for wait-expressions in VHDL/Verilog designs;
  • Support for hierarchical (i.e. having sub-modules) VHDL/Verilog designs;
  • Support for concurrent (non-blocking) statements in VHDL/Verilog designs;
  • New command line scripts for Windows & Unix;
  • New heuristic for initial EFSM state & reset signal detection;
  • New fully-functional *.tar.gz distribution format;
  • A number of bugs was fixed.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

HDL Retrascope v0.1.1 released

Added by Sergey Smolov almost 5 years ago

We are happy to announce the first build of the HDL Retrascope toolkit.

HDL Retrascope is a toolkit for Reverse Engineering and TRAnsformation of digital hardware designs described in such HDLs (hardware description languages) as Verilog и VHDL. The toolkit allows analyzing HDL descriptions, reconstructing the underlying models (extended finite state machines, EFSMs) and using the derived models for test generation, property checking and other tasks. HDL Retrascope is organized as an extendable framework with the ability to add new types of models as well as tools for their analysis and transformation. The primary application domain of the toolkit is functional verification of hardware at the unit level.

To reconstruct EFSM models and generate tests for them, Retrascope requires the SMT-solver be installed. See Installation Guide for more information.

In the 0.1.1 build the following features have been implemented:

- Support for VHDL/Verilog little-size designs (without iteration loops/functions/sub-modules);
- Support for control flow graph (CFG) construction;
- Support for CFG visualization in GraphML format;
- Support for interface signals extraction from CFG;
- Support for guarded actions decision diagram (GADD) construction;
- Support for GADD visualization in GraphML format;
- Support for extended finite state machine (EFSM) extraction;
- Support for EFSM visualization in GraphML format;
- Support for read/write conflicts extraction from EFSM;
- Support for conflicts saving into XML format;
- Support for test sequences generation for EFSM;
- Support for test sequences saving into VHDL testbenches/XML format.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

You are welcome to report bugs and leave your feedback at the main project site: http://forge.ispras.ru/projects/retrascope

Merry Christmas and Happy New Year!

(1-10/12)

Also available in: Atom