Retrascope

This release publishes improvements that were made mostly before January 2022.

Since this time the development was actually stopped.

The new release includes the following changes:

• CFG-GADD-Transformer: '--no-phase' option to produce phase-free GADD;
• CFG-Model: general support of SVA properties;
• Distribution: self-made RTL models and demo scripts are added;
• Documentation: ChangeLog and README files are rewritten into `Markdown` format;
• EFSM-GraphML-Printer: `--detailed` option for EFSM detailed/limited printing;
• Tool: `--check` option to check if tool dependencies were installed properly;
• Tool: migration to JDK 11;
• Tool: `--version` option;
• VCD-Printer: a new engine to print test sequences into VCD format;
• Verilog-Parser: `--library-file` option for path to system tasks/functions file.

The complete list of resolved issues is available here

The binary distribution of the tool can be downloaded from here

Retrascope 1.1.* distribution packages have been re-uploaded to Files with the build base version having been set.

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

• 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

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

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

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...

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

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

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...