Assume and Restrict in SVA

SystemVerilog
, , ,
1

Hello all,
I would like to know the difference between “assume” and “restrict” property in SVA. In LRM, it is mentioned that “restrict property statement is not verified in simulation and has no action block”.

If restrict property is not verified in simulation, then how exactly it should be used in the simulation.
2

In reply to SriGanesh D:

From my SVA book:
4.5.1.3 restrict statement  Rule: [1] In formal verification, for the tool to converge on a proof of a property or to initialize the design to a specific state, it is often necessary to constrain the state space. For this purpose, the assertion statement restrict property is introduced. It has the same semantics as assume property, however, in contrast to that statement, the restrict property statement is not verified in simulation and has no action block. The difference between the restrict statement and the assume statement is that the restrict is used to limit scenarios to converge on a proof, whereas the assume defines legal input states.
For example, suppose that a cache controller performs behavior A when there is a cache hit (e.g., fetch data from the cache), or performs behavior B when there is a cache miss (e.g., invalidate cache entry, fetch data from main memory through an interface, store data into the cache, supply the needed value). To simplify the problem for the formal verification tool, one could constrain or “restrict” the problem to one of the two cache modes. Thus, the following can be written in one set of scenarios:

 
restrict property (@(posedge clk) cache_hit == 1’b0);  // cache miss scenario  
// Another formal verification session could use this restriction:     
restrict property (@(posedge clk) cache_hit == 1’b1);  // cache hit scenario

Another example of a restrict statement is the reset signal that can be classified as “one-shot” (i.e., one-time) that has a specific behavior during initialization. In this case, one needs to restrict the signal reset_n to low for 1 to 100 cycles, and then to high forever. Thus,:

 initial 
 ap_reset_then_hi : restrict property ( @ (posedge clk)    
      !reset_n[*1:100] ##1 reset_n |=>  always (reset_n));

This is a good use of the restrict because it is never illegal for reset_n to go active, but it is a common scenario to limit possible scenarios. In formal tools, you can typically re-qualify each assertion as assume, assert, or cover because the role of some assertion in a whole system may actually be different depending on what “part” of the system you are currently examining with formal. However, there is no need for the same re-qualification for the restrict statements - they mean one and only one thing, and the restrict should not be used as an assert or assume statement…

**Guideline:**Use assume to define legal input states that prevent false failures. Use restrict in formal verification when you are just trying to reduce the state space by limiting a test to one of several legal scenarios.

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:
3

In reply to ben@SystemVerilog.us:

Hello Ben
Thanks for your response. I have one more clarification in this, Assume and restrict are used only in formal verification, not in functional verification.?

4

In reply to SriGanesh D:

In reply to ben@SystemVerilog.us: Assume and restrict are used only in formal verification, not in functional verification.?

restrict is only used in formal verification.
assume is used in 1) definition of requirements, verification through simulation, and in formal verification. For example, if I know that the application for the design is only used in MASTERmode, and modes are input pins, I can write:


let MASTER=2'b00;
ap_mode: assume property(@ (posedge clk) mode==MASTER );

A chip designer runs into many situations where certain conditions are not yet well defined and assumptions have to be made. Thus, one can document those assumptions and go over them during reviews to refine them. The point, there is a lot of value in specifying assumptions.

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 - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: