Verifying values a and b values using assertions

SystemVerilog
,
1

Suppose when bit a is high then next cycle, bit [1:0]b is 11 in first cycle and second cycle is b=00 and third cycle b=11… Continuous, suppose in between a=0 then again whenever ‘a’ becomes 1 then b value is 11 and then continuous same as above??
please help me how to write assertion for this or any alternate solution available for this?

2

In reply to Subbi Reddy:
I suggest that you take an attempt at a solution. I’ll be glad to review it.
If you fail at even an attempt, then you should seriously study SVA.
Ben SystemVerilog.us

3

Please verify below code:

property a_is_active;
(a |=> b) || (a |=>(!b));
b= ~b;
endproperty
property a_is_in_active;
b=2’b11;
endproperty
// See the OR operator
property a_b_prop;
@ (posedge clk)
if (a==1)
a_is_active
else
a_is_in_active;
endproperty

a_b_prop_assert : assert property (a_b_prop);

4

In reply to Subbi Reddy:
Your requirements are ambiguous. I provided a solution that HAS ISSUES as explained below.
requirements: When bit “a” is high then at the next cycle
bit [1:0]b ==11 ##1 b==00 ##1 b=11 ##1 b=00 …
When a=0 then b==00


t  1   2   3   4   5   6   7 
a  0   0   1   1   1   1   0   1   0   0   1   1   1   
            \   \
             \ OK \
              \    \ BAD
b  11  11  11  11  00  11  11  11  11  11  11  00  11 
** ISSUE 
@t2 attempt a==0, then b==11  // OK 
@t3 attempt a==1, requires b==11 at t4, b==00 @t5, 
@t4 attempt a==1,              requires b==11 @t5
// Can't have at t5 b==11 and b==00 at the same time !!!!

Here is a solution that does have issues


   // [1] $stable returns true if the sampled value of the expression did not change between 
   // the sampled value at the previous cycle and the sampled value at the current cycle. 
   //Otherwise, it returns false. $changed is a complement to $stable; $changed returns true 
   // if the sampled value of the expression changed.
// ************ EDITED THIS FUNCTION ****************
    function bit[1:0] b_changed(bit[1:0] x);
     if($past(x==2'b00,1 , 1, @(posedge clk) ) && x==2'b11)return 1; 
     else if ($past(x==2'b11, 1, 1, @(posedge clk) ) && x==2'b00) return 1; 
     else return 0; 
   endfunction
   // $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])



   property a_is_active;
     // a |=> b==2'b11 ##1 $changed(b)[*1:$] ##1 !a; // was a consideration 
     a |=> b==2'b11 ##1 b_changed(b)[*1:$] ##1 !a;
     // ** ISSUE HERE as explained above  

    // (a |=> b) or (a |=>(!b));// (a |=> b) || (a |=>(!b)); // need the sequential "or" 
    // b= ~b ; ??  
    endproperty

    property a_is_in_active;
      b==2'b11;
    endproperty

    property a_b_prop;
      @ (posedge clk)
        if (a==1)
          a_is_active
        else
          a_is_in_active;
    endproperty
    
    a_b_prop_assert : assert property (a_b_prop);

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

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
5

In reply to ben@SystemVerilog.us:

Edited the function above to

function bit[1:0] b_changed(bit[1:0] x);
     if($past(x==2'b00,1 , 1, @(posedge clk) ) && x==2'b11)return 1; 
     else if ($past(x==2'b11, 1, 1, @(posedge clk) ) && x==2'b00) return 1; 
     else return 0; 
   endfunction
   // $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
6

I agree with you when a is active

we are trying forcibly b=2’b11 when a is in_active, why we want to change b value when a is in_active, lets try to keep b value same when a is in_active

Ex: the b value is 2’b00 when before a is in_active, a is in_active state more than 5 cycles, in 5 cycles b value is 2’b11, as per my knowledge its incorrect to change b value??

can we write when a is in_active like:
property a_is_in_active
(b || !b) ##1 1[*0:$] ##1 1->(a && x==2’b11);
endproperty

7

In reply to Subbi Reddy:
Sorry, but your requirements are very ambiguous.

I’ll comment on the structure of your proposed solution:


(b || !b) ##1 1[*0:$] ##1 1->(a && x==2'b11);
// 
(b || !b) is always true ( yet the ORING of 0,1)
1[*0:$] ##1 1 is same 1 // SVA rules on repeats with [*0
// Property gets reduced to 
1 ##1   1->(a && x==2'b11); // same as 
 ##1   1->(a && x==2'b11); // after the very first cycle, is same as  
(a && x==2'b11); 
// I don't know if that meets your ambiguous requirements.

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

** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers: