Files
iceFun_Projects/fsm-tut4/rtl/top.v
2020-10-24 14:29:44 -05:00

128 lines
3.4 KiB
Verilog

`default_nettype none
module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
parameter WIDTH = 22;
input wire i_clk;
output wire [5:0] o_led;
output wire o_led_row_0;
input wire i_request;
output wire o_busy;
wire clk_12MHz;
clk_gen clk_gen_0 (/*autoinst*/
// Outputs
.o_clk (clk_12MHz),
// Inputs
.i_clk (i_clk));
reg [WIDTH-1:0] counter;
reg [3:0] state;
reg [5:0] led_buf; // output buffer, take into account the icefun use active low LED
// reg strobe;
reg busy_buf;
wire req_buf;
assign o_busy = ~busy_buf;
assign o_led = ~led_buf;
assign o_led_row_0 = 1'b0;
assign req_buf = ~i_request;
initial begin
led_buf = 6'h0;
// {strobe, counter} = 0;
counter = 0;
state = 0;
busy_buf = 0;
end
always @(posedge clk_12MHz) begin
if (!busy_buf && req_buf)
busy_buf <= 1;
else
busy_buf <= (state != 4'h0);
end
// counter and strobe run only during busy signal is High
always @(posedge clk_12MHz) begin
if (busy_buf)
counter <= counter + 1'b1;
// {strobe, counter} <= counter + 1'b1;
else
// {strobe, counter} <= 0;
counter <= 0;
end
// state change once strobe starts
always @(posedge clk_12MHz) begin
if (!busy_buf && req_buf)
state <= 4'h1;
else if (state >= 4'hB)
state <= 4'h0;
else if (state != 0)
state <= state + 1'b1;
end
// fsm for led_buf
always @(posedge clk_12MHz) begin
// if (strobe)
case (state)
4'h1: led_buf <= 6'b00_0001;
4'h2: led_buf <= 6'b00_0010;
4'h3: led_buf <= 6'b00_0100;
4'h4: led_buf <= 6'b00_1000;
4'h5: led_buf <= 6'b01_0000;
4'h6: led_buf <= 6'b10_0000;
4'h7: led_buf <= 6'b01_0000;
4'h8: led_buf <= 6'b00_1000;
4'h9: led_buf <= 6'b00_0100;
4'ha: led_buf <= 6'b00_0010;
4'hb: led_buf <= 6'b00_0001;
default: led_buf <= 6'b00_0000;
endcase
end
`ifdef FORMAL
// state should never go beyond 13
always @(*)
assert(state <= 4'hd);
// I prefix all of the registers (or wires) I use in formal
// verification with f_, to distinguish them from the rest of the
// project.
reg f_valid_output;
always @(*)
begin
// Determining if the output is valid or not is a rather
// complex task--unusual for a typical assertion. Here, we'll
// use f_valid_output and a series of _blocking_ statements
// to determine if the output is one of our valid outputs.
f_valid_output = 0;
case(led_buf)
8'h01: f_valid_output = 1'b1;
8'h02: f_valid_output = 1'b1;
8'h04: f_valid_output = 1'b1;
8'h08: f_valid_output = 1'b1;
8'h10: f_valid_output = 1'b1;
8'h20: f_valid_output = 1'b1;
8'h40: f_valid_output = 1'b1;
8'h80: f_valid_output = 1'b1;
endcase
assert(f_valid_output);
// SV supports a $onehot function which we could've also used
// depending upon your version of Yosys. This function will
// be true if one, and only one, bit in the argument is true.
// Hence we might have said
// assert($onehot(o_led));
// and avoided this case statement entirely.
end
`endif
endmodule
// Local Variables:
// verilog-library-directories:(".." "./rtl" ".")
// End: