Project

General

Profile

Retrascope 1.1.1 released

Retrascope 1.1.1 has been released.
Added by Sergey Smolov 5 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


Comments