Anzu
Anzu synthesizes Verilog designs from specifications written in LTL (Linear Temporal Logic). It is an implementation of Pnueli, Piterman, and Sa'ar's Reactive-1 approach (see N. Piterman, A. Pnueli, and Y. Sa'ar. "Synthesis of Reactive(1) Designs", LNCS 3855, 2006), which can handle a huge subset of LTL given in a particular format (see "Input Format" below).
News
2009-09-09: A new synthesis tool, based on the same algorithm as Anzu, has been released. It provides the same basic functionality as Anzu, and has several new features, such as different output formats, different ways of circuit generation, a graphical user interface, etc. The new tool is called RATSY and can be downloaded from http://rat.fbk.eu/ratsy. The release also contains a utility program to convert Anzu input files to RATSY input files.
Install
In order to run anzu on your computer you need to install Perl 5 if it is not yet on your machine. In all following steps we will assume that Perl 5 is installed. To install anzu you have to do following:
- Goto the download section,
download anzu and extract the tar-ball to a directory:
tar -xvzf anzu-??????.tgz
- Download PerlDD from Fabio
Somenzi's Homepage and extract it. Then, apply the PerlDD-Patch and install
PerlDD:
tar -xvzf PerlDD-0.07.tgz cd PerlDD-0.07 patch -p1 < PerlDD-0.07.patch perl Makefile.pl make
Note that you do not need to install PerlDD by typing make install, because we will set the Perl5LIB-Path in the next step. -
Set your PATH and Perl5LIB-Path by the use of
following commands (for tcsh). Replace
"/path/to/anzu/src/" with the path to your
anzu directory and "/path/to/PerlDD" with
the path to your PerlDD installation.
setenv ANZU_SRC /path/to/anzu/src setenv PERLDD_PATH /path/to/PerlDD setenv PERL5LIB ${PERLDD_PATH}/blib/arch:${PERLDD_PATH}/blib/lib:.:${ANZU_SRC}:${PERL5LIB} setenv PATH ${PATH}:${ANZU_SRC}
Now you should be able to run anzu. The following command will dump the description of possible command line arguments to the standard output:
anzu.pl -h
Download
- Anzu
- AMBA-Case Study
- GenBuf-Case Study
- Running Lights Demo
- Debugging Formal Specifications
- Enhanced Anzu version with debugging features,
including specifications and scripts to perform the debugging case study (tgz, 526kB)
- Enhanced Anzu version with debugging features,
Case Studies
- IBM GenBuf Controller
(see R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer. "Specify, Compile, Run: Hardware from PSL" in Workshop on Compiler Optimization Meets Compiler Verification (COCV'07), [pdf]) - ARM AMBA AHB Arbiter
(see R. Bloem, S. Galler, B. Jobstmann, N. Piterman, A. Pnueli, and M. Weiglhofer. "Automatic hardware synthesis from specification: A case study" in DATE'07, [pdf])
Please note that there is a typo in Table 1: Guarantee 7 should read ∀ i: always( (DECIDE /\ next! HGRANTi) -> (HLOCKi <-> next!(LOCKED))) - Debugging Formal Specifications
(see R. Könighofer, G. Hofferek, R. Bloem. "Debugging Formal Specifications Using Simple Counterstrategies" in Formal Methods in Computer Aided Design (FMCAD) 2009, [pdf])
Input Format
The specification has to be split into assumptions on the environment, and constraints on the system. Both parts consist of (1) initial constraints (formulas like a=0 * b=0), (2) constraints on the transition function (e.g. G(a -> X(b)), and (3) fairness constraints (G(F(a))). A lot of LTL formulas can we converted into this format. Below you'll find a small example of a config file for Anzu: The first two sections ([INPUT_VARIABLES], [OUTPUT_VARIABLES]) define the input and output signals of the design we'd like to generate. The following three sections ([ENV_INITIAL], [ENV_TRANSITIONS], [ENV_FAIRNESS]) state the assumptions on the environment, and the last three sections ([SYS_INITIAL], [SYS_TRANSITIONS], [SYS_FAIRNESS]) specify the desired behavior of the system.
[INPUT_VARIABLES]
r0;
r1;
[OUTPUT_VARIABLES]
g0;
g1;
[ENV_INITIAL]
r0=0;
r1=0;
[ENV_TRANSITIONS]
G((r0=1 * g0=0) -> X(r0=1));
G((r0=0 * g0=1) -> X(r0=0));
G((r1=1 * g1=0) -> X(r1=1));
G((r1=0 * g1=1) -> X(r1=0));
[ENV_FAIRNESS]
G(F(r0=0 + g0=0));
G(F(r1=0 + g1=0));
[SYS_INITIAL]
g0=0;
g1=0;
[SYS_TRANSITIONS]
G((r0=0 * g0=0) -> X(g0=0));
G((r0=1 * g0=1) -> X(g0=1));
G((r1=0 * g1=0) -> X(g1=0));
G((r1=1 * g1=1) -> X(g1=1));
G(g0=0 + g1=0);
[SYS_FAIRNESS]
G(F((r0=1) <-> (g0=1)));
G(F((r1=1) <-> (g1=1)));
Generated Design
In order to give an idea how the generated design looks like, we show the design generated from the specification above:
module main(clock, r0, r1, g0, g1, jx0);
input clock;
wire zero_value = 0;
wire one_value = 1;
wire v844766;
wire v84476c;
...
wire v844a9c;
reg r0_p;
input r0;
reg r1_p;
input r1;
reg g0_p;
output g0;
reg g1_p;
output g1;
reg jx0_p;
output jx0;
assign v84477b = g0_p & v844766 | !g0_p & !v84476c;
assign v84479f = g0_p & v844766 | !g0_p & !v844773;
assign v84479b = r1_p & v844770 | !r1_p & !v844770;
assign v844766 = 1;
assign v84476c = r1_p & v844766 | !r1_p & !v844766;
assign g1 = !v844a9c;
assign v844778 = jx0_p & v8447b3 | !jx0_p & !v84476e;
assign v844770 = g1_p & v844766 | !g1_p & !v844766;
assign v84478d = r1 & v84476c | !r1 & v844766;
assign v84479c = g0_p & v84478d | !g0_p & !v84479b;
assign v8447b3 = g0_p & v84476c | !g0_p & !v84479b;
assign v84476e = g0_p & v844766 | !g0_p & !v844766;
assign v844a4d = r0_p & v844780 | !r0_p & v844778;
assign v844773 = r1_p & v844770 | !r1_p & !v844766;
assign g0 = v844a80;
assign v8447b7 = jx0_p & v84477b | !jx0_p & v84479f;
assign jx0 = v844a4d;
assign v844a80 = r0_p & v8447b7 | !r0_p & !v844766;
assign v844a9c = r0_p & v8447b7 | !r0_p & !v84476c;
assign v844780 = jx0_p & v84479c | !jx0_p & v84476e;
initial begin
r0_p = 0;
r1_p = 0;
g0_p = 0;
g1_p = 0;
jx0_p = 0;
end
always @(posedge clock) begin
r0_p = r0;
r1_p = r1;
g0_p = g0;
g1_p = g1;
jx0_p = jx0;
end
endmodule
Since automatically generated design are hard to read and understand, you'll find a simulation run of our example design below. Each line represents one time step. The left two columns show the values of the input signals r0 and r1, the columns on the right show the response of the generated system. The signal "jx0" in internal signal necessary for the synthesis process (You can simple ignore it :-)).
Input; Output ---------------- r0 r1 g0 g1 jx0 0 0 ; 0 0 1 1 0 ; 0 0 0 0 0 ; 1 0 0 0 1 ; 0 0 0 0 1 ; 0 1 1 0 0 ; 0 1 0 1 1 ; 0 0 1 1 1 ; 0 1 1 1 1 ; 0 1 0 1 0 ; 0 1 0 1 0 ; 1 0 0 0 0 ; 1 0 1 0 0 ; 0 0 0