In reply to ben@SystemVerilog.us:
Also, consider the restrict.
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