`default_nettype  none

module top(i_clk, o_led, lcol1);
   parameter WIDTH = 22;
   input wire i_clk;
   output reg [7:0] o_led;
   output wire lcol1;

   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 [7:0] obuf; // output buffer, take into account the icefun use active low LED
   reg [3:0] led_index;
   reg strobe;

   initial begin
      obuf = 8'h1;
      {strobe, counter} = 0;
      led_index = 0;
   end

   always @(posedge clk_12MHz)
      {strobe, counter} <= counter + 1'b1;

   // fsm
   always @(posedge clk_12MHz) begin
      if (strobe) // led_index change only when strobe is 1
         if (led_index >= 4'hd)
            led_index <= 0;
         else
            led_index <= led_index + 1'b1;

      case (led_index)
         4'h0: obuf <= 8'h01;
         4'h1: obuf <= 8'h02;
         4'h2: obuf <= 8'h04;
         4'h3: obuf <= 8'h08;
         4'h4: obuf <= 8'h10;
         4'h5: obuf <= 8'h20;
         4'h6: obuf <= 8'h40;
         4'h7: obuf <= 8'h80;
         4'h8: obuf <= 8'h40;
         4'h9: obuf <= 8'h20;
         4'ha: obuf <= 8'h10;
         4'hb: obuf <= 8'h08;
         4'hc: obuf <= 8'h04;
         4'hd: obuf <= 8'h02;
         default : begin
            obuf <= 8'h01;
         end
      endcase
   end

`ifdef	FORMAL
   // led_index should never go beyond 13
	always @(*)
		assert(led_index <= 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(obuf)
         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
   /* shift reg
   // shifting bit
   always @(posedge clk_12MHz)
      if (strobe)
         obuf <= {obuf[6:0], obuf[7]}; // left shift
         // obuf <= {obuf[0], obuf[7:1]}; // right shift
   */


   always @(posedge clk_12MHz)
      o_led <= ~obuf;

   assign lcol1 = 1'b0;
endmodule

// Local Variables:
// verilog-library-directories:(".." "./rtl" ".")
// End: