Project

General

Profile

Command Line Options » History » Version 61

Sergey Smolov, 02/19/2020 05:31 PM

1 1 Sergey Smolov
h1. Command Line Options
2
3 2 Sergey Smolov
{{toc}}
4
5 55 Sergey Smolov
The tool can be run by using  scripts (@retrascope.sh@ for Unix-like OS, @retrascope.bat@ for Window-like OS).
6 1 Sergey Smolov
7 44 Sergey Smolov
In this document the command line interface for "Retrascope":http://forge.ispras.ru/projects/retrascope is described.
8 23 Sergey Smolov
9
By default, the tool is run with "--help" option. Here is an output of the tool that is run with "--help" option:
10 1 Sergey Smolov
11
<pre>
12 47 Sergey Smolov
usage: files [options]
13 60 Sergey Smolov
    --check                   Check if all the dependencies are installed
14
                              properly
15 29 Sergey Smolov
    --engine <arg>            Set a subset of engines
16
    --help                    Show this message
17
    --log <arg>               Set a log file
18
    --log-level <arg>         Set a log level
19
    --solver-debug            Set debug mode for SMT solver
20
    --target <arg>            Set a target entity
21
    --tool-debug-file <arg>   Set debug mode and save info to debug log file
22 60 Sergey Smolov
    --version                 Print the tool version
23 1 Sergey Smolov
</pre>
24
25 44 Sergey Smolov
This output shows four main categories of "Retrascope":http://forge.ispras.ru/projects/retrascope command line options: source files, engines, logging mode and targets.
26 1 Sergey Smolov
Options can be put into command line in an arbitrary order. 
27
28 16 Sergey Smolov
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:
29
30
<pre>
31
--target cfg file1.v:file2.v:file3.v
32
</pre>
33
34
while on Windows:
35
36
<pre>
37
--target cfg file1.v;file2.v;file3.v
38
</pre>
39
40
41 1 Sergey Smolov
h2. Source files
42
43
This option keeps paths to files that contain source code of hardware modules.
44
45 44 Sergey Smolov
The "Retrascope":http://forge.ispras.ru/projects/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. 
46 1 Sergey Smolov
47 46 Sergey Smolov
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.
48 1 Sergey Smolov
For Verilog - similar to VHDL.
49
50 44 Sergey Smolov
If these limitations are satisfied there is a high probability that "Retrascope":http://forge.ispras.ru/projects/retrascope will be able to elaborate your design:-) Otherwise an exception will occur.
51
It is possible to run the "Retrascope":http://forge.ispras.ru/projects/retrascope both on several VHDL and Verilog designs. In such case a composite inner representation based on Control FLow Graph model will be constructed.
52 46 Sergey Smolov
To transform VHDL design into Control Flow Graph model you need to run "Retrascope":http://forge.ispras.ru/projects/retrascope with the following parameters:
53 1 Sergey Smolov
54 44 Sergey Smolov
<pre>
55 49 Sergey Smolov
--target cfg --module-name module_name /path/to/file/file.vhd
56 1 Sergey Smolov
</pre>
57
58 49 Sergey Smolov
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):
59 3 Sergey Smolov
60
<pre>
61
entity hello_world is
62
end;
63
 
64
architecture hello_world_arc of hello_world is
65
begin
66 1 Sergey Smolov
  stimulus : process
67 3 Sergey Smolov
  begin
68
    assert false report "Hello World"
69 1 Sergey Smolov
    severity note;
70 4 Sergey Smolov
  end process stimulus;
71 3 Sergey Smolov
end hello_world_arc;
72
</pre>
73
74
we need to run "Retrascope":http://forge.ispras.ru/projects/retrascope with the following parameters:
75 44 Sergey Smolov
76 3 Sergey Smolov
<pre>
77 49 Sergey Smolov
--target cfg --module-name hello_world /path/to/file/hello.vhd
78 3 Sergey Smolov
</pre>
79 2 Sergey Smolov
80 49 Sergey Smolov
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.
81 30 Sergey Smolov
82 2 Sergey Smolov
h2. Targets
83
84 46 Sergey Smolov
From the tool point of view, the "Retrascope":http://forge.ispras.ru/projects/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.
85 5 Sergey Smolov
86 57 Sergey Smolov
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). Entities are used by other Retrascope's components that are called "engines".
87 5 Sergey Smolov
88 44 Sergey Smolov
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):
89 5 Sergey Smolov
90
<pre>
91
--target efsm-graphml example.v
92
</pre>
93
94 44 Sergey Smolov
Here is the list of all target options of "Retrascope":http://forge.ispras.ru/projects/retrascope:
95 6 Sergey Smolov
|*Name*|*Description*|
96 34 Sergey Smolov
|assertion|Assertion model|
97 6 Sergey Smolov
|cfg|Control flow graph model|
98 8 Sergey Smolov
|cfg-graphml|Control flow graph model that is saved in the "GraphML":http://graphml.graphdrawing.org file|
99 6 Sergey Smolov
|cfginterface|Interface (input and output signals) of control flow graph model|
100
|cgaa|Clocked guarded atomic actions model|
101 8 Sergey Smolov
|cgaa-graphml|Clocked guarded atomic actions model that is saved in the "GraphML":http://graphml.graphdrawing.org file|
102 35 Mikhail Lebedev
|conflicts|Conflict model|
103
|conflicts-xml|Conflict model that is saved in the XML file|
104 6 Sergey Smolov
|efsm|Extended finite state machine model|
105 8 Sergey Smolov
|efsm-graphml|Extended finite state machine model that is saved in the "GraphML":http://graphml.graphdrawing.org file|
106 37 Mikhail Lebedev
|hldd|High-level decision diagram (HLDD) model|
107 42 Mikhail Lebedev
|smv|HLDD model stored in the SMV file|
108
|smv-launch|SMV file execution by the model checker|
109 25 Igor Melnichenko
|vhdl-testbench|VHDL testbench|
110 43 Sergey Smolov
|verilog-testbench|Verilog testbench|
111 1 Sergey Smolov
112
h2. Engines
113
114 44 Sergey Smolov
As it is described above, the "Retrascope":http://forge.ispras.ru/projects/retrascope consists of components called "engines" for source files & models elaboration. The "Retrascope":http://forge.ispras.ru/projects/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.
115 8 Sergey Smolov
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".
116 44 Sergey Smolov
Here is the list of all engines of "Retrascope":http://forge.ispras.ru/projects/retrascope:
117 8 Sergey Smolov
|*Name*|*Description*|
118
|verilog-parser|Parser of hardware modules descriptions written in Verilog|
119
|vhdl-parser|Parser of hardware modules descriptions written in VHDL|
120
|cfg-graphml-printer|Printer of control flow graph model into "GraphML":http://graphml.graphdrawing.org format|
121
|cfg-cgaa-transformer|Transformer of control flow graph model into clocked guarded actions model|
122
|cfg-cfginterface-extractor|Extractor of interface signals of control flow graph model|
123 39 Sergey Smolov
|cfg-random-test-generator|Random test generator for control flow graph model|
124 8 Sergey Smolov
|cgaa-graphml-printer|Printer of clocked guarded atomic actions model into "GraphML":http://graphml.graphdrawing.org format|
125
|cgaa-efsm-transformer|Transformer of control flow graph model into extended finite state machine model|
126 37 Mikhail Lebedev
|cgaa-hldd-transformer|Transformer of control flow graph model into high-level decision diagram model|
127 8 Sergey Smolov
|efsm-graphml-printer|Printer of extended finite state machine model into "GraphML":http://graphml.graphdrawing.org format|
128
|efsm-fate-test-generator|The "FATE":http://link.springer.com/article/10.1007%2Fs10836-011-5209-8 test generator from extended finite state machine model|
129 1 Sergey Smolov
|efsm-test-generator| Generator of tests from extended finite state machine model|
130 36 Sergey Smolov
|efsm-transition-assertion-extractor| Extractor of EFSM transition assertions|
131 1 Sergey Smolov
|efsm-conflict-extractor|Extractor of conflict model from extended finite state machine|
132
|conflict-xml-printer|Printer of conflict model into XML format|
133 42 Mikhail Lebedev
|hldd-smv-printer|Prints the high-level decision diagram model into SMV format|
134
|smv-modelchecker-launcher|Executes a SMV file by the model checker|
135
|smv-test-parser|Parser of tests from the model checker output|
136 1 Sergey Smolov
|test-xml-printer|Printer of tests into XML format|
137
|xml-test-parser|Parser of XML format files keeping the tests|
138
|test-vhdl-testbench-printer|Creates VHDL testbenches on the basis of an HDL source code and generated tests|
139 26 Sergey Smolov
|test-verilog-testbench-printer|Creates Verilog testbenches on the basis of an HDL source code and generated tests|
140 43 Sergey Smolov
141 8 Sergey Smolov
142 43 Sergey Smolov
Some options are common for all the tool engines. Here they are:
143 14 Sergey Smolov
|*Option name*|*Description*|*Acceptable value*|
144
|printer-style|Set a printer style|VERILOG/VHDL|
145
146
Some engines have individual command line options. Here is the list of all engine-specific options:
147
148 1 Sergey Smolov
|*Engine name*|*Option*|*Description*|*Acceptable value*|*Default value*|
149 54 Sergey Smolov
|<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)||
150
|<any>|no-backends|Disables all the backends (optimizations) for the engine|||
151 51 Sergey Smolov
|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|
152 45 Sergey Smolov
|verilog-parser, vhdl-parser|first-file-module|Get top level module name from first HDL file in a list|||
153 53 Sergey Smolov
|verilog-parser|include-path|Path to find included files|Any existing file system path|<none>|
154 48 Sergey Smolov
|cfg-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|cfg-model.graphml|
155 39 Sergey Smolov
|cfg-random-test-generator|test-len|Length of test sequence to be generated.|Integer number that is greater than zero|<none>|
156 41 Sergey Smolov
|cfg-random-test-generator|test-seed|Random ssed value for test generation.|Integer number|0|
157 39 Sergey Smolov
|cfg-random-test-generator|clk-name|Name of clock signal|Any string value|clk|
158
|cfg-random-test-generator|clk-lvl|Active level of clock signal|Integer number (supposed 1 or 0)|1|
159
|cfg-random-test-generator|rst-name|Name of reset signal|Any string value|rst|
160
|cfg-random-test-generator|rst-lvl|Active level of reset signal|Integer number (supposed 1 or 0)|1|
161
|cfg-random-test-generator|rst-delay|Reset signal delay|Integer number that is greater than 0|1|
162 40 Sergey Smolov
|cfg-random-test-generator|input-values|Input signals and their possible values.|list of "name=[min,max,radix]" expressions|<none>|
163 52 Sergey Smolov
|cfg-cgaa-transformer|clk-name|Name of clock variable.|String name of target module variable that is treated as clock|<none>|
164 48 Sergey Smolov
|cgaa-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|cgaa-model.graphml|
165 39 Sergey Smolov
|cgaa-efsm-transformer|state-vars|Names of state-like variables|Any string name or names separated by system separators|<none>|
166 61 Sergey Smolov
|efsm-graphml-printer|detailed|Print EFSM model in a detailed way|When enabled, the engine prints EFSM transition guards and actions|disabled|
167 48 Sergey Smolov
|efsm-graphml-printer|graphml|Output GraphML file name|Any string name for file that is acceptable by OS|efsm-model.graphml|
168 18 Igor Melnichenko
|efsm-fate-test-generator|sequence-length|Amount of vectors in one randomly generated sequence|Any integer (including zero)|a total amount of states|
169
|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)|
170 1 Sergey Smolov
|efsm-fate-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|
171 43 Sergey Smolov
|efsm-fate-plus-test-generator|sequence-length|Amount of vectors in one randomly generated sequence|Any integer (including zero)|a total amount of states|
172
|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)|
173
|efsm-fate-plus-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|
174 35 Mikhail Lebedev
|efsm-test-generator|loop-limit|Loop iteration limit|Any integer which is greater than zero|1|
175 1 Sergey Smolov
|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|
176
|efsm-conflict-extractor|search-depth|Depth of search performed on an extended finite state machine|Any integer which is greater than zero|10|
177
|conflict-xml-printer|output-file|Output XML file name|Any string name for file that is acceptable by OS|conflicts.xml|
178
|hldd-smv-printer|output-file|Output SMV file name|Any string name for file that is acceptable by OS|model.smv|
179 42 Mikhail Lebedev
|hldd-smv-printer|check-method|Model checking method|bdd (for CTL) or bmc (for LTL)|bmc|
180
|smv-modelchecker-launcher|check-method|Model checking method|bdd (for CTL) or bmc (for LTL)|bmc|
181 59 Mikhail Lebedev
|smv-modelchecker-launcher|use-nusmv|Use NuSMV model checker instead of nuXmv|||
182
|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|
183
|smv-modelchecker-launcher|smv-verbosity|Sets the verbosity level of the model checker|Any integer which is greater or equals zero|0|
184 1 Sergey Smolov
|test-xml-printer|file-name|Output XML file name|Any string name for file that is acceptable by OS|test.xml|
185
|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%|
186 56 Sergey Smolov
|test-vhdl-testbench-printer|overwrite|Overwrite target files if they already exist|||
187 46 Sergey Smolov
|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%|
188 56 Sergey Smolov
|test-verilog-testbench-printer|overwrite|Overwrite target files if they already exist|||
189 15 Sergey Smolov
190 2 Sergey Smolov
h2. Logging
191
192 46 Sergey Smolov
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.
193 19 Igor Melnichenko
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>.
194 24 Sergey Smolov
195
h2. SMT solver debug mode
196
197 58 Sergey Smolov
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.