source: vis_dev/vis-2.1/examples/tlc/tlc.v @ 15

Last change on this file since 15 was 11, checked in by cecile, 13 years ago

Add vis

File size: 6.3 KB
Line 
1/**************************************************************************
2   Adaptation of Mead and Conway traffic light controller.
3
4   A little used farm road intersects with a multi-lane highway; a traffic
5   light controls the traffic at the intersection.
6   The light controller is implemented to maximize the time the highway light
7   remains green.  A submodule implements a timer, which outputs "short" and
8   "long" time outs. The highway light stays green for at least "long" time.
9   Any time after "long" time, if there is a car waiting on the farm road, then
10   the farm light turns green.  The farm light remains green until there are no
11   more cars on the farm road, or until the long timer expires.  The yellow
12   light for both directions stays yellow for "short" time.
13
14   The timer has non-determinism in it.  Liveness properties won't pass until
15   fairness constraints are placed on the timer, so that it can't pause
16   forever.
17
18   Tom Shiple, 25 October 1995
19
20***************************************************************************/ 
21
22/*
23 * Symbolic variables.
24 */
25typedef enum {YES, NO} boolean;
26typedef enum {START, SHORT, LONG} timer_state;
27typedef enum {GREEN, YELLOW, RED} color;
28
29/*
30 * Module main ties together the underlying modules.  In addition, it
31 * ORs together the start timer outputs of the farm road and highway
32 * controllers.  Note that only a single timer is used for both the farm
33 * road and highway controllers. In theory, this could lead to conflicts; as
34 * implemented, such conflicts are avoided.
35 */
36module main(clk);
37input clk;
38
39color wire farm_light, hwy_light;
40wire start_timer, short_timer, long_timer;
41boolean wire car_present;
42wire enable_farm, farm_start_timer, enable_hwy, hwy_start_timer;
43
44assign start_timer = farm_start_timer || hwy_start_timer;
45
46timer timer(clk, start_timer, short_timer, long_timer);
47sensor sensor(clk, car_present);
48farm_control farm_control(clk, car_present, enable_farm, short_timer, long_timer, 
49        farm_light, farm_start_timer, enable_hwy);
50hwy_control  hwy_control (clk, car_present, enable_hwy,  short_timer, long_timer, 
51        hwy_light, hwy_start_timer, enable_farm);
52
53
54endmodule
55
56
57/*
58 * There is a single, coupled sensor that detects the presence of a car
59 * in either direction of the farm road.  At each clock tick, it non-
60 * deterministically reports that a car is present or not.
61 */
62module sensor(clk, car_present);
63input clk;
64output car_present;
65
66wire rand_choice;
67boolean reg car_present;
68
69initial car_present = NO;
70
71assign rand_choice = $ND(0,1);
72
73always @(posedge clk) begin
74    if (rand_choice == 0) 
75        car_present = NO;
76    else 
77        car_present = YES;
78end
79endmodule
80
81
82/*
83 * From the START state, the timer produces the signal "short"
84 * after a non-deterministic amount of time. The signal "short"
85 * remains asserted until the timer is reset (via the signal "start").
86 * From the SHORT state, the timer produces the signal "long"
87 * after a non-deterministic amount of time. The signal "long"
88 * remains asserted until the timer is reset (via the signal "start").
89 * The following Buchi fairness constraints should be used:
90 *
91 *  !(timer.state=START);
92 *  !(timer.state=SHORT);
93 */
94module timer(clk, start, short, long);
95input clk;
96input start;
97output short;
98output long;
99
100wire rand_choice;
101wire start, short, long;
102timer_state reg state;
103
104initial state = START;
105
106assign rand_choice = $ND(0,1);
107
108/* short could as well be assigned to be just (state == SHORT) */
109assign short = ((state == SHORT) || (state == LONG));
110assign long  = (state == LONG);
111
112always @(posedge clk) begin
113        if (start) state = START;
114        else 
115                begin
116                case (state)
117                START: 
118                        if (rand_choice == 1) state = SHORT;
119                SHORT: 
120                        if (rand_choice == 1) state = LONG;
121                /* if LONG, remains LONG until start signal received */
122                endcase
123                end
124end
125endmodule
126
127
128/*
129 * Farm light stays RED until it is enabled by the highway control. At
130 * this point, it resets the timer, and moves to GREEN.  It stays in GREEN
131 * until there are no cars, or the long timer expires.  At this point, it
132 * moves to YELLOW and resets the timer.  It stays in YELLOW until the short
133 * timer expires.  At this point, it moves to RED and enables the highway
134 * controller.
135 */
136module farm_control(clk, car_present, enable_farm, short_timer, long_timer, 
137        farm_light, farm_start_timer, enable_hwy);
138input clk;
139input car_present;
140input enable_farm;
141input short_timer;
142input long_timer;
143output farm_light;
144output farm_start_timer;
145output enable_hwy;
146
147boolean wire car_present;
148wire short_timer, long_timer;
149wire farm_start_timer;
150wire enable_hwy;
151wire enable_farm;
152
153color reg farm_light;
154
155initial farm_light = RED;
156
157assign farm_start_timer = (((farm_light == GREEN) 
158                                && ((car_present == NO) || long_timer))
159                            ||
160                            (farm_light == RED) && enable_farm);
161assign enable_hwy = ((farm_light == YELLOW) && short_timer);
162
163always @(posedge clk) begin
164        case (farm_light)
165        GREEN:
166                if ((car_present == NO) || long_timer) farm_light = YELLOW;
167        YELLOW:
168                if (short_timer) farm_light = RED;
169        RED:
170                if (enable_farm) farm_light = GREEN;
171        endcase
172end
173endmodule
174
175
176/*
177 * Highway light stays RED until it is enabled by the farm control. At
178 * this point, it resets the timer, and moves to GREEN.  It stays in GREEN
179 * until there are cars and the long timer expires.  At this point, it
180 * moves to YELLOW and resets the timer.  It stays in YELLOW until the short
181 * timer expires.  At this point, it moves to RED and enables the farm
182 * controller.
183 */
184module hwy_control(clk, car_present, enable_hwy, short_timer, long_timer, 
185        hwy_light, hwy_start_timer, enable_farm);
186input clk;
187input car_present;
188input enable_hwy;
189input short_timer;
190input long_timer;
191output hwy_light;
192output hwy_start_timer;
193output enable_farm;
194
195boolean wire car_present;
196wire short_timer, long_timer;
197wire hwy_start_timer;
198wire enable_farm;
199wire enable_hwy;
200
201color reg hwy_light;
202
203initial hwy_light = GREEN;
204
205assign hwy_start_timer = (((hwy_light == GREEN) 
206                                && ((car_present  == YES) && long_timer))
207                            ||
208                            (hwy_light == RED) && enable_hwy);
209
210assign enable_farm = ((hwy_light == YELLOW) && short_timer);
211
212always @(posedge clk) begin
213        case (hwy_light)
214        GREEN:
215                if ((car_present == YES) && long_timer) hwy_light = YELLOW;
216        YELLOW:
217                if (short_timer) hwy_light = RED;
218        RED:
219                if (enable_hwy) hwy_light = GREEN;
220        endcase
221end
222endmodule
Note: See TracBrowser for help on using the repository browser.