SVA, counter with features and formal verification

SystemVerilog
1

So here’s the problem: we have a counter, which after enabled counts signal FOO pulses to 5 and wraps back to 0. Counting stops with HALT.

How to make a property?

Something along the lines like this?


##0 EN
##1 (FOO, count++)[=0:100]
##0 HALT
|=>
RESULT == count

But the above cannot do the wrapping. I restricted the cycle count with [100] since after that we already know that the design is ok. Note that FOO with same time as HALT is also counted.

Should I code a SVA function with wrapping and use that in the property?

2

I did not understand your question fully what i understood is when ever FOO is high count will be incremented by 1 , but you want that count to be wrapped to zero after reaching 5, is that correct?

in that case can you try like this :



##0 EN
##1 (FOO, count=(count==5)?0:count+1)[=0:100]
##0 HALT
|=>
RESULT == count

I am not sure whether that expression works there or not , can you try that ?

3

The following code is from a class that I taught. It is very similar to your requirements, thus you should be able to modify it as needed.
requirements:
// Loadable counter, reset to 0 if reset_n==0,
// Min count -2, Max count ==5
// This is an activity counter, thus count must change at least
// every 8 cycles (i.e., cannot stay forever at max value)

module counter_max #(MAX_COUNT=9, MIN_COUNT=2)( // parameter port list 
            input logic[3:0] data_in, 
            input logic ld, 
            output logic[3:0] counter, 
            input logic clk, rst_n) ;
        int cover_count=0; 
        int fail_count=0; 
        // ap_P:  assert property(@ (posedge clk) P ) 
   
        // parameter MIN_COUNT=2; // module item parameter
        // If use of parameter port list, then can't use defparam 
        default disable iff !rst_n;
                     
        property p_load;
            logic[3:0] v_data_in; // local variable to property 
            (ld, v_data_in=data_in) |=> counter==v_data_in;
        endproperty : p_load
        ap_load: assert property ( @(posedge clk) p_load); 
        	
        ap_count: assert property(@(posedge clk) 
                !ld && (counter!=MAX_COUNT) |=> counter==$past(counter)+1'b1);
            
                
        ap_hold: assert property(@(posedge clk) 
                counter==MAX_COUNT |=> counter==$past(counter)); 
                
        ap_min_load: assume property(@(posedge clk) disable iff (!rst_n) 
            ld |-> not(data_in<MIN_COUNT)); 
        
        ap_max_load: assume property(@ (posedge clk) disable iff(!rst_n)
            ld |-> not(data_in > MAX_COUNT))
            cover_count++; else fail_count++ ;  
        	
                
        ap_statble8: assume property(@(posedge clk) 
            $stable(counter)|-> ##[1:8] !$stable(counter));
    		
        always @(posedge clk) begin : counter1
            if(!rst_n) counter <= 0; 
            else if (ld) counter <= data_in;
            else begin : counter2
                counter <= counter + 1'b1;
            end : counter2
        end : counter1
	
    endmodule : counter_max

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

  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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 cool_cake20:

Thanks for the interesting suggestion. It’s basically a mux inside sequence? Anyway, it does not seem to compute :(

illegal inc/dec operator in sva; only allowed in sequence match items

Also on problem seems to be that EN has be ‘1’ all the time. Otherwise in the design the counters will obviously be reset. I’ve been trying to use “EN throughout ((FOO, count++)[=100)” type of a solution but the tools do not seem to like clk tick “unbounded” sequences with local variables…I then tried “EN[*200] intersect ((FOO, count++)[=100)” but again this seems to be illegal use of local variables.

5

In reply to ben@SystemVerilog.us:

Thanks Ben. I have not yet had the time to trial your mehtod, but there’s one interesting part:

ap_min_load: assume property(@(posedge clk) disable iff (!rst_n) 
            ld |-> not(data_in not(data_in > MAX_COUNT))
            cover_count++; else fail_count++ ;

What is this else part? I have been trying to if/else inside my properties but me and the tools seem to have a different understanding about what I want to achieve.

6

In reply to Jarno:

Looks like an extra “paste”. Should be

ap_min_load: assume property(@(posedge clk) disable iff (!rst_n) 
            ld |-> not(data_in > MAX_COUNT))
            cover_count++; else fail_count++ ;

The cover_count and fail_count statements are part f the action block.
assert property(property_spec) action_block
assume property(property_spec) action_block
cover property(property_spec) statement_or_null
cover sequence([clocking_event]
[disable iff (expression_or_dist)]
sequence_expr ) statement_or_null

Ben SystemVerilog.us