Retrascope

h1. Command Line Options

{{toc}}

The tool can be run by using  scripts (@retrascope.sh@ for Unix-like OS, @retrascope.bat@ for Window-like OS).

In this document the command line interface for "Retrascope":http://forge.ispras.ru/projects/retrascope is described.

By default, the tool is run with "--help" option. Here is an output of the tool that is run with "--help" option:

<pre>

usage: files [options]

    --check                   Check if all the dependencies are installed

                              properly

    --engine <arg>            Set a subset of engines

    --help                    Show this message

    --log <arg>               Set a log file

    --log-level <arg>         Set a log level

    --solver-debug            Set debug mode for SMT solver

    --target <arg>            Set a target entity

    --tool-debug-file <arg>   Set debug mode and save info to debug log file

    --version                 Print the tool version

</pre>

This output shows four main categories of "Retrascope":http://forge.ispras.ru/projects/retrascope command line options: source files, engines, logging mode and targets.

Options can be put into command line in an arbitrary order. 

Options can have multi-values i.e. sequences of values, separated by system-dependent symbols. For example, for running the tool on multiple Verilog files (@file1.v@, @file2.v@, @file3.v@) on *nix OS, do the following:

<pre>

--target cfg file1.v:file2.v:file3.v

</pre>

while on Windows:

<pre>

--target cfg file1.v;file2.v;file3.v

</pre>

h2. Source files

This option keeps paths to files that contain source code of hardware modules. The tool elaborates hardware descriptions written in synthesizable subsets of VHDL and Verilog. For the current ( *1.1.2* ) version of the tool it is possible to elaborate the source code when it satisfies some limitations: 

For VHDL - satisfies "IEEE 1076-2008":https://standards.ieee.org/standard/1076-2008.html standard + no function calls, no 'Z' or 'X' values.

For Verilog - satisfies "IEEE 1364-2005":https://standards.ieee.org/standard/1364-2005.html standard.

h2. Targets

Retrascope operates with data representations, so called *entities*. One kind of these entities called "source files" was described in the previous section and for it's elaboration the default tool components (called HDL parsers) are used.

Other entities may be treated as equivalent transformations of source code, or as data that can be extracted from source code (for example, knowledge about module interfaces) or generated (unit-level HDL testbenches).

To select the entity the user wants to get as result, the "target" option is needed to be initialized. For example, to get the EFSM (Extended Finite State Machine) that is stored into "GraphML":http://graphml.graphdrawing.org graphical format, the "Retrascope":http://forge.ispras.ru/projects/retrascope should be run with the following options (for Verilog design called example.v):

<pre>

--target efsm-graphml example.v

</pre>

Here is the list of all target options of "Retrascope":http://forge.ispras.ru/projects/retrascope:

|*Name*|*Description*|

|assertion|Assertion model|

|cfg|Control flow graph model|

|cfg-graphml|Control flow graph model that is saved in the "GraphML":http://graphml.graphdrawing.org file|

|cfginterface|Interface (input and output signals) of control flow graph model|

|gadd|Guarded Actions Decision Diagram (GADD) model|

|gadd-graphml|GADD model that is stored in the "GraphML":http://graphml.graphdrawing.org file|

|conflicts|Conflict model|

|conflicts-xml|Conflict model that is stored in the XML file|

|efsm|Extended finite state machine (EFSM) model|

|efsm-graphml|EFSM model that is stored in the "GraphML":http://graphml.graphdrawing.org file|

|hldd|High-level decision diagram (HLDD) model|

|smv|HLDD model stored in the SMV file|

|smv-launch|SMV file execution by the model checker|

|vhdl-testbench|VHDL testbench|

|verilog-testbench|Verilog testbench|

h2. Engines

As it is described above, the tool includes engines for source files & models elaboration.

Here is the list of all engines of "Retrascope":http://forge.ispras.ru/projects/retrascope:

|*Name*|*Description*|

|verilog-parser|Parser of hardware modules descriptions written in Verilog|

|vhdl-parser|Parser of hardware modules descriptions written in VHDL|

|cfg-graphml-printer|Printer of CFG model into "GraphML":http://graphml.graphdrawing.org format|

|cfg-gadd-transformer|Transformer of CFG model to GADD model|

|cfg-cfginterface-extractor|Extractor of interface signals from CFG model|

|cfg-random-test-generator|Random test generator for CFG model|

|gadd-graphml-printer|Printer of GADD model to "GraphML":http://graphml.graphdrawing.org format|

|gadd-efsm-transformer|Transformer of GADD model to EFSM model|

|efsm-graphml-printer|Printer of EFSM model to "GraphML":http://graphml.graphdrawing.org format|

|efsm-fate-test-generator|The "FATE":http://link.springer.com/article/10.1007%2Fs10836-011-5209-8 test generator from EFSM model|

|efsm-test-generator| Generator of tests from EFSM model|

|efsm-transition-assertion-extractor| Extractor of EFSM transition assertions|

|efsm-conflict-extractor|Extractor of conflict model from EFSM model|

|conflict-xml-printer|Printer of conflict model into XML format|

|gadd-hldd-transformer|Transformer of GADD model into HLDD model or invariant formula|

|hldd-smv-printer|Prints the HLDD model into SMV format|

|hldd-property-smv-printer|Prints the HLDD model and the generated EFSM-based properties into SMV format|

|hldd-spec-smv-printer|Prints the HLDD model and the user-specified properties into SMV format|

|hldd-usedef-smv-printer|Prints the HLDD model and the generated conflict-based properties into SMV format|

|smv-modelchecker-launcher|Executes a SMV file by the model checker|

|smv-test-parser|Parser of tests from the model checker output|

|test-xml-printer|Printer of tests into XML format|

|xml-test-parser|Parser of XML format files keeping the tests|

|test-vhdl-testbench-printer|Creates VHDL testbenches on the basis of an HDL source code and generated tests|

|test-verilog-testbench-printer|Creates Verilog testbenches on the basis of an HDL source code and generated tests|

h3. Common options

Some options are common for all the tool engines. Here they are:

|*Option name*|*Description*|*Acceptable value*|

|printer-style|Set a printer style|VERILOG/VHDL|

h3. Engine-specific options

Some engines have individual command line options. Here is the list of all engine-specific options:

|*Engine name*|*Option*|*Description*|*Acceptable value*|*Default value*|

|<any>|disable-backends|Disables all the backends (optimizations) that names are specified|path separator separated names of backends (run "--disable-backends help" for more details)||

|<any>|no-backends|Disables all the backends (optimizations) for the engine|||

|verilog-parser, vhdl-parser|module-name|Toplevel module names|Names of top level HDL modules|path separator separated list of names for more than one input files; file name for only input file|

|verilog-parser, vhdl-parser|first-file-module|Get top level module name from first HDL file in a list|||

|verilog-parser|include-path|Path to find included files|Any existing file system path|<none>|

|cfg-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|cfg-model.graphml|

|cfg-random-test-generator|test-len|Length of test sequence to be generated.|Integer number that is greater than zero|<none>|

|cfg-random-test-generator|test-seed|Random ssed value for test generation.|Integer number|0|

|cfg-random-test-generator|clk-name|Name of clock signal|Any string value|clk|

|cfg-random-test-generator|clk-lvl|Active level of clock signal|Integer number (supposed 1 or 0)|1|

|cfg-random-test-generator|rst-name|Name of reset signal|Any string value|rst|

|cfg-random-test-generator|rst-lvl|Active level of reset signal|Integer number (supposed 1 or 0)|1|

|cfg-random-test-generator|rst-delay|Reset signal delay|Integer number that is greater than 0|1|

|cfg-random-test-generator|input-values|Input signals and their possible values.|list of "name=[min,max,radix]" expressions|<none>|

|cfg-gadd-transformer|clk-name|Name of clock variable.|String name of target module variable that is treated as clock|<none>|

|gadd-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|gadd-model.graphml|

|gadd-efsm-transformer|state-vars|Names of state-like variables|Any string name or names separated by system separators|<none>|

|efsm-graphml-printer|detailed|Print EFSM model in a detailed way|When enabled, the engine prints EFSM transition guards and actions|disabled|

|efsm-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|efsm-model.graphml|

|efsm-fate-test-generator|sequence-length|Amount of vectors in one randomly generated sequence|Any integer (including zero)|a total amount of states|

|efsm-fate-test-generator|sequences-number|Amount of sequences in a randomly generated fragment of a test|Any integer (including zero)|A ratio of a total amount of transitions to a total amount of states (rounded to an integer)|

|efsm-fate-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|

|efsm-fate-plus-test-generator|sequence-length|Amount of vectors in one randomly generated sequence|Any integer (including zero)|a total amount of states|

|efsm-fate-plus-test-generator|sequences-number|Amount of sequences in a randomly generated fragment of a test|Any integer (including zero)|A ratio of a total amount of transitions to a total amount of states (rounded to an integer)|

|efsm-fate-plus-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|

|efsm-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|

|efsm-conflict-extractor|search-type|Type of search performed on an extended finite state machine|BFS (Breadth-First Search) or DFS (Depth-First Search)|BFS|

|efsm-conflict-extractor|search-depth|Depth of search performed on an extended finite state machine|Any integer which is greater than zero|10|

|conflict-xml-printer|output-file|Output XML file name|Any string name for file that is acceptable by OS|conflicts.xml|

|gadd-hldd-transformer|formula-based|Transform a GADD into an invariant|||

|gadd-hldd-transformer|collect-usedef|Collect variables' defines/uses|||

|gadd-hldd-transformer|delete-unused|If any variable is never used, remove it from the resulting model|||

|hldd-property-smv-printer|check-method|Model checking method|ltl-bmc (bounded LTL), ltl-msat (bounded LTL using MathSat, nuXmv only), psl-bmc (bounded PSL), ctl-bdd (symbolic CTL), psl-bdd (symbolic PSL)|ltl-bmc|

|hldd-smv-printer / hldd-property-smv-printer / hldd-spec-smv-printer / hldd-usedef-smv-printer|smv-file|Output SMV file name|Any string name for file that is acceptable by OS|model.smv|

|hldd-spec-smv-printer|spec-file|User-defined file with specifications for model checking|Any string name for file that is acceptable by OS||

|smv-modelchecker-launcher|check-method|Model checking method|ltl-bmc (bounded LTL), ltl-msat (bounded LTL using MathSat, nuXmv only), psl-bmc (bounded PSL), ctl-bdd (symbolic CTL), psl-bdd (symbolic PSL)|ltl-bmc|

|smv-modelchecker-launcher|use-nusmv|Use NuSMV model checker instead of nuXmv|||

|smv-modelchecker-launcher|command-file|Specifies a command file for nuXmv|Either a relative or an absolute path to a file|Command file is generated using the src/main/resources/SmvCommandFile.stg template|

|smv-modelchecker-launcher|smv-verbosity|Sets the verbosity level of the model checker|Any integer which is greater or equals zero|0|

|test-xml-printer|file-name|Output XML file name|Any string name for file that is acceptable by OS|test.xml|

|test-vhdl-testbench-printer|testbench-dir|A directory where testbenches are saved|Either a relative or an absolute path to a directory. The %%MODULE_NAME%% placeholder is replaced by a processed design's name|testbenches/%MODULE_NAME%|

|test-vhdl-testbench-printer|overwrite|Overwrite target files if they already exist|||

|test-verilog-testbench-printer|testbench-dir|A directory where testbenches are saved|Either a relative or an absolute path to a directory. The %%MODULE_NAME%% placeholder is replaced by a processed design's name|testbenches/%MODULE_NAME%|

|test-verilog-testbench-printer|overwrite|Overwrite target files if they already exist|||

h2. Logging

By default, "Retrascope":http://forge.ispras.ru/projects/retrascope prints it's output to the standard error stream. It is also possible to redirect the tool output to the specified file by using <code>--log</code> option.

The default logging level is <code>INFO</code>. It is possible to change it by means of the <code>--log-level</code> option. The acceptable values are <code>ERROR</code>, <code>WARNING</code>, <code>INFO</code>, <code>DEBUG</code>.

h2. SMT solver debug mode

By default, "Fortress":https://forge.ispras.ru/projects/solver-api do not store the *.smt2 files through which it communicates with SMT solver. It can be enabled by setting <code>--solver-debug</code> option.