// This is a testcase that shows false assertion firing,
// due to intra-timestep value fluxuations.
// Run this on your favorite verilog simulator.
// To model strobe semantics (which have the same problem) use
// the argument +define+STROBE 

// To prevent the problem, use +define+STROBE+PREVENT to disable any
// previously started assertions (from the same timestep.)

module intra;

  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;
    rs1a = 1'b1;
    s2   = 1'b0;

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

    @(posedge clk);
    s2   = 1'b1;  // Oops, we have both selects set...
    rs1a = 1'b1;  // Because of the always block below.

    @(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 intra-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

    // 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);
      if (s2) 
        begin
        `ifdef STROBE
          // This part models assert_strobe semantics.
	  -> docheck;
	`else
          // This part models immediate assert semantics.
          $display("Error at time %0d - s1 and s2 are true.", $stime);
	`endif
        end


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

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

  // Model of another combinatorial block of equations.
  always @(rs1a)
    s1a = ~rs1a;

    

endmodule