Assertion recursive properties

[bdecelles.ostendo.com]

Hi,

I am trying to create a monitor that counts the number of t_pwm_pin=1 in at the pin output of a design (t_pwm_pin=0 is random). The design could be done simply with an always block and a counter but I am looking for a less memory intensive design that fits with the SVA approach. The design needs about a million instances of the checker.

I am using a recursive property to count using the local variable t_pwm_count the number of t_pwm_pin=1 when t_row_en=1 and after start=1. Unfortunately there does not seem to be any way to debug a recursive property using Questa ATV.

Is the assumption correct - will the SVA use less computer ram than always statements?
Is there a better approach to consider?
How can this local variable t_pwm_pin be viewed?

property p_pwm_value_on(t_pwm_clk_misp, t_pwm_clk, t_pwm_start, t_pwm_pin, t_pwm_value) ;
int t_pwm_count = 0;
@(posedge t_pwm_clk_misp)
  disable iff(t_rst|| !t_pwm_row_en)
      $rose(t_pwm_start) |-> 
        p_check_pwm_on(t_pwm_pin, t_pwm_value, t_pwm_count)            
endproperty
         
         
property p_check_pwm_on( t_pwm_pin, t_pwm_value, t_pwm_count) ;  
  if (t_pwm_row_en==1'b1 && t_pwm_pin == BIT1) ( 
    (t_pwm_count+1) |=> p_check_pwm_on(t_pwm_pin, t_pwm_value, t_pwm_count) 
  )
  else if (t_pwm_row_en==1'b1) ( 
    1'b1 |=> p_check_pwm_on(t_pwm_pin, t_pwm_value, t_pwm_count) 
  )
  else (
    1'b1 |=> (t_pwm_count == t_pwm_value[0]  * DB0 +
                            t_pwm_value[1]  * DB1 +
                            t_pwm_value[2]  * DB2 +
                            t_pwm_value[3]  * DB3 +
                            t_pwm_value[4]  * DB4 +
                            t_pwm_value[5]  * DB5 +
                            t_pwm_value[6]  * DB6 +
                            t_pwm_value[7]  * DB7 +
                            t_pwm_value[8]  * DB8 +
                            t_pwm_value[9]  * DB9 +
                            t_pwm_value[10] * DB10 +
                            t_pwm_value[11] * DB11   ) 
  )      
endproperty 

Thanks,
Bryan

[user49]

In reply to bdecelles@ostendo.com:
I was never a proponent of recursive properties as they are difficult to understand and debug.
Recursive properties are definitely brain teasers.

The design could be done simply with an always block and a counter but I am looking for a less memory intensive design that fits with the SVA approach. The design needs about a million instances of the checker.

Have you considered putting your always block inside a SystemVerilog checker? You can then instantiate the checker in a manner similar to a concurrent assertion.
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
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• 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
• 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

---

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy

[bdecelles.ostendo.com]

In reply to ben@SystemVerilog.us:

Hi Ben,

I have not seen any example with the always block inside the checker. This would help some as the checker would only be active after the qualifiers. Is there is an example you can send.
disable iff(t_rst|| !t_pwm_row_en)
$rose(t_pwm_start) |->

I build the simpler checker with an always block for a faction of the design and am waiting for it to complete simulation in order to see the memory usage, but it is really slowing down the simulation.

Many conditions are checked for the test cases with a known relationship of the low and high times for the PWM signal (property below). This might need to be good enough.

// BIT0, D*, DB* are localparam

property p_pwm_value(t_pwm_clk_misp, t_pwm_clk, t_pwm_start, t_pwm_pin, t_pwm_value) ;
@(posedge t_pwm_clk_misp)
disable iff(t_rst || !t_pwm_row_en)
$rose(t_pwm_start) |->
(t_pwm_pin==BIT0) [*D0] ##1 (t_pwm_pin==t_pwm_value[0]) [DB0] ##1
(t_pwm_pin==BIT0) [(D1-1):D1] ##1 (t_pwm_pin==t_pwm_value[1]) [*DB1] ##1
(t_pwm_pin==BIT0) [*D2] ##1 (t_pwm_pin==t_pwm_value[2]) [*DB2] ##1
(t_pwm_pin==BIT0) [*D3] ##1 (t_pwm_pin==t_pwm_value[3]) [DB3] ##1
(t_pwm_pin==BIT0) [(D4-1)] ##1 (t_pwm_pin==t_pwm_value[4]) [*DB4] ##1
(t_pwm_pin==BIT0) [*D5] ##1 (t_pwm_pin==t_pwm_value[5]) [DB5] ##1
(t_pwm_pin==BIT0) [(D6-1)] ##1 (t_pwm_pin==t_pwm_value[6]) [*DB6] ##1
(t_pwm_pin==BIT0) [*D7] ##1 (t_pwm_pin==t_pwm_value[7]) [DB7] ##1
(t_pwm_pin==BIT0) [(D8-1)] ##1 (t_pwm_pin==t_pwm_value[8]) [*DB8] ##1
(t_pwm_pin==BIT0) [*D9] ##1 (t_pwm_pin==t_pwm_value[9]) [DB9] ##1
(t_pwm_pin==BIT0) [(D10-1)] ##1 (t_pwm_pin==t_pwm_value[10]) [*DB10] ##1
(t_pwm_pin==BIT0) [*D11] ##1 (t_pwm_pin==t_pwm_value[11]) [*DB11]
endproperty

[user49]

In reply to bdecelles@ostendo.com:

In reply to ben@SystemVerilog.us:
Hi Ben,
I have not seen any example with the always block inside the checker. This would help some as the checker would only be active after the qualifiers. Is there is an example you can send.
disable iff(t_rst|| !t_pwm_row_en)
$rose(t_pwm_start) |->
I build the simpler checker with an always block for a faction of the design and am waiting for it to complete simulation in order to see the memory usage, but it is really slowing down the simulation.
Many conditions are checked for the test cases with a known relationship of the low and high times for the PWM signal (property below). This might need to be good enough.
// BIT0, D*, DB* are localparam
property p_pwm_value(t_pwm_clk_misp, t_pwm_clk, t_pwm_start, t_pwm_pin, t_pwm_value) ;
@(posedge t_pwm_clk_misp)
disable iff(t_rst || !t_pwm_row_en)
$rose(t_pwm_start) |->
(t_pwm_pin==BIT0) [*D0] ##1 (t_pwm_pin==t_pwm_value[0]) [*DB0] ##1
…
endproperty

The SystemVerilog checker has definite rules. From my SVA Handbook below is one page that summarizes the rules.

checker_contents.pdf

• The always is illegal in a checker, you need thealways_ff instead.
• Static assertion. A static assertion is an assertion statement that appears outside procedural code, i.e., not in an always (illegal in a checker), always_ff, initial, or final block; they stand on their own.
• Procedural assertion. A procedural assertion is one that is inside a procedural block, such as one inside an always (illegal in a checker), always_ff, initial, or final block. A final block may only contain immediate assertions, and not concurrent assertions
• There are two types of checker instances.

• - Static checker instance: This represents a checker instantiated outside procedural code.
  -  Procedural checker instance: This represents a checker instantiated in an always_ff, initial, or final procedural statement.
  
  
• checker behavior: see http://SystemVerilog.us/fv/checker_behavior.pdf
• If your always_ff code is more efficient than concurrent assertions, then use a checker.
• If you put a concurrent assertion in a checker, you can then istantiate that checker procedurally in your testbench.

---

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
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• 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
• 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

---

See Paper: VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy

[bdecelles.ostendo.com]

In reply to ben@SystemVerilog.us:

Hi Ben,

Thanks for the information especially the checker_behavior.pdf.
In the end I implemented an always statement to count the number of PWM=1.
It does seem to use more computer RAM but it is not too much for our system.
Here is the code.

property p_pwm_value_on(t_pwm_clk_misp, t_pwm_clk, t_pwm_start, t_pwm_pin, t_pwm_value, t_pwm_count) ;
@(posedge t_pwm_clk_misp)
disable iff(t_rst|| !t_pwm_row_en)
rose(t_pwm_start) |-> @(posedge t_pwm_clk) strong(##[0:] $fell(t_pwm_row_en)
##1 (t_pwm_count == t_pwm_value[0] * DB0 +
t_pwm_value[1] * DB1 +
t_pwm_value[2] * DB2 +
t_pwm_value[3] * DB3 +
t_pwm_value[4] * DB4 +
t_pwm_value[5] * DB5 +
t_pwm_value[6] * DB6 +
t_pwm_value[7] * DB7 +
t_pwm_value[8] * DB8 +
t_pwm_value[9] * DB9 +
t_pwm_value[10] * DB10 +
t_pwm_value[11] * DB11 ))
endproperty

always @(posedge t_pwm_clk) begin
if (t_rst || t_pwm_pn_start) begin
t_pwm_count_p0 <= 'b0;
end
else if (t_pwm_row_en) begin
if (t_pwm_p0_pin==BIT1)
t_pwm_count_p0 <= t_pwm_count_p0 + 1’b1;
end
end

a_pwm_value_on_p0 : assert property(p_pwm_value_on(t_pwm_clk_misp, t_pwm_clk, t_pwm_start_en, t_pwm_p0_pin, t_pwm_value_p0, t_pwm_count_p0))
else $error(“ASSERTION ERROR : a_pwm_value_p0, R_ID=%0d, C_ID=%0d\n”, R_ID, C_ID);