|
|
The starting point of the design flow are programs written in the language Quartz. Using qrz2aif.exe of the Averest distribution, a Quartz program in file "file.qrz" is translated to a corresponding aifs file "file.aifs" where all modules called in "file.qrz" are also compiled (if not already done) to aif modules (having suffix "aifm").
Only aif systems (having suffix "aifs") can be processed by further tools, aif modules (having suffix "aifm") are only used as intermediate files for modular compilation.
The aifs files contain the guarded commands that are derived from the Quartz file. Instead of applying qrz2aif to a single Quartz file, you might also apply the tool to a list of Quartz files, and even to a directory. The Quartz compiler qrz2aif.exe will then compile all Quartz files in the directory.
You may view the content of aifs files using the pretty printer aif2txt.exe, and you may write your own tools for working with aifs files. To this end, note that aifs files are XML files, and you may contact us for further information on their syntax.
The tool aif2dot translates aifs files to dot files used by the GraphViz software which can layout these graphs and generate various file formats from them. For example, you may explore the extended finite state machine or the dependence graph of the guarded actions by these graphs.
Typically, the next step involves the use the simulator aif2trc.exe which prints out a simulation trace either in micro steps or macro steps of the execution. Specifications are not considered by the simulator, and the simulation of hybrid systems is also not yet available in the distributed version.
Verification is available in terms of the translation of aifs files to SMV so that a version of SMV can be used for model checking. Averest will soon offer many translations from temporal logics to mu-calculus, and we intend to support soon also interfaces to interactive theorem provers like HOL.
For synthesis, aifs files can be translated to C or Verilog programs. We are currently working out further code generations for dataflow networks and other form of multithreaded code generation.
Several important transformations can be applied to aifs files, like e.g. a translation to an extended finite state machine. The code generators behave very different if the one or the other transformation has been applied in advance. The set of transformation is currently reworked, so that we do not yet offer a detailed documentation. You may consult us if you are interested to work with aifs transformations.
While all the above executables are command line tools, Averest offers also a small graphical user interface that allows one to apply the command line tools as well. To this end, you may simply drag Quartz or aif files to the panel and then select the desired action to be performed.
rmaif.exe is a tool that removes all aif files that are found in the directory given as argument except that there no Quartz file is found for the corresponding aifs file. Thus, if you have obtained aifs files from someone else, you may savely use rmaif.exe to clean up directories.
In the folder averest/bin, you can call the executables from the command
line where a typical call is of the form "toolname.exe
Note that you cannot simply move the executables to other directories since the dynamic libraries are expected to be in the same directory. For your convenience, you can however create a link to the executables, and in particular to the Averest GUI. To this end, right-click on an executable in the bin directory, select "Send..." and choose entry "Desktop (Create link)".
To call the executable toolname.exe, use a terminal and type
mono path-to-averest/bin/toolname.exeinfile
For your convenience, you may create for each tool an alias or even a small shell script to avoid the explicit call to mono e.g. a script for qrz2aif.exe would look like this
#!/bin/bash mono path-to-averest/bin/qrz2aif.exe $@
The above explanations also apply to the GUI Averest.exe.
|