Command Line Options¶

• Table of contents
• Command Line Options
  • Source files
  • Targets
  • Engines
  • Logging
  • SMT solver debug mode

The tool can be run by using either scripts (retrascope.sh for Unix-like OS, retrascope.bat for Window-like OS) or Retrascope IDE plugin for Eclipse.

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

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 Retrascope can elaborate hardware descriptions written in synthesizable subsets of VHDL and Verilog. For current version of the tool it is possible to elaborate the source code when it satisfies some limitations.

For VHDL - no loop-cycles, no other modules' instantiations, no wait-constructions, no function calls, no 'Z' or 'X' values, code size is less than 1 KLOC.
For Verilog - similar to VHDL.

If these limitations are satisfied there is a high probability that Retrascope will be able to elaborate your design:-) Otherwise an exception will occur.
It is possible to run the Retrascope both on several VHDL and Verilog designs. In such case a composite inner representation based on Control FLow Graph model will be constructed.
To transform VHDL design into Control Flow Graph model you need to run Retrascope with the following parameters:

--target cfg --module-name module_name /path/to/file/file.vhd

where "cfg" encodes Control Flow Graph model as target, and "module-name" is a string name of the top-level module of the specified VHDL file. For example, to elaborate the following VHDL design (that is saved in the hello.vhd file):

entity hello_world is
end;

architecture hello_world_arc of hello_world is
begin
  stimulus : process
  begin
    assert false report "Hello World" 
    severity note;
  end process stimulus;
end hello_world_arc;

we need to run Retrascope with the following parameters:

--target cfg --module-name hello_world /path/to/file/hello.vhd

You may omit the "--module-name" option in the case you are going to elaborate a single VHDL module which name is the same as it's toplevel module name.

Targets¶

From the tool point of view, the Retrascope operates with 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, like knowledge about module interfaces) or constructed (like module-level tests). Every entity which representation is included into Retrascope is stronlge connected with the tool component called "engine".

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
cgaa	Clocked guarded atomic actions model
cgaa-graphml	Clocked guarded atomic actions model that is saved in the GraphML file
conflicts	Conflict model
conflicts-xml	Conflict model that is saved in the XML file
efsm	Extended finite state machine model
efsm-graphml	Extended finite state machine model that is saved 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 Retrascope consists of components called "engines" for source files & models elaboration. The Retrascope tool takes the target and constructs a sequence of engines called "toolchain" that reaches the specified target as a result. If the specified target is unreachable, the tool returns an error message.
When the specified target can be reached by several toolchains, the user can select the desired one by selecting engines with special option called "engine".
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 control flow graph model into GraphML format
cfg-cgaa-transformer	Transformer of control flow graph model into clocked guarded actions model
cfg-cfginterface-extractor	Extractor of interface signals of control flow graph model
cfg-random-test-generator	Random test generator for control flow graph model
cgaa-graphml-printer	Printer of clocked guarded atomic actions model into GraphML format
cgaa-efsm-transformer	Transformer of control flow graph model into extended finite state machine model
cgaa-hldd-transformer	Transformer of control flow graph model into high-level decision diagram model
efsm-graphml-printer	Printer of extended finite state machine model into GraphML format
efsm-fate-test-generator	The FATE test generator from extended finite state machine model
efsm-test-generator	Generator of tests from extended finite state machine model
efsm-transition-assertion-extractor	Extractor of EFSM transition assertions
efsm-conflict-extractor	Extractor of conflict model from extended finite state machine
conflict-xml-printer	Printer of conflict model into XML format
hldd-smv-printer	Prints the high-level decision diagram model 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

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

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

Engine name	Option	Description	Acceptable value	Default value
verilog-parser	include-path	Path to find included files	Any existing file system path	<none>
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	--disable-backends	Disables all the backends (optimizations) for the HDL parser that names are specified	path separator separated names of backends (run "--disable-backends help" for more details)
verilog-parser, vhdl-parser	no-backends	Disables all the backends (optimizations) for the HDL parser
verilog-parser, vhdl-parser	first-file-module	Get top level module name from first HDL file in a list
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>
cgaa-graphml-printer	graphml	Output GraphML file name	Any string name for file that is acceptable by OS	cgaa-model.graphml
cgaa-efsm-transformer	state-vars	Names of state-like variables	Any string name or names separated by system separators	<none>
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
hldd-smv-printer	output-file	Output SMV file name	Any string name for file that is acceptable by OS	model.smv
hldd-smv-printer	check-method	Model checking method	bdd (for CTL) or bmc (for LTL)	bmc
smv-modelchecker-launcher	check-method	Model checking method	bdd (for CTL) or bmc (for LTL)	bmc
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-existing	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-existing	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.