DIPLODOCUS Help: Simulation and Formal Verification
Simulation, verification: What's for?
Using TTool's graphical interface, it is quite easy to perform the simulation of a DIPLODODOCUS model. Yet, only basic functions are accessible with the graophical interface of the simulator. Also, whenever the simulator shall be called from a script, then the command line interface of the simulator becaomes useful. This page is about the syntax of the command line interface
How to generate the simulator code?
- You first need to make generate the simulation code from the TTool mapping model.
- Second, you need to compile the generated code. It he commpilation succeeds, a "run.x" file should be created.
$ cd TTool/simulartors/c++2
$ make all
Using the simulator
Usual functions
- The most obvious way to get help on the simulator is to start it with the -help option:
$ ./run.x -help
To simulate the system until it terminates, simply do:
$ ./run.x
One interesting feature is to select how the results are output, eith in html, text or vcd format. For example the following command simulates the system and writes traces to ofile in vcd format:
$ ./run.x -o-ovcd ofile
Formal verification
The simulator can be used to
output a reachability graph of the system under design. To do so, enter the following command (the graph will be saved in
mygraph:
$ ./run.x -explo -gpath mygraph
Advanced functions
The simulator interface makes it possible to
execute a set of commands in sequence. This can be obtained by providing the sequence of commands to the simulator with the -cmd options. For example, the following sequence of commands executes 1000000 commands in the simulator, and then saves the trace in vcd format in the file
vcddump.vcd
$ ./run.x -cmd '1 2 1000000;7 0 vcddump.vcd'
List of commands
"Cmd" stands for "Command", "P1", "P2", "P3", "P4, P5" represents the parameters of the command. The two next columns explain whether the command can be executed with the command line interface ("Impl:Sim"), or from the TTool graphical simulation window ("Impl:GUI"). By default, all commands are synchronous, that is, they can be executed only when another command is not currently under execution by the simulator. Yet, the simulator accepts a few asynchronous commands that can be accepted by the simulator while the latter is executing another command (column "Async").
Cmd |
P1 |
P2 |
P3 |
P4 |
P5 |
Impl:Sim |
Impl:GUI |
ASync |
Description |
0 |
|
|
|
|
|
OK |
OK |
YES |
Terminate simulator |
1 |
0 |
|
|
|
|
OK |
OK |
|
Run to next break point |
1 |
2 |
x:Int |
|
|
|
OK |
OK |
|
Run x transactions |
1 |
4 |
x:Int |
|
|
|
OK |
OK |
|
Run x commands |
1 |
5 |
x:Int |
|
|
|
OK |
OK |
|
Run to time x |
1 |
6 |
x:Int |
|
|
|
OK |
OK |
|
Run for x time units |
1 |
7 |
|
|
|
|
OK |
OK |
|
Run exploration |
1 |
8 |
x:ID |
|
|
|
OK |
OK |
|
Run to next transfer on bus x |
1 |
9 |
x:ID |
|
|
|
OK |
OK |
|
Run until CPU x executes |
1 |
10 |
x:ID |
|
|
|
OK |
OK |
|
Run until Task x executes |
1 |
11 |
x:ID |
|
|
|
OK |
OK |
|
Run until Memory x is accessed |
1 |
12 |
x:ID |
|
|
|
OK |
OK |
|
Run until operation on Channel x is performed |
1 |
13 |
|
|
|
|
OK |
OK |
|
Run to next random choice command |
1 |
14 |
x:ID |
y:String |
|
|
OK |
|
|
Run until Condition y expressed in terms of variables of Task x is fulfilled |
2 |
|
|
|
|
|
OK |
OK |
|
Reset simulation |
3 |
x:Int |
y:ID |
|
|
|
OK |
OK |
|
Print Variable y of Task x |
4 |
0 |
x:ID |
|
|
|
OK |
OK |
|
Get information about CPU x |
4 |
1 |
x:ID |
|
|
|
OK |
OK |
|
Get information about Bus x |
4 |
2 |
x:ID |
|
|
|
|
|
|
Get information about Memory x |
4 |
3 |
x:ID |
|
|
|
|
|
|
Get information about Bridge x |
4 |
4 |
x:ID |
|
|
|
OK |
|
|
Get information about Channel x |
4 |
5 |
x:ID |
|
|
|
OK |
OK |
|
Get information about Task x |
4 |
6 |
x:ID |
|
|
|
|
|
|
Get information about HWA x |
5 |
x:ID |
y:ID |
z:Int |
|
|
OK |
OK |
|
Set Variable y of Task x to value z |
6 |
x:ID |
y:Int |
|
|
|
OK |
OK |
|
Write y samples to Channel x |
6 |
x:ID |
y:Int |
p1:Int |
p2:Int |
p3:Int |
OK |
|
|
Write y Events to Channel x, parameters p1-p3 |
7 |
0 |
x:String |
|
|
|
OK |
OK |
|
Save traces in VCD File x |
7 |
1 |
x:String |
|
|
|
OK |
OK |
|
Save traces in HTML File x |
7 |
2 |
x:String |
|
|
|
OK |
OK |
|
Save traces in TXT File x |
8 |
x:String |
0 |
|
|
|
OK |
OK |
|
Save simulation state in File x |
8 |
x:String |
1 |
|
|
|
|
|
|
Save simulation state in RAM, Identifier x |
9 |
x:String |
0 |
|
|
|
OK |
OK |
|
Restore simulation state from File x |
9 |
x:String |
1 |
|
|
|
|
|
|
Restore simulation state from RAM, Identifier x |
10 |
0 |
x:String |
|
|
|
OK |
OK |
|
Print benchmarks on screen |
10 |
1 |
x:String |
|
|
|
OK |
OK |
|
Save benchmarks in File x |
11 |
x:ID |
y:ID |
|
|
|
OK |
OK |
|
Set break point in Task x, Command y |
12 |
x:ID |
y:ID |
z:Int |
|
|
OK |
|
|
Choose branch in Task x, Command y, branch ID z |
13 |
|
|
|
|
|
OK |
OK |
YES |
Get actual time |
14 |
x:ID |
|
|
|
|
OK |
OK |
YES |
Get actual command of Task x |
15 |
|
|
|
|
|
OK |
OK |
YES |
Stop simulation |
16 |
x:ID |
y:ID |
|
|
|
OK |
OK |
|
Remove break point in Task x, Command y |
17 |
|
|
|
|
|
OK |
|
|
Get number of branches of current command |
18 |
|
|
|
|
|
OK |
OK |
|
Get break point list |
19 |
|
|
|
|
|
OK |
OK |
|
Get hash value |
20 |
0/1 |
|
|
|
|
OK |
OK |
|
Disable/Enable breakpoints |
21 |
|
|
|
|
|
OK |
OK |
|
Get execution statistics of commands |
22 |
x:Int |
|
|
|
|
OK |
OK |
|
Get list of the last n transactions for each execution (CPU) and transfer (bus) nodes |
- ID refers to the id or a name of a component.
- Asynchronous commands can be carried out at any time, regardless whether the simulator is running or not.
- An asynchronous command is processed right away and merely one response is generated which also represents the ACK.
- Parameters are sent in plain text format (ASCII), separated by space characters. That way, the simulator can also be operated manually via a simple telnet connection.
- Synchronous commands which are received while the simulator is running are discarded without further notice.
- Two acknowledgments are sent in response to a synchronous command: the first one upon reception of the command and the second one upon its completion. Thus, the application controlling the simulator has to perform the following procedure: issue a synchronous command, wait for a reception ACK, wait for a completion ACK, and so forth. As the connection is reliable (TCP), timeouts are not necessarily required, but they could reveal that the simulator has crashed.
- Replies of the simulator are sent in XML format in compliance with a provided DTD format.
Extending/scripting the simulation engine
Events generated by the event sources
Components of the simulation engine can transmit information events. They are listed in the following table.
|
Kernel |
Cmd |
Task |
Channel |
CPU |
Bus |
Mem |
Bridge |
transExecuted |
|
|
X |
X |
X |
X |
X |
X |
cmdEntered |
|
X |
|
|
|
|
|
|
cmdStarted |
|
X |
|
|
|
|
|
|
cmdExecuted |
|
X |
|
|
|
|
|
|
cmdFinished |
|
X |
|
|
|
|
|
|
taskStarted |
|
|
X |
|
|
|
|
|
taskFinished |
|
|
X |
|
|
|
|
|
readTrans |
|
|
|
X |
|
|
|
|
writeTrans |
|
|
|
X |
|
|
|
|
simStarted |
X |
|
|
|
|
|
|
|
simFinished |
X |
|
|
|
|
|
|
|
- Shorthands for event sources of a specific type: allCPUs, allBuses, allBridges, allMems, allHWA, allChannels, allEvents, allRequests, allTasks.
- Within ERBs, filters (event text box in TTool's ERB attributes window) are defined using the following syntax: event(source1, source2, source3,...), for example: transExecuted(allCPUs, channel1, bus2).
Exposed API
Task abstraction
- getPriority()
- getName()
- getID()
- Statistics missing: getExecTime(), getAvContDelay()
Bus abstraction
- getBurstSize()
- getName()
- getID()
- Beware: support for several buses missing
CPU abstraction
Channel abstraction
- getName()
- getID()
- getOverflow()
- getUnderflow()
- getContent()
Command abstraction
- getCommandStr()
- getID()
- getProgress()
- getLength()
Transaction abstraction
- getRunnableTime()
- getStartTime()
- getLength()
- getVirtualLength()