Retrascope

• 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