// This is a testcase that shows false assertion firing,
// due to intra-timestep value fluxuations.
// Run this on your favorite SystemVerilog simulator.
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


  // Block with out assertion (modeled with a display statement.)
  always @(s1 or s2 or d1 or d2)
    begin
    disable checkit;  // disable any (ALL) previous assertions.

    // This is our model of the antecedent in more complex
    // assertions. This may have been several nested if()'s or
    // a case item, etc.
    // We need assert_strobe to delay the evaluation until all values
    // settle and we need the disable above in case s1 settles to
    // the value 0 (meaning that we shouldn't have run the assertion.
    if (s1) checkit: assert_strobe (! s2);

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

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

    

endmodule