- Table of contents
- Getting Started
Retrascope should be installed.
Command Line Interface¶
As it is described in Overview, Retrascope contains a number of data representations that are called entities and a number of active components that are called engines. When working with the tool through command line interface, valuable engines and\or entities are to be specified. To describe the approach, let's look at the map of all engines and entities at Retrascope:
Figure 1 : Engines & entities dependency graph
On the Fig. 1 engines are depicted as labeled edges, entities are depicted as labeled nodes. Entities that are represented by text files, are shown as grey rectangles. Entities, that are stored in memory, are shown as yellow circles. Edge and node labels store engine and entity identifiers respectively. Edge directions mean input (source) and output (destination) entities for engines.
At simple case, it is enough for the tool running to pass the desired entity or engine identifier as command line parameter. However, as it can be seen from Fig. 1, some engines require two or more inputs. For such engines (like
smv-test-parser, for example) merge points that are depicted by white circle nodes are introduced. Having such merge points in Retrascope engines\entities dependency graph, means that it is not enough to specify only the destination engine or entity. Tool parameters should be selected with the aim to describe the concrete path at the dependency graph.
For example, we would like to run the tool on VHDL module that is called
example.vhd with the aim to check properties that are extracted from it's internal EFSM model (
efsm-transition-property-extractor) by a VHDL testbench. Here is the module code:
entity example is port (input : in bit_vector(2 downto 1); output: out bit_vector(1 downto 0); clock: in bit); end example; architecture BEHAV of example is begin process(clock) begin if clock'event and clock='1' then if (input(2) = '1') then output <= "11"; end if; if (input(1) = '0') then output <= "01"; end if; end if; end process; end BEHAV;
On Windows, Retrascope should have at least the following arguments:
> retrascope.bat example.vhd --module-name example --target vhdl-testbench --engine vhdl-parser;efsm-transition-property-extractor
On Linux-based OS:
$ retrascope example.vhd --module-name example --target vhdl-testbench --engine vhdl-parser:efsm-transition-property-extractor
Next chapters of this guide describe main use cases of the Retrascope tool.
Model visualization¶Retrascope tool extracts the following categories of models from target HDL descriptions:
- Control Flow Graph (CFG)
- Guarded Actions Decision Diagram (GADD)
- High-Level Decision Diagram (HLDD)
- Extended Finite State Machine (EFSM)
$ ./retrascope example.vhd --module-name example --engine cfg-graphml-printer --graphml example-cfg.graphml
To convert the generated example-cfg.graphml file into the PNG format, do the following:
- Run yEd editor
- From main menu select "File" -> "Open...", then select the example-cfg.graphml file in your file system and press "Open"
- Select "Layout" -> "Hierarchical" then press "OK"
- Select "File" -> "Export..." and select PNG format
The result is on Figure 2.
Figure 2 : CFG model
Parameters are similar for GADD model:
$ ./retrascope example.vhd --module-name example --engine gadd-graphml-printer --graphml example-gadd.graphml
and for EFSM model:
$ ./retrascope example.vhd --module-name example --engine efsm-graphml-printer --graphml example-efsm.graphml
Random test generation¶
Random test generation is based on CFG model extraction. To generate random VHDL testbench for example.vhd VHDL module, run the tool with the following parameters:
$ ./retrascope example.vhd --module-name example --overwrite --engine cfg-random-test-generator --target vhdl-testbench --test-len 10
In this example two options should be mentioned. The "--test-len" option specifies the length of the test in simulation ticks. The "--overwrite" option, when enabled, allows the tool to overwrite the resulting testbench files.
By default, the HDL testbench has the following structure (the structure is the same for other test generators that use "test-vhdl-testbench-printer" or "test-verilog-testbench-printer" engines):
testbenches - top directory |__EXAMPLE - testbench directory (it's name is equal to the target top level module name) |__ EXAMPLE_testbench.vhd - top level testbench module |__ EXAMPLE_test.tst - test data file |__ EXAMPLE_tst_parser.vhd - test data file parser
EFSM Model Extraction¶
To be continued...