In reply to SriGanesh D:
From my SVA book:
220.127.116.11 restrict statement Rule:  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,:
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.
For training, consulting, services: contact http://cvcblr.com/home
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
1) SVA Package: Dynamic and range delays and repeats https://rb.gy/a89jlh
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
- SVA Alternative for Complex Assertions
- SVA in a UVM Class-based Environment
- Understanding the SVA Engine,