Assertion not getting hit even conditions are matched and true

SystemVerilog
, ,
1

Hi,
I’m trying to write an assertion for below condition. However, my assertion is not getting hit.

Precondition: a_read and a_bit should be high
condition: whenever we have precondition matched, if we see b_read high and at the same time b_load should not be there, then in next cycle b_bit should go low then following cycle a_bit should go low

property fp_clear();
        @(posedge clk)
            disable iff(~rst_b)
            (a_read & a_bit) ##0 first_match(##[1:$] (b_read)) ##0 (~b_load) |=> (b_bit == 0) ##1(a_bit == 0);

endproperty
2

This is what I think you wnat based on your requirements:

 // If  (a_read && a_bit) then at the first_match(##[1:$] b_read && !b_load ##1 b_bit == 0 ##1  a_bit == 0) we met the requirements
  (a_read && a_bit) |-> first_match(##[1:$] b_read && !b_load ##1 b_bit == 0 ##1  a_bit == 0);

Also, use the logical operators for negation or anding instead of the bitwise operators.
Thus use !a instead of ~a
Use && insted of &
Why? it is more readable, at least for those who know SystemVerilog

3

Antecedent should cover first_match as well.

(a_read & a_bit) should be there and then if (b_read) comes and at the same time (b_load==0) then only check for (b_bit ==0) in next cycle and then following cycle check for (a_bit==0)

4 
(a_read & a_bit) ##0 first_match(##[1:$] (b_read)) ##0 (~b_load) |=> ..
when (a_read & a_bit) is a match 
and 
 ##0 first_match(##[1:$] (b_read)) is a match 
and  ##0 (~b_load) is a **NO match**
 **Then the assertion completes vacuously**-
-------------
first_match( a_read & a_bit ##[1:$] b_read ##0 !b_load) |=> ..
when (a_read & a_bit) is a match 
and 
 (##[1:$] (b_read)) is a match 
and  ##0 (!b_load) is a **NO match**
 **Then the assertion completes KEEPS ON LOOKING FOR A MATCH**-

I understood your Requirement to be this instead.
(a_read && a_bit) |-> first_match(##[1:$] b_read && !b_load ##1 b_bit == 0 ##1
5

I tried your suggestion. Still, property is not hitting.

This is what I tried:

(a_read & a_bit) |-> first_match(##[1:$] (b_read && !b_load) ##1 (b_bit == 0) ##1 (a_bit == 0);
6 
SVA: ##[1:$], the often forgotten rules
Q1: What's wrong with this code? Need a first_match?
(a_read & a_bit) |-> 
 ##[1:$] (b_read && !b_load) ##1 (b_bit == 0);
A1: A consequent sequence with a ##[1:$] can only succeed; it can never fail. 
Here, the ##[1:$] is the ORing of an infinite number of threads, and the search 
is for a successful match. Upon any match, the consequent terminates and the assertion is true. 
The first_match(##[1:$] SEQUENCE) is of no value here, we're looking for a match. 
// Something like this is better because it can pass or fail 
(a_read & a_bit) |-> 
 (b_read && !b_load)[->1] ##1 (b_bit == 0); 
It says if (a_read & a_bit) then at the 1st and only possible occurrence of 
(b_read && !b_load) we must have in the next cycle (b_bit == 0) 

Q2: What's wrong with this code? Need a first_match?
(a_read & a_bit) ##[1:$] (b_read && !b_load) |-> ##1 (b_bit == 0);
A2: A antecedent sequence with a ##[1:$] can only fail; it can never succeed. 
Here, the ##[1:$] is the ORing of an infinite number of threads, 
and for the property to be true it is required that ALL POSSIBLE threads 
of the antecedent be tested along with consequent, and each property of that thread 
must be true, vacuously or nonvacuously. 
 
The first_match(##[1:$] SEQUENCE) IS of value here because a match of the antecedent
stops the search. Any non-matched antecedent makes that property for that thread vacuous.
THUS: 
1. OK, but not recommended style because because the first_match is a burden on the simulator
first_match((a_read & a_bit) ##[1:$] (b_read && !b_load)) |-> ##1 (b_bit == 0);
2. Recommended style with the goto operator. 
(a_read & a_bit) ##0 (b_read && !b_load)[->1] |-> ##1 (b_bit == 0); 
3. DO NOT USE THE GOTO as the 1st term of the antecedent, 
 it creates unnecessary threads. Thus, 
 BAD: a[->1] ##1 b[->1] |-> c; // May need $rose(a) 
 GOOD: a ##1 b[->1] |-> c;
I explain all of this in my paper: Understanding the SVA Engine Using the Fork-Join Model
https://lnkd.in/gAZzHGn
Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total
independence of attempts