Assertion after reset

SystemVerilog
,
1

How to write assertion after reset condition to check if any of the output signal become X or Z during simulation.

2

In reply to vatsaldwivedi:

assert property (@(posedge clock) disable iff (reset) $isunknown({list_of_output_signals}) );
3

In reply to dave_59:
$isunknown (data);
// Returns true if any bit of the vector is X or Z
// Same as $countbits(data,‘X,‘Z)
Thus, in the assertion you want to assert that the correct expectation is that it is NOT unknown.


// Correct
assert property (@(posedge clock) disable iff (reset) !$isunknown({list_of_output_signals}) );
// Other options, from my SystemVerilog Assertions Handbook 
// If coverage is true, then an X or a Z was observed
cp_aXZ: cover property(@ (posedge clk iff smpl) $isunknown(a));
// An assertion can also be written to flag when the variable a is X or Z.
ap_aNoXZ: assert property(@ (posedge clk iff smpl) $isunknown(a)==0);
// The other solution is to use coverpoints, such as:
covergroup a_is_x_cg;
type_option.merge_instances = 0;
option.per_instance = 1;
option.get_inst_coverage = 1;
cp_unknown: coverpoint $isunknown(a)==0; // ($isunknown ==0) i.e. true then no X or Z
cp_with_countbits: coverpoint countbits(a) ==0 ;
cp_with_countbits_axz: coverpoint $countbits (a, 'x, 'z) ==0; // 1800-2012
// ($countbits (a, 'x, 'z) ==0) then no X or Z
endgroup

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
4

In reply to dave_59:

Is there a way to print the signals for which $isunknown is failing?

5

In reply to abhi9891:

  • The “list_of_output_signals” is an expression (e.g., an int, logic[10:0]). It is NOT a list of signals ( (it is not (a, b, c) $isunknown({list_of_output_signals})
  • You can use the concatenation operator to create a vector, as shown below:
 
bit_vector_function ::=
$countbits ( expression , list_of_control_bits )
| $countones ( expression )
| $onehot ( expression )
| $onehot0 ( expression )
| $isunknown ( expression )
 logic db, a, b=0, c; 
   ap_isX: assert property(@(posedge(clk)) $isunknown({a, b, c}))
     $display("{a, b, c}= %b ", $sampled({a, b, c})); 

    ap_isXa: assert property(@(posedge(clk)) $isunknown(a))
     $display("a= %b", $sampled(a)); 

simulation results: 
# a= x
# {a, b, c}= x0x 
# {a, b, c}= x0x 
# a= x
# {a, b, c}= x0x 
# a= x

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy
6

In reply to ben@SystemVerilog.us:

Thanks

7

In reply to dave_59:

hai, dave, if I am using disable iff condition how it works? can you explain?

the scenario is: there is a signal called(grant) where it can be asserted at any time after reset and once it is asserted no x or z values should be propagated.

for example 1. when my reset is high (write and read transaction should happen), if reset is low then every trnsactn shuld stop at any instant of time.

for this, I have written
property p;
(@(posedge clk) disable iff(reset) !$isunknown(grant);
endproperty
a1: assert property(p) $display(" grant=%0b", $sampled(grant)); else $error("x or z ")

is that correct

8

In reply to ben@SystemVerilog.us:

hai ben,

disable iff(reset) // what does it means? does it mean if reset==1 assertion pass or assertion is failed ?
and one more question $isunknown(a) // what does it mean? does it mean if any unknown are found will it neglect or it will catch?

9

In reply to vickyvinay:

property p;
(@(posedge clk) disable iff(reset) !$isunknown(grant);
endproperty
a1: assert property(p) $display(" grant=%0b", $sampled(grant)); else $error("x or z ")

Your assertion stops if reset becomes high.
If you want the assertion to be stop checking when reset=0, use disable iff(!reset)