Introduction to Assertion-Based Formal Verification - SVA: The Power of Assertions in SystemVerilog - page 444

RTL with
embedded
assertions

Check
specification in
simulation

Fix RTL

no

OK

yes

real CEX

Run
FV

failed

Check
CEX

Check
results

passed or unknown

spurious CEX

Done

Add missing
assumptions

Fig. 20.4 Lightweight formal verification flow

o1

Block1 i1 Block2

a1:
assert final (o1!=o2);

m1:
assume final

o2 i2

(i1 != i2);

Fig. 20.5 Assume-guarantee paradigm

20.5 Assume-Guarantee Paradigm

As we have seen, the correctness and completeness of FV of a design block depends
very much on the specification of assumptions. To check assumptions for the block,
it is necessary to prove them as assertions on the parts of the design that drive the
block, as shown in Fig. 20.5 .
In this example, we verify Block2 using assumption m1 stating that the two inputs
i1 and i2 are complements of each other. This assumption should be proven as an
assertion a1 on the outputs o1 and o2 when verifying Block1 .