tests/demo.sv

   1 module demo (
   2   input clk,
   3   output reg [5:0] counter
   4 );
   5   initial counter = 0;
   6
   7   always @(posedge clk) begin
   8     if (counter == 15)
   9       counter <= 0;
  10     else
  11       counter <= counter + 1;
  12   end
  13
  14 `ifdef FORMAL
  15   always @(posedge clk) begin
  16     assert (counter < 7);
  17   end
  18 `endif
  19 endmodule