assertion

Immediate Assertion:

design.sv

                                          
module AND_Gate(
  input A,
  input B,
  output Y,
  input clk);
  assign Y = A&&B; 
endmodule

testbench.sv

                                          
module AND_Gate_tb;
reg A;
reg B;
reg clk;
wire Y;

AND_Gate inst(.A(A), .B(B), .Y(Y), .clk(clk));
always #5 clk = ~clk;
initial 
AND_Gate inst(.A(A), .B(B), .Y(Y), .clk(clk));
always #5 clk = ~clk;
initial begin
  clk=0;
  A=0;
  B=0;

  #10
  A=0;
  B=1;
  
  #10
  A=1;
  B=0;
  
  #10
  A=1;
  B=1;

  #15 $finish;
end


  always @(posedge clk) 
  begin 
    assert (A==1 && B==1)
      $display("%0t, A=1 and B=1, assertion pass\n",$time);
    else
      $display("%0t fail\n",$time);
  end
  initial begin
    $dumpfile("waveform.vcd");
    $dumpvars();
  end
endmodule 


``` begin
  clk=0;
  A=0;
  B=0;

  #10
  A=0;
  B=1;
  
  #10
  A=1;
  B=0;
  
  #10
  A=1;
  B=1;

  #15 $finish;
end


  always @(posedge clk) 
  begin 
    assert (A==1 && B==1)
      $display("%0t, A=1 and B=1, assertion pass\n",$time);
    else
      $display("%0t fail\n",$time);
  end
  initial begin
    $dumpfile("waveform.vcd");
    $dumpvars();
  end
endmodule 

Output:

To run assertions we need to add an extra option/Flag in the command called –assert. The modified command is shown below

verilator --binary --assert [testbench_file_name]  

Waveform:

Concurrent Assertion:

                                          
module overlapped_assertion;
  bit clk,a,b,valid;
  
  always #5 clk = ~clk; //clock generation
  
  //generating 'a'
  initial begin
    valid=1;
        a=1; b=1;
    #15 a=1; b=0;
    #10 b=1;
    #12 b=0;
    #10 a=0; b=1;
    valid=0;
    #15 a=1; b=0;
    #100 $finish;
  end
  
  property p;
    @(posedge clk) valid |-> (a ##3 b);
  endproperty
  
  //calling assert property
  a_1: assert property(p)
    $info("pass");
    else
      $info("fail");

      initial begin
        $dumpfile("waveform.vcd");
        $dumpvars();
      end
    
endmodule

ERROR

Note: Verilator does not support sequences and variable delay assertions. It only supports simple expressions in assertions.