From 4e192d5d70d89f3107addff976f97fdd2029f5d6 Mon Sep 17 00:00:00 2001 From: Nam Tran Date: Sun, 25 Oct 2020 20:37:32 -0500 Subject: [PATCH] remove strobe parts since it is on its own branch --- fsm-tut4/rtl/top.v | 110 +++++++++++++++++++++------------------------ 1 file changed, 52 insertions(+), 58 deletions(-) diff --git a/fsm-tut4/rtl/top.v b/fsm-tut4/rtl/top.v index 648478b..65432dc 100644 --- a/fsm-tut4/rtl/top.v +++ b/fsm-tut4/rtl/top.v @@ -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