Transcript presentation

February 22-25, 2010
Designers Work Less with Quality Formal
Equivalence Checking
by
Orly Cohen, Moran Gordon, Michael Lifshits,
Alexander Nadel, and Vadim Ryvchin
Intel
Agenda
• Formal Equivalence Checking (FEC) in Parts Using AssumeGuarantee
• FEC Flow Description and the Importance of Assumptions
• Minimizing Assumptions
– Naive Approaches
– FEC as SAT Problem
– Minimizing Assumptions Using SAT
• Comparison of SAT-Based and Naive Minimization Approaches
• Impact of Assumption Minimization on the Manual Debug
Effort
• Conclusions and Recommendations
Michael Lifshits, Intel
2 of 14
Assume-Guarantee in Formal
Equivalence Checking (FEC)
• FEC proves the equivalence of 2 designs (e.g. schematics vs. RTL)
• FEC is done on small sub-blocks (slices) suitable for formal tools’
capacity
• Slices’ inputs are restricted with assumptions, e.g. in SVA
Assertion
Inputs
Outputs
Assumption
DUT with Properties
Michael Lifshits, Intel
3 of 14
Origins of Assumptions
• Manually added assumptions
• Design intent properties
– ABV methodology
• Schematic Assumptions
– appear in the standard cells library
– save transistors, area, power
Michael Lifshits, Intel
INVERSE(a,b)
4 of 14
FEC Stages – the Importance of
Assumptions
Assumptions must be
proved relative to the
driving logic
smaller set of
assumptions is better!
Assumptions must
be proved relative
to the driving logic
“Intel CPU project arrived with a dead A0 silicon due to a missed assumption
verification step”
Michael Lifshits, Intel
5 of 14
Minimizing the Assumptions Set
Naive approaches:
• Static Structural Analysis
• Iterative Trial and Error alg.
MinAssump := ∅
// start without assumptions
while verification fails and MinAssump  All_Assump do
Try proving with assumptions in MinAssump
if pass  Done
Use the counterexample (CEX) and find A ∈ All_Assump : A ∈ MinAssump
and A contradicts with CEX
Add (at most K) such assumptions to MinAssump // K=20
return MinAssump
Michael Lifshits, Intel
6 of 14
Formal as SAT Problem
• Most FEC tools are implemented with SAT-based FV engines
• FEC is reduced to a propositional formula: F=a AND b OR c…
• SAT solver proofs the lack of counterexamples for F;
– CEX is an assignment for {a,b,c..} | F==TRUE
ENB
S1
O1=NOTS1
O2’=(S1ANDS2 ANDENB) OR (O2AND^ENB)
S2
• same(O1,O2)(t), F=XOR(O1, O2’)(t), fails when F=TRUE
NOTS1(t)AND(S1(t)…
checked for t=1,2.. fails when S1=T, S2=T, ENB=T
• Unsatisfiable core – sub-formulas required for the proof
Michael Lifshits, Intel
7 of 14
Minimizing Assumptions Using SAT
• The projection of UNSAT CORE onto the assumptions is the subset of
assumptions required for the proof
• Minimization at the SAT level  minimal number of assumptions
• Simple approach:
assumptions
SAT Formula
UNSAT CORE
• Our approach:
Michael Lifshits, Intel
8 of 14
Iterative SAT Algorithm to
Minimize Assumptions
Solve formula F: SAT(F) with All_Assump
Extract UNSAT CORE: UC
MinAssump := A ∈ Assump: A ∩ Proj(UC) ≠∅ // start with all used
for all A ∈ MinAssump do
// try removing 1 assumption, reuse learning in SAT
SAT(F) with MinAssump / {A} // solve F without A
If pass  MinAssump := MinAssump /{A} , update UC
return MinAssump
SAT-Based Minimization vs. Naive Trial and Error
50% assumptions in most cases, and dramatically fewer in some
Michael Lifshits, Intel
9 of 14
SAT-Based Minimization
Algorithms Comparison
35%
45.00
30%
40.00
35.00
25%
30.00
20%
25.00
15%
20.00
15.00
10%
10.00
5%
5.00
0%
0.00
DUT1
DUT2
DUT3
Run time (hours)
Remaining properties
• UNSAT CORE Projection vs. Iterative Minimization (ours)
Projection
Iterative
Minimization
Projection TIME
Iterative
Minimization TIME
DUT4
• It is justified mainly when minimizing the core is more important than
reducing the run-time
Michael Lifshits, Intel
10 of 14
Impact of Assumption Reduction
on the Manual Debug Effort
• All properties (including assumptions) are formally verified
• SQL database used to store the verification results
• Combined verification status – status of the recursive set of used
assumptions:
For each used-by-FEC (UBF) property P
Get the set of assumptions (Assump) used to verify a property P
For each Ai ∈ Assump Assumpi := set of assumptions used to verify Ai
Assumpall = Assump ∪ Assumpi …∪ Assumpn // a recursive set
if all Ai ∈ Assumpall pass
status(P) = pass
else
status(P) = conditional
Michael Lifshits, Intel
11 of 14
% of all properties
Impact of Assumption Reduction
on the Manual Debug Effort
60%
50%
40%
30%
original
20%
assump_min
10%
0%
Conditional
Failed
Not Run
Passed
Problematic
• 36% more properties passed
• Number of properties in FEC is large – a large amount of
manual effort is saved to the design team
Michael Lifshits, Intel
12 of 14
Conclusion and Recommendations
Reducing the number of used assumptions decreases manual debug time and
computational effort
UNSAT core-based techniques are much more effective than naive techniques
Tradeoff between the reduction effectiveness and the run-time
Different SAT-based assumption minimization techniques fit various FEC stages
• Assumptions minimization is more important for RTL and SCH equivalence
verification than for the RTL assumption verification
• RTL assumptions verification complexity is greater than RTL and SCH
equivalence
Iterative SAT-based assumption minimization for RTL and SCH
equivalence
Assumption reduction (UNSAT core projection) for RTL assumption
verification
Michael Lifshits, Intel
13 of 14
Backup
Michael Lifshits, Intel
14 of 14
SAT-Based Minimization vs. Naive
Trial and Error
Time (logarithmic scale)
“naive” trial and error
SAT-based
•
•
22 random microprocessor design blocks
% indicate the improvement compared to the iterative
50% == ½ assumptions
Half as many assumptions in most cases, and
dramatically fewer in some
Michael Lifshits, Intel
15 of 14