Assertions

SystemVerilog
,
1

hello, I try to verify AND gate design using assertion.Iam not getting correct as I expected.The assertion passed only for this condition (a && b) |-> y;

I am getting output like this in waveform.
#10 a=0;b=1; =============failed
#10 a=0;b=0; =============Inactive
#10 a=1;b=0; =============failed
#10 a=1;b=1; =============success

here what is “Inactive” means??

note:;Iam using cadence tool
////////////////////////////////////////////////////////////////

module test(a,b,y);
input a,b;
output reg y;

bit clock;

always@(a,b)
begin
y=a&b;
end

initial
begin
clock=1’b0;
forever
#5 clock=~clock;
end

property s1;
@(posedge clock)
$rose(a) || $rose(b) |-> !y or (a && b) |-> y;
endproperty

P1:assert property(s1);
/*sequence d1;
(a || b) ##1 !y;
endsequence

sequence d2;
(a && b) ##1 y;
endsequence

P1:assert property(s1);

property s1;
@(posedge clock)

(d1) or (d2);
endproperty*/

endmodule

module tb();
reg a,b;
wire y;

test DUT(a,b,y);

initial
begin
#10 a=0;b=1;
#10 a=0;b=0;
#10 a=1;b=0;
#10 a=1;b=1;

end

initial
#100 $finish;

endmodule

2

In reply to surya narayana Gutha:
I strongly suggest that you get a good book with thorough explanations on assertions along with lots of examples and methodologies; may I suggest my book * SVA Handbook 4th Edition, 2016 ISBN 978-1518681448, though with self-interest, but it has been widely accepted by many well-known companies and is the culmination of the work of 4 authors who are well integrated and experts in this industry, with lots of design, verification, and tool development experiences.

Getting back to your question, you first need to understand the definition of a property, you really need to understand the syntax, as there is a very rich set of possibilities. I’ll consider one of those, specifically:


property_expr ::=
...
| sequence_expr |-> property_expr
  1. If the antecedent sequence_expr does not match, then the property is vacuous and the property_expr is not evaluated. An example of a sequence that does not match:
    a ##1 b, where a==1 and b==0
  2. if the antecedent has multiple threads (implicit or explicit ORing of sequences, then for a success of the property, all threads must be tested.
  3. if the antecedent is true the sequence_expr is evaluated.
  4. Since sequence_expr |-> property_expr IS a property expression, the following is also a property expression:
    sequence_expr |-> sequence_expr |-> property_expr

There really IS a lot more to the story. Get a book!
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr