Formal Verification
A mathematical approach to prove or disprove the correctness of a system with respect to a specification.
Tools
Verilog Statements
assume
- constraint that the system relies on to be true for correct operation
- skip states that violate assumptions (generally input or environmental)
cover
- constraint that must be demonstrably reachable in the system
- break (pass) on desired state, skip others
assert
- constraint that must always hold during system execution
- skip desired state, break (fail) on others
past
- value of signal in on previous clock
always @(posedge clk) begin
f_past_valid <= 1;
if(f_past_valid)
assert($past(y) == y);
end