Hardware Reference
In-Depth Information
We are not going to further elaborate the distribution usage in assumptions as it
falls beyond the scope of this topic.
In formal verification dist acts as inside operator, and the weight specifications
are ignored. It is also legal, though meaningless, to use distributions in assert and
cover statements, and they are also treated as inside operators there. 9
4.6
Restrictions
Sometimes it is difficult to formally verify a block. It becomes necessary to verify
special cases separately and then combine them together. We can take an Arithmetic
Logic Unit (ALU) as an example. ALU can perform several commands, such as
addition, subtraction, arithmetic shift, etc. It thus makes sense to split the verification
process into several cases corresponding to the commands, i.e., we separately verify
addition, subtraction, etc.
To specify the case of addition it is natural to use an assumption, such as
m1: assume property (@clk opcode == OP_ADD);
where opcode is an operation code control variable in ALU, and OP_ADD means
addition.
This will do the job in FV, but in simulation this assumption is likely to fail
because the simulation test cases are not guaranteed to limit the ALU commands
to addition only. The workaround is to wrap such assumptions in 'ifdef , which
makes the code less readable and dependent on the custom setup.
In SystemVerilog, there is a cleaner solution, called restriction . Other than the
keyword restrict , the restriction syntax is the same as the syntax of assertions and
assumption. Unlike assertions and assumptions, restrictions have only concurrent
form, and they cannot have action blocks:
restriction ::= name : restrict property ( property );
Restrictions are treated as assumptions in FV, but they are completely ignored
in simulation. They are meant for limiting formal proofs to particular cases.
Consequently, the above example should be rewritten as:
r1: restrict property (@clk opcode == OP_ADD);
Since restrictions are ignored in simulation, using actions with them is meaning-
less, this is why the restriction syntax does not allow actions.
9 It is conceivable that simulators could also check that the values of the expression in the dist
operator used in an assertion or cover satisfy the specified distributions at the end of simulation.
Search WWH ::




Custom Search