Project

General

Profile

News

Retrascope 1.1.2 released

Added by Sergey Smolov 10 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 12 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 almost 3 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 over 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 4 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 4 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 about 5 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 5 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 5 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

(1-10/13)

Also available in: Atom