Lily - a LInear Logic sYnthesizer
Lily is a linear logic synthesizer, which synthesizes a functionally correct design from a formal specification. Lily is a command-line tool implemented on top of Wring (by Fabio Somenzi) and written in Perl. Lily takes a set of PSL or LTL properties and a partition of the used signals into input and output signals. If the given specification is realizable, Lily provides a design with the stated input and output signals that fulfills the specification. The design is a state machine represented as a VERILOG module or as a directed graph in DOT format.
General
Lily is based on the paper Barbara Jobstmann and Roderick Bloem, Optimizations for LTL Synthesis, FMCAD'06 [pdf].
For additional information, please contact Barbara Jobstmann or Roderick Bloem.
How to use Lily
Since Lily is written in Perl all you have to do is download the source files, unpack them, and add the source directory to the Perl 5 library and the search path. E.g., if the sources are in the directory /opt/lily and you use tcsh type
setenv PERL5LIB /opt/lily:${PERL5LIB}
setenv PATH /opt/lily:${PATH}
Now you can call Lily by simply typing
lily.pl
We use an example to show how to use Lily.
Traffic Light Example
We specify a small traffic light system for a crossing of a highway and a farm road. The systems has only two lights, which are either green or red. Signals hl and fl, which are output signals, encode these two lights. The highway light is green iff hl = 1, and similarly for the crossing farm road and fl. The input signal car indicates that a car is waiting at the farm road and timer represents the expiration of a timer. The specification assumes that the timer expires regularly. It requires that a green lamp stays green until the timer expires. Furthermore, one of the lamps must always be red, every car at the farm road is eventually allowed to drive on, and the highway lamp is regularly set to green.
Lily takes a specification and a partition file as input. The specification file holds a formal specification written in the linear-part of PSL or in LTL. The partition file divides the signals used in the specification file into input and output signals. Below we show the specification file and the partition file for our example.
Specification File in PSL Flavor
assume always(eventually!(timer)); assert always(!(hl & fl)); assert always(eventually!(hl)); assert always(car -> eventually!(fl)); assert always(hl -> (hl until! timer)); assert always(fl -> (fl until! timer));
Specification File in LTL Flavor
G(F(timer=1)) -> (G(fl=1 -> (fl=1 U timer=1)) *
G(hl=1 -> (hl=1 U timer=1)) *
G(car=1 -> F(fl=1)) *
G(F(hl=1)) *
G(!(hl=1 * fl=1)));
In our Example we have the four signals car, timer, fl, and hl. The first two are input signals, the later are output signals. The corresponding partition file is shown below.
Important note about the LTL syntax: The NOT-operator (!) has a lower operator precedence than the OR- and the AND-operator, e.g., !(G(a)) + F(b) = !( (G(a)) + F(b)).
Partition File
.inputs timer car .outputs hl fl
Command
Lily is an extension to Wring. All command line options valid in Wring are valid in Lily as well.
lily.pl [-c {0,1}] [-f formula] [-h] [-ltl file]
[-m method] [-o {0,1}] [-p prefix] [-s {0,1}] [-v n]
[-ver {0,1}] [-auto file] [-mon file]
[-syn file] [-syndir synthesisDir] [-mc]
[-ouct {0,1}] [-oawt {0,1}] [-owit {0,1}]
[-omh {0,1}] [-omhc {0,1}]
[-oedges {0,1}] [-orelease {0,1}] [-oreuse {0,1}]
With the command line options inherited from Wring the user can determine the name of the specification file, the prefix for the output files, verbosity, and parameters for the construction of Buechi automata provided by Wring. Lily has new command line options to invoke the synthesis process, to define the name of the partition file, to specify an output directory, to verify the generated design, and to switch various optimizations on and off. By default all optimizations are turned on. The user need not care about those options. For a detailed description of all command line options type
lily.pl -h
Let us continue the traffic light example. If the specification is stored in the file tl.ltl and the partition is stored in the file tl.part the simplest way to call Lily is to use one of the following commands:
lily.pl -syn tl.part -ltl tl.ltl lily.pl -syn tl.part -ltl tl.ltl -syndir trafficlight
The output files are stored in the current directory or in the new directory trafficlight depending on the chosen command.
Output Files
Lily provides a VERILOG module and a graphical state diagram of the the generated design. We use DOT format to store the state diagram. Files in DOT format can be translated using dot.
By default Lily generated the following two files:
ltl2vl-verilog.v ltl2vl-synthesis.dot
If the specification is realizable the file ltl2vl-verilog.v holds the VERILOG module of the generated design. The state diagram of the generated design is stored in the file ltl2vl-synthesis.dot. If the specification is not realizable both files state that the given specification is unrealizable. Note that the prefix ltl2vl can be replaced by a user defined prefix with the option -p.
The specification we used in our traffic light example is realizable and the generated design and the corresponding state diagram are shown below. Note that the result you get can differ from the one below because most of the structures are based on Perl Hashes, which do not have a unique order.
module synthesis(fl,hl,clk,car,timer);
input clk,car,timer;
output fl,hl;
wire clk,fl,hl,car,timer;
reg [1:0] state;
assign hl = (state == 0)||(state == 2);
assign fl = (state == 1);
initial begin
state = 0; //n15_1n18_1
end
always @(posedge clk) begin
case(state)
0: begin //n15_1n18_1
if (car==0) state = 0;
if (car==1 && timer==1) state = 1;
if (car==1 && timer==0) state = 2;
end
1: begin //n12_1n18_1
if (timer==1) state = 0;
if (timer==0) state = 1;
end
2: begin //n10_1n15_1n18_1
if (timer==0) state = 2;
if (timer==1) state = 1;
end
endcase
end
endmodule //synthesis
