remove strobe parts since it is on its own branch

This commit is contained in:
2020-10-25 20:37:32 -05:00
parent 6096187250
commit 4e192d5d70

View File

@@ -19,7 +19,6 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
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;
@@ -30,7 +29,6 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
initial begin
led_buf = 6'h0;
// {strobe, counter} = 0;
counter = 0;
state = 0;
busy_buf = 0;
@@ -46,13 +44,10 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
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;
@@ -64,61 +59,60 @@ module top(i_clk, o_led, o_led_row_0, i_request, o_busy);
// 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;
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
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
`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