Retrascope

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