formal verification stuff

fsm/rtl/top.v

@@ -56,6 +56,44 @@ module top(i_clk, o_led, lcol1);
       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)