Project

General

Profile

Actions

Command Line Options

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

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

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

This output shows four main categories of 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:

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

while on Windows:

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

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 standard + no function calls, no 'Z' or 'X' values.
For Verilog - satisfies IEEE 1364-2005 standard.

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 graphical format, the Retrascope should be run with the following options (for Verilog design called example.v):

--target efsm-graphml example.v
Here is the list of all target options of Retrascope:
Name Description
assertion Assertion model
cfg Control flow graph model
cfg-graphml Control flow graph model that is saved in the GraphML 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 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 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

Engines

As it is described above, the tool includes engines for source files & models elaboration.
Here is the list of all engines of 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 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 format
gadd-efsm-transformer Transformer of GADD model to EFSM model
efsm-graphml-printer Printer of EFSM model to GraphML format
efsm-fate-test-generator The FATE 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

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

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

Logging

By default, 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 --log option.
The default logging level is INFO. It is possible to change it by means of the --log-level option. The acceptable values are ERROR, WARNING, INFO, DEBUG.

SMT solver debug mode

By default, Fortress do not store the *.smt2 files through which it communicates with SMT solver. It can be enabled by setting --solver-debug option.

Updated by Sergey Smolov 5 months ago · 64 revisions