// This is a testcase that shows false assertion firing,
// due to inter-timestep value fluxuations.
// Run this on your favorite verilog simulator.

// To prevent the problem, use +define+PREVENT to disable any
// previously started assertions. This will kill any erroneously
// started ones.

module inter;

  reg rs1, rs1a, s2, s3;

  reg do, d1, d2;

  reg tmp, s1a;

  reg clk;
  initial
    begin
    clk = 1'b1;
    forever clk = #5 ~clk;
    end

  wire  s1  = rs1 | ~s1a;

initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);

  initial begin
    rs1  <= 1'b0;
    s1a  <= 1'b1;
    s2   <= 1'b0;

    @(posedge clk);
    s1a <= 1'b0;  // Turn on s1.

    @(posedge clk);
    s2  <=    1'b1;    // Oops, we have both selects set...
    s1a <= #1 1'b1;  // Model input delay (from different coding style block.)

    @(posedge clk);

    s2  <= 1'b0;

    repeat (5) @(posedge clk);
    $finish;
    end



  event docheck;
  // Block with out assertion (modeled with a display statement.)
  always @(s1 or s2 or d1 or d2)
    begin
    // This is how one prevents false firings due to inter-timestep
    // value changes. By disabling a previously started assertion
    // it will not fail. NOTE: requiring this kills overlapping 
    // assertions, because disable stops all running blocks/assertions!
    `ifdef PREVENT
    disable checkit;  // disable any (ALL) previous assertions.
    `endif

    `ifdef INTER
    // This is our model of the antecedent in more complex
    // assertions. This may have been several nested if()'s or
    // a case item, etc.
    if (s1) 

      // Model our assertion - //assert never (s1 & s2);
      // This part uses assert (immediate) semantics by checking at the
      // end of the cycle.
	  -> docheck;
    `else
      if (s1) 
      // Model our assertion - //assert never (s1 & s2);
      if (s2) 
        begin
          // This part models assert_strobe semantics.
          -> docheck;
        end
    `endif


    // Our functionality that we are preventing.
    do = s1 & d1 | s2 & d2;
    end

  `ifdef INTER
  // Assert_Strobe model version.
  always @(docheck)
    begin :checkit
    @(posedge clk);
    if (s2)
      $display("Error(1) at time %0d - s1 and s2 are true.", $stime);
    end

  `else

  // Assert_Strobe model version.
  always @(docheck)
    begin :checkit
     #0 $display("Error(2) at time %0d - s1 and s2 are true.", $stime);
     //#0 $display("Error again - was this still running?.");
    end
  `endif

endmodule