traffic_light.v
· 1.9 KiB · Coq
Raw
module top (
input clk,
input rst,
output reg red,
output reg yellow,
output reg green
);
localparam CLK_CYCLES_PER_SECOND = 27000000;
localparam
S_RED = 2'b00,
S_RED_YELLOW = 2'b01,
S_GREEN = 2'b10,
S_YELLOW = 2'b11;
reg [31:0] counter;
reg [31:0] wait_time;
reg [1:0] state, next_state;
function [31:0] get_wait_time;
input [1:0] s;
begin
case (s)
S_RED: get_wait_time = 5 * CLK_CYCLES_PER_SECOND;
S_RED_YELLOW: get_wait_time = 1 * CLK_CYCLES_PER_SECOND;
S_GREEN: get_wait_time = 5 * CLK_CYCLES_PER_SECOND;
S_YELLOW: get_wait_time = 1 * CLK_CYCLES_PER_SECOND;
default: get_wait_time = 5 * CLK_CYCLES_PER_SECOND;
endcase
end
endfunction
always @(posedge clk) begin
if (~rst) begin
state <= S_RED;
end else
state <= next_state;
wait_time <= get_wait_time(next_state);
end
always @(posedge clk) begin
if (~rst)
counter <= 0;
else if (counter < wait_time)
counter <= counter + 1;
else
counter <= 0;
end
always @(*) begin
next_state = state;
if (counter >= wait_time)
case (state)
S_RED: next_state = S_RED_YELLOW;
S_RED_YELLOW: next_state = S_GREEN;
S_GREEN: next_state = S_YELLOW;
S_YELLOW: next_state = S_RED;
default: next_state = S_RED;
endcase
end
always @(posedge clk) begin
if (~rst) begin
red <= 1'b0;
yellow <= 1'b0;
green <= 1'b0;
end else begin
red <= ~(state == S_RED || state == S_RED_YELLOW);
yellow <= ~(state == S_RED_YELLOW || state == S_YELLOW);
green <= ~(state == S_GREEN);
end
end
endmodule
| 1 | module top ( |
| 2 | input clk, |
| 3 | input rst, |
| 4 | output reg red, |
| 5 | output reg yellow, |
| 6 | output reg green |
| 7 | ); |
| 8 | |
| 9 | localparam CLK_CYCLES_PER_SECOND = 27000000; |
| 10 | |
| 11 | localparam |
| 12 | S_RED = 2'b00, |
| 13 | S_RED_YELLOW = 2'b01, |
| 14 | S_GREEN = 2'b10, |
| 15 | S_YELLOW = 2'b11; |
| 16 | reg [31:0] counter; |
| 17 | reg [31:0] wait_time; |
| 18 | reg [1:0] state, next_state; |
| 19 | |
| 20 | function [31:0] get_wait_time; |
| 21 | input [1:0] s; |
| 22 | begin |
| 23 | case (s) |
| 24 | S_RED: get_wait_time = 5 * CLK_CYCLES_PER_SECOND; |
| 25 | S_RED_YELLOW: get_wait_time = 1 * CLK_CYCLES_PER_SECOND; |
| 26 | S_GREEN: get_wait_time = 5 * CLK_CYCLES_PER_SECOND; |
| 27 | S_YELLOW: get_wait_time = 1 * CLK_CYCLES_PER_SECOND; |
| 28 | default: get_wait_time = 5 * CLK_CYCLES_PER_SECOND; |
| 29 | endcase |
| 30 | end |
| 31 | endfunction |
| 32 | |
| 33 | always @(posedge clk) begin |
| 34 | if (~rst) begin |
| 35 | state <= S_RED; |
| 36 | end else |
| 37 | state <= next_state; |
| 38 | wait_time <= get_wait_time(next_state); |
| 39 | end |
| 40 | |
| 41 | always @(posedge clk) begin |
| 42 | if (~rst) |
| 43 | counter <= 0; |
| 44 | else if (counter < wait_time) |
| 45 | counter <= counter + 1; |
| 46 | else |
| 47 | counter <= 0; |
| 48 | end |
| 49 | |
| 50 | always @(*) begin |
| 51 | next_state = state; |
| 52 | if (counter >= wait_time) |
| 53 | case (state) |
| 54 | S_RED: next_state = S_RED_YELLOW; |
| 55 | S_RED_YELLOW: next_state = S_GREEN; |
| 56 | S_GREEN: next_state = S_YELLOW; |
| 57 | S_YELLOW: next_state = S_RED; |
| 58 | default: next_state = S_RED; |
| 59 | endcase |
| 60 | end |
| 61 | |
| 62 | always @(posedge clk) begin |
| 63 | if (~rst) begin |
| 64 | red <= 1'b0; |
| 65 | yellow <= 1'b0; |
| 66 | green <= 1'b0; |
| 67 | end else begin |
| 68 | red <= ~(state == S_RED || state == S_RED_YELLOW); |
| 69 | yellow <= ~(state == S_RED_YELLOW || state == S_YELLOW); |
| 70 | green <= ~(state == S_GREEN); |
| 71 | end |
| 72 | end |
| 73 | endmodule |
| 74 |