AverestExe 3.4.0

About Averest

Averest is a tool for the model-based design of reactive systems that supports the modeling, specification, simulation, compilation, formal verification, and synthesis of hardware circuits and software with a special focus on formally proven correctness. It contains compilers for synchronous languages, a simulator for the latter, support for formal verification with temporal and other logics, and various transformations for the hardware and software synthesis of reactive embedded systems which also covers pure hardware circuits and pure software systems. It also provides a small compiler for a tiny sequential programming language called MiniC and code generators for RISC and buffered exposed dataflow (BED) processors like the SCAD processor. Averest is developed by the Embedded Systems Group at the RPTU Kaiserslautern-Landau and is the result of a long-term and still ongoing research effort of this group. See also http://www.averest.org for further information.

Synchronous Programs: Quartz

The typical design flow with Averest starts with a system description written in the synchronous programming language Quartz that has been developed by the Embedded Systems Group at the RPTU Kaiserslautern-Landau. Quartz is very similar to Esterel, but also has some differences. Details about the Quartz language can be found in the introductory tutorial at http://www.averest.org/pdf/QuartzPresentation.pdf.

Sequential Programs: MiniC

MiniC is a toy language for sequential programs that has been introduced originally for teaching, but is now also part of Averest to describe sequential programs generated from the synchronous models. Averest provides also code generators for RISC processors, and buffered exposed datapath processors like the SCAD machine developed at RPTU.

Command Line Options

General Options

* Averest -h : print available command line options
* Averest -v : print version number

MiniC Compilation

* Averest -mnc2cmd file.mnc        -> file.cmd   (MiniC to CMD language)
* Averest -mnc2cfg file.cmd        -> file.dot   (MiniC to control-flow graph)
* Averest -mnc2cdfg file.cmd       -> file.dot   (MiniC to control-dataflow graph)
* Averest -mnc2abc file.mnc        -> file.abc   (MiniC to Abacus)
* Averest -mnc2dpn file.mnc        -> file.dpn   (MiniC to DPN)
* Averest -mnc2scad file.mnc [opt] -> file.scad,file.mvc (MiniC to SCAD move code)
    further options:
        -vb : verbose mode prints code simulation
        -level : levelize DPN before code generation
        -numPU p : use p general purpose PUs (default 4)
        -bfs n : set buffer size to n (default 4)
        -io x1=3,x7=8 : map input variables to constants
* Averest -mnc2cal file.mnc        -> file.cal   (MiniC to CAL)
* Averest -mnc2c file.mnc     -> file.c     (MiniC to C)
* Averest -mnc2fs file.mnc    -> file.fs    (MiniC to F#)

Quartz Compilation and linking

* Averest -qrz2aifs file.qrz  -> file.aifs  : translate Quartz to AIF system
* Averest -qrz2aifm file.qrz  -> file.aifm  : translate Quartz to AIF module
* Averest -linkaifm file.aifm -> file.aifs  : translate AIF module to AIF system
* Averest -aif2txt file.aif* [-flat] -> file.txt : AIF to Text
* Averest -aif2mnc file.aifs  -> file.mnc   : translate AIF to MiniC
* Averest -aif2smv file.aifs  -> file.smv   : translate AIF to SMV: equat+bitblast
* Averest -aif2crc file.aifs  -> file.crc   : translate AIF to Circuit: equat+bitblast
* Averest -crc2vhd file.crc   -> file.vhd   : translate Circuit to vhdl
* Averest -efsm file.qrz/.aifs-> file.efsm  : translate Quartz to EFSM by SOS rules

AIF Transformations

* Averest -equations file.aifs -> file-eqs.aifs    : group guarded actions into equations
* Averest -bitblast file.aifs  -> file-bits.aifs   : bitblasting aifs
* Averest -scalarize file.aifs -> file-scl.aifs    : expand arrays and tuples
* Averest -aif2aif tName file.aifs -> file-xx.aifs : apply AIF transformation tName
     available AIF transformations are:
    + SomeAbsenceToActions
    + AllAbsenceToActions
    + CtrlFlowToDataFlow
    + NxtDataEventsToMemorized
    + NxtOutToNow
    + PresetCompoundWrites
    + PresetCompoundReads
    + EliminateCompound
    + Scalarize
    + Bitvectorize
    + TupelizeBitvectors
    + Boolify
    + EliminateDeadCode
    + EqualizeControl
    + EqualizeData
    + Equalize

AIF Verification

* Averest -check file.aifs   : check specifications
* Averest -vcg file.aifs     : generate verification conditions
* Averest -prove file.prf    : execute proof commands

Simulation of qrz/aif/abc/dpn/scad

* Averest -simul file.qrz  [-micro -all -log] -> file.log
* Averest -simul file.aifs [-micro -all -log] -> file.log
* Averest -simul file.abc [-m steps]          -> file.log
* Averest -simul file.dpn [-m steps]          -> file.log
* Averest -simul file.mvc [opt]               -> file.html
    further options:
        -m n   : set number of steps to n (default unbounded)
        -isw n : set instruction issue width to n (default 4)
        -mms n : set memory size to n (default 4)
        -bfs n : set buffer size to n (default 4)