Averest 3.1.1

About Averest

Averest is a framework 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 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.

Main modules

The full documentation of the API generated by FsDocs is available at http://www.averest.org/AverestLibDoc/reference. To give you a quick overview on the modules of the Averest library, have a look at the following (incomplete) list of modules:

• Averest.Core

  • Graphs: some basic algorithms on graphs and partial orders
  • Types: implements types of the Quartz language
  • Names: implements qualified names used by identifiers
  • Declarations: implements declarations of modules
  • Abbreviations: implements an abbreviation table to share common subexpressions
  • Expressions: implements the expressions of the Quartz language
  • Actions: implements atomic actions like immediate/delayed assignments and assertions
  • Specifications: implements temporal logic specifications

• Averest.Quartz

  • UtyExprs: untyped expressions (after initial parsing)
  • UtyStmts: untyped statements (after initial parsing)
  • Statements: typed statements of the Quartz language
  • Compiler: provides parsers and compilers to systems and modules

• Averest.MiniC

  • Types: Abacus instructions, CMD instructions, MiniC expressions/statements/programs
  • IO: parsers for Abacus, MiniC, CMD programs
  • CodeTransformations: MiniC->C, MiniC->F#, predication and SSA-form of MiniC
  • Compiler: translate to control-dataflow graphs (CMD programs)
  • DataflowProcessNetworks: MiniC->DPN, Leveling DPNs, Parsing DPNs, Simulation of DPNs, Dataflow Computer
  • CodeGenAbacus: perform dataflow analysis (liveness, used variables), register allocation and RISC code generation
  • CodeGenSCAD: DPN->SAT/SMT constraints; DPN+PUalloc->2SAT constraints, VertexDisjointNodeCovers
  • Abacus: simulator for the Abacus RISC processor
  • ScadSim: simulator for the SCAD processor

• Averest.Analysis

  • BDD: provides a complete implementation of binary decision diagrams
  • Matrices: provides types for matrices, linear equation solvers, linear inequality solvers (simplex and Fourier-Motzkin)
  • SatSolver: provides a little SAT solver with non-chronological backtracking
  • TemporalLogic: provides translations of LTL/LeftCTL*/CTL to omega-automata, and mu-calculus

• Averest.Transform

  • BitBlast: converts expressions and modules to a bit-level
  • Scalarizer: expands all variables of compound types to scalar enumerations
  • Scheduling: provides some scheduling algorithms (ASAP,ALAP,Force-Directed,List,Linear scheduling)