Dear Fang,
Here is how it goes.
First, you are going to use the vis language_emptiness command, which
looks for the existence of a single path that satisfies the formula.
You are not interested in whether there is a single path that satisfies
"G(((car_present = YES) * (timer.state = LONG)) -> F(farm_light =
GREEN))," but rather you want to know if there is a path that violates
it! So you negate the property and create an automaton:
./ltl2aut.pl -f '!(G(((cp=1)*(tst=1)) -> F(fl=1)))' -p wring -s 0 -o 0
-m GPVW -v 0 -mon tlcmon.v
Then you add this automaton to your model, and connect up the wires.
First the automaton goes in, of which we'll just show the header here.
See the attachment for the rest.
module Buechi(clock,fl,tst,cp,fair);
Then we'll add some wires and hook up the monitor:
/* for monitor */
wire car_present_yes;
wire timer_state_long;
wire farm_light_green;
timer_state wire state;
wire fair;
assign car_present_yes = (car_present == YES);
assign timer_state_long = (state == LONG);
assign farm_light_green = (farm_light == GREEN);
Buechi monitor(clk, timer_state_long, car_present_yes,
farm_light_green, fair);
Finally, we need to add a fairness constraints to the constraints
already present: (monitor.fair=1). (See attachments for the complete
set of fairness constraints.)
Then all we have left to do is to run vis:
vis> read_verilog tlc-ltl1.v
tlc-ltl1.v
Warning: Some variables are unused in model main.
Warning: Some variables are unused in model Buechi.
vis> init
vis> read_fairness tlc-ltl1.fair
vis> language_emptiness -d1
# LTL_MC: formula passed
It worked! Le has found that the language is empty, hence there are no
paths that violate the property, and we can be happy. All cars may
eventually pass the lights.
An automated way of doing all this is in the works. Keep your eyes out
for the next Vis release!
Roderick
Fang Wang wrote:
>Dear vis,
>
>I still had some problem in using vis "lang_empty".
>My problem is as follwing.
>
>I used `tlc` example in the package in the path "\examples\tlc"
>and try to verify an LTL property
>
>"G(((car_present = YES) * (timer.state = LONG)) -> F(farm_light =
>GREEN))"
>
>First, I used "Wring-1.1.0" generated a verilog file "foo.v" in which
>I replace
> "car_present = YES" with "p = 1"
> "timer.state = LONG" with "q = 1"
> "farm_light = GREEN" with "r = 1"
>
>then I try to use vis "lang_empty" to verify it,
>but I donot know how to put in both "tlc.mv" and "foo.mv".
>
>Could you please tell me how to do this property check.
>
>Regards!
>
>fang
>
>
>
/**************************************************************************
Adaptation of Mead and Conway traffic light controller.
A little used farm road intersects with a multi-lane highway; a traffic
light controls the traffic at the intersection.
The light controller is implemented to maximize the time the highway light
remains green. A submodule implements a timer, which outputs "short" and
"long" time outs. The highway light stays green for at least "long" time.
Any time after "long" time, if there is a car waiting on the farm road, then
the farm light turns green. The farm light remains green until there are no
more cars on the farm road, or until the long timer expires. The yellow
light for both directions stays yellow for "short" time.
The timer has non-determinism in it. Liveness properties won't pass until
fairness constraints are placed on the timer, so that it can't pause
forever.
Tom Shiple, 25 October 1995
***************************************************************************/
/*
* Symbolic variables.
*/
typedef enum {YES, NO} boolean;
typedef enum {START, SHORT, LONG} timer_state;
typedef enum {GREEN, YELLOW, RED} color;
/*
* Module main ties together the underlying modules. In addition, it
* ORs together the start timer outputs of the farm road and highway
* controllers. Note that only a single timer is used for both the farm
* road and highway controllers. In theory, this could lead to conflicts; as
* implemented, such conflicts are avoided.
*/
module main(clk);
input clk;
color wire farm_light, hwy_light;
wire start_timer, short_timer, long_timer;
boolean wire car_present;
wire enable_farm, farm_start_timer, enable_hwy, hwy_start_timer;
/* for monitor */
wire car_present_yes;
wire timer_state_long;
wire farm_light_green;
timer_state wire state;
wire fair;
assign car_present_yes = (car_present == YES);
assign timer_state_long = (state == LONG);
assign farm_light_green = (farm_light == GREEN);
assign start_timer = farm_start_timer || hwy_start_timer;
timer timer(clk, start_timer, short_timer, long_timer, state);
sensor sensor(clk, car_present);
farm_control farm_control(clk, car_present, enable_farm,
short_timer, long_timer, farm_light,
farm_start_timer, enable_hwy);
hwy_control hwy_control(clk, car_present, enable_hwy,
short_timer, long_timer, hwy_light,
hwy_start_timer, enable_farm);
Buechi monitor(clk, timer_state_long, car_present_yes,
farm_light_green, fair);
endmodule
/*
* Monitor to check G(((cp=YES)*(tst=1)) -> F(fl=1))
* Model check EG_fair true.
*/
typedef enum {n1,n2,n3,Trap} states;
module Buechi(clock,fl,tst,cp,fair);
input clock,fl,tst,cp;
output fair;
states reg state;
states wire ND_n1_n3;
assign ND_n1_n3 = $ND(n1,n3);
assign fair = (state == n2) || (state == n3);
initial state = n1;
always @ (posedge clock) begin
case (state)
n2,n3:
case (fl)
1'b0: state = n2;
1'b1: state = Trap;
endcase
Trap:
state = Trap;
n1:
case ({cp,fl,tst})
3'b0??: state = n1;
3'b100: state = n1;
3'b101: state = ND_n1_n3;
3'b11?: state = n1;
endcase
endcase
end
endmodule
/*
* There is a single, coupled sensor that detects the presence of a car
* in either direction of the farm road. At each clock tick, it non-
* deterministically reports that a car is present or not.
*/
module sensor(clk, car_present);
input clk;
output car_present;
wire rand_choice;
boolean reg car_present;
initial car_present = NO;
assign rand_choice = $ND(0,1);
always @(posedge clk) begin
if (rand_choice == 0)
car_present = NO;
else
car_present = YES;
end
endmodule
/*
* From the START state, the timer produces the signal "short"
* after a non-deterministic amount of time. The signal "short"
* remains asserted until the timer is reset (via the signal "start").
* From the SHORT state, the timer produces the signal "long"
* after a non-deterministic amount of time. The signal "long"
* remains asserted until the timer is reset (via the signal "start").
* The following Buchi fairness constraints should be used:
*
* !(timer.state=START);
* !(timer.state=SHORT);
*/
module timer(clk, start, short, long, state);
input clk;
input start;
output short;
output long;
output state;
wire rand_choice;
wire start, short, long;
timer_state reg state;
initial state = START;
assign rand_choice = $ND(0,1);
/* short could as well be assigned to be just (state == SHORT) */
assign short = ((state == SHORT) || (state == LONG));
assign long = (state == LONG);
always @(posedge clk) begin
if (start) state = START;
else
begin
case (state)
START:
if (rand_choice == 1) state = SHORT;
SHORT:
if (rand_choice == 1) state = LONG;
/* if LONG, remains LONG until start signal received */
endcase
end
end
endmodule
/*
* Farm light stays RED until it is enabled by the highway control. At
* this point, it resets the timer, and moves to GREEN. It stays in GREEN
* until there are no cars, or the long timer expires. At this point, it
* moves to YELLOW and resets the timer. It stays in YELLOW until the short
* timer expires. At this point, it moves to RED and enables the highway
* controller.
*/
module farm_control(clk, car_present, enable_farm, short_timer, long_timer,
farm_light, farm_start_timer, enable_hwy);
input clk;
input car_present;
input enable_farm;
input short_timer;
input long_timer;
output farm_light;
output farm_start_timer;
output enable_hwy;
boolean wire car_present;
wire short_timer, long_timer;
wire farm_start_timer;
wire enable_hwy;
wire enable_farm;
color reg farm_light;
initial farm_light = RED;
assign farm_start_timer = (((farm_light == GREEN)
&& ((car_present == NO) || long_timer))
||
(farm_light == RED) && enable_farm);
assign enable_hwy = ((farm_light == YELLOW) && short_timer);
always @(posedge clk) begin
case (farm_light)
GREEN:
if ((car_present == NO) || long_timer) farm_light = YELLOW;
YELLOW:
if (short_timer) farm_light = RED;
RED:
if (enable_farm) farm_light = GREEN;
endcase
end
endmodule
/*
* Highway light stays RED until it is enabled by the farm control. At
* this point, it resets the timer, and moves to GREEN. It stays in GREEN
* until there are cars and the long timer expires. At this point, it
* moves to YELLOW and resets the timer. It stays in YELLOW until the short
* timer expires. At this point, it moves to RED and enables the farm
* controller.
*/
module hwy_control(clk, car_present, enable_hwy, short_timer, long_timer,
hwy_light, hwy_start_timer, enable_farm);
input clk;
input car_present;
input enable_hwy;
input short_timer;
input long_timer;
output hwy_light;
output hwy_start_timer;
output enable_farm;
boolean wire car_present;
wire short_timer, long_timer;
wire hwy_start_timer;
wire enable_farm;
wire enable_hwy;
color reg hwy_light;
initial hwy_light = GREEN;
assign hwy_start_timer = (((hwy_light == GREEN)
&& ((car_present == YES) && long_timer))
||
(hwy_light == RED) && enable_hwy);
assign enable_farm = ((hwy_light == YELLOW) && short_timer);
always @(posedge clk) begin
case (hwy_light)
GREEN:
if ((car_present == YES) && long_timer) hwy_light = YELLOW;
YELLOW:
if (short_timer) hwy_light = RED;
RED:
if (enable_hwy) hwy_light = GREEN;
endcase
end
endmodule
#The timer leaves state START non-deterministically. This constraint
#prevents it from staying in START forever, without leaving.
!(timer.state=START);
#The timer leaves state SHORT non-deterministically. This constraint
#prevents it from staying in SHORT forever, without leaving.
!(timer.state=SHORT);
#Buechi fairness correct
monitor.fair=1;
This archive was generated by hypermail 2b30 : Thu Feb 21 2002 - 01:58:51 MST