|
|
The Averest project aims at providing a complete set of tools for the development of reactive systems. Currently, it consists of the following components: a compiler for translating synchronous programs to our intermediate format, a set of transformations, a symbolic model checker, and a tool for hardware/software synthesis. Thus, Averest already covers large parts of the design flow of reactive systems from the specification to the implementation.
The design flow using Averest consists of the following steps: First, the system is described as a program in our imperative synchronous language Quartz. Then, the program is translated to synchronous guarded actions, which are the base of the Averest Intermediate Format (AIF) using the Quartz compiler qrz2aif. This intermediate description can be directly used for simulation with the simulator aif2trc. Furthermore, it can be used by the symbolic model checker SMV or the interactive theorem prover HOL to check whether the system satisfies its specifications. If this is the case, it can be synthesized using the various aif2* tools, which are able to generate an implementation in hardware or software.
Synchronous languages are well-suited for the design of reactive systems. Their common paradigm is the perfect synchrony, which means that most of the statements are executed as micro steps in zero time. Consumption of time is explicitly programmed by partitioning the micro steps using pause statements into macro steps that all take the same amount of logical time. Thus, concurrent threads run in lockstep and automatically synchronize at the end of a macro step. The introduction of micro and macro steps is not only a convenient programming model, it is also the key to generate deterministic single-threaded code from multi-threaded synchronous programs. Thus, synchronous programs can be executed on ordinary microcontrollers without complex operating systems. As another advantage, the translation of synchronous programs to circuits is straightforward. Moreover, the formal semantics of synchronous languages makes them particularly attractive for reasoning about program semantics and correctness.
Key features of Quartz are generic statements to describe parameterized systems, different forms of parallel execution (synchronous, asynchronous, interleaved), nondeterministic choice, event and state variables, integers of infinite and finite bitwidth as well as multi-dimensional array types.
The compiler qrz2aif is used to translate Quartz programs to synchronous guarded actions. Most parts of the translation of Quartz statements to transitions implemented in Ruby have been formally verified using the HOL theorem prover. In particular, the translation covers schizophrenic local declarations which is a nontrivial issue in the compilation of synchronous languages.
The Averest Intermediate Format (AIF) is a file format designed for describing synchronous systems at an intermediate level. Its main purpose is to serve as a language for exchanging system descriptions between the Averest component. AIF is based on the Extensible Markup Language (XML) and is not intended for interaction with human users, though it can be used for this purpose. The following features were essential for the design of AIF:
Since AIF is based on the Extensible Markup Language (XML), it is independent of operating systems and encodings. Additionally, most programming languages offer support for XML and there is large number of tools for processing XML files, e.g. parsers and converters. AIF follows the style of guarded actions, a well-established model for the description of concurrent systems. This simplifies the semantics and provides a high degree of flexibility.
Averest provides various transformations to prepare the synchronous guarded actions obtained by the compilation for synthesis. For example:
Aggregate data types like arrays and bitvectors can be translated to scalar data types. This allows to translate Quartz programs to hardware circuits and also to interface Averest with many other tools that are not able to deal with such data types directly.
Specifications given in linear temporal logic (LTL) even with an anchored version of past operators are translated to omega-automata and/or fixpoints in CTL and the µ-calculus. Averest currently offers two translations that respect the membership to safety, liveness, and fairness classes of temporal logic. Moreover, specifications may also be parameterized, e.g. to specify parametric conjunctions.
Built-in verification is provided by a symbolic model checker for finite and infinite state systems. As usual in symbolic model checking, finite sets are encoded by their characteristic functions in propositional logic using binary decision diagrams (BDDs). For the representation of infinite sets, however, more powerful logics are required, since propositional logic is naturally limited to the representation of finite sets. For that purpose, we use Presburger arithmetic, a decidable first-order predicate logic over the integers with addition as the basic operation. In the same way, we lift the specification language from propositional logic to Presburger arithmetic. As the specification language, Averest uses the µ-calculus which subsumes popular temporal logics such as CTL and LTL. Even though the µ-calculus is very powerful, it is commonly viewed as some sort of 'assembly' language for verification. For this reason, Averest includes a translator from FairCTL, an extension of CTL with fairness constraints, to the µ-calculus.
The synthesis tools aif2* translating system descriptions in AIF to hardware or software. Moreover, they can be used as a converter for third-party tools, e.g. other model checkers. Currently, the supported languages include ISO C, LEGO C, SystemC, Java, Standard ML, Verilog and VHDL.
For Verilog or VHDL output, finite state machines are generated that can be used as input for other tools such as FPGA compilers to build hardware. The C output can be used for simulation or for a direct implementation on a micro-controller. For that purpose, functions are provided to set the inputs and to get the outputs of a program.
|