Transcript Danger #1: Constraints

FEV’s Greatest Bloopers:
False Positives in Formal
Equivalence
Erik Seligman
CS 510, Lecture 7, January 2009
(Adapted from Seligman/Kim paper in
DVCon 2007)
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Agenda
 Introduction: FEV and False
Positives
 Danger #1: Constraints
 Danger #2: Libraries
 Danger #3: Unreachables
 Danger #4: Black Boxes
 Danger #5: RTL Language Usage
 Danger #6: Obscure Tool Behaviors
 Advice and Conclusions
What is a False Positive?
 False Positive: FEV incorrectly labels designs
equivalent
• Very costly
– FEV typically gates next design phase
– Wrong FEV answer at tapeout  silicon respin
 Not just theoretical– seen in Intel processors & ASICs
 Not discussing FEV tool bugs
• Many dangers for misuse when tool is OK
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Constraints in FEV
 Constraints: Reduce set of possible values
–Turn off scan
–Known conditions on inputs
–Eliminate unused state encodings
 Numerous types can be defined
–Explicit: “add pin constraint 0…”
–RTL: $constraint(foo | !bar | baz);
– Conformal: add ‘-define CONSTRAINT’ to read
design command to enable
–Within one-many mapping: “a -> b c d”
– Or combo of mapping + ‘add pin eq’ in Conformal
Example Where Constraint
Needed
Block 1
Block 2
A
B
C
INVERSE (A,B) needed to prove C==0 in Block 2
Bad Constraints  False
Positive

Conflicting pair of constraints
• INVERSE(a,b)
• Mapping: “a b -> c”
 Why is this a problem?
Bad Constraints  False
Positive

Conflicting pair of constraints
• INVERSE(a,b)
• Mapping: “a b -> c”  EQUAL(a,b)
 Result: no valid input space, so module passed
• Vacuous pass: all inputs illegal
• INVERSE(a,b) && EQUAL(a,b) ???
• Dead silicon in processor A0 stepping!
 New tool feature would catch contradiction
• But what if first constraint was !(A & B) ?
Recommendation #1
Review & Formally Verify Your
Constraints
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Library Cells and FEV
 Libraries of common cells used in designs
• AND, OR, Flip-Flops, etc.
• Often developed by remote team
 Library collateral supplied for FEV
• Logic representations trusted for higher-level FEV
– Analyze at transistor level every run? Too hard.
• Library team FEVs logic vs. actual circuits
• May come with assumptions on inputs
– Must prove for library to be valid
Example Of Library
Assumption
~b
b
~a
a
out
Need OR
here?
 Shorting together two wires– contention?
 Cell is legal IF we guarantee INVERSE (a,b)
• Save some transistors, power, area
Unproven Assumptions 
False Positive
 Processor FEV flow has ‘schematic assumption’ step
• Required to prove assumptions on library cell inputs
• Separate step from equivalence verification
– Actually an FPV run embedded in the FEV flow, since proving an
assertion rather than proving equivalence
 Design engineer didn’t understand requirement
• Formal Property Verification (FPV) optional in other areas
• Schematic Assumption step not run for one block
Another false positive & broken A0 processor silicon!
Recommendation #2
Make Sure Library Requirements are
Verified and Understood
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Unreachable Points in FEV

Unreachable: flop/latch that cannot affect output
 can be logically ignored
• Must be ignored, if not in both models
 Common causes
• Synthesis optimizations
• Tied off no-longer-relevant logic
 But be careful about backend logic
• Some flows (scan, bonus cells) connect later
• So ‘unreachables’ may be important!
Reachable and
Unreachable Flops
in1
A
misc logic
A: Reachable
in1
B
B: Unreachable
(logic tieoff)
C
C: Unreachable
(bonus flop)
misc logic
out1
Unreachables in Conformal
 Default: reported, not mapped/compared
 Be careful: two stages for elimination
• Some unreachables eliminated on load
• Some eliminated & reported during mapping
 My preference: do a best-effort mapping
• Compare any that were mapped
• Review unmapped ones & signoff
 Conformal commands
• read design … -keep_unreach
• set mapping method … –unreach
Lost Unreachables 
False Positive
 Bonus logic placed in ASIC design
 RTL-netlist FEV, backend net-net passed
• Bonus cells lost somewhere
• Intermediate FEV owners did not notice
 Problem aggravated by tool feature
• Two places for unreachables: loading,
mapping
• “Simple” bonus cells removed during loading
 Missing cells discovered at late inspection
Recommendation #3
Monitor Unreachable Points
Carefully
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Black Boxes in FEV
 Some logic usually must be
excluded
• IP received as-is from remote teams
• Pure analog blocks
 FEV tools allow black boxing
• Logic to boundaries of black box is verified
• But be careful!
–Audit to ensure everything is verified
somewhere
“Analog” Black Box? 
False Positive
FEV-able
Glue Logic
True Analog
Logic
Black Boxed Module
Recommendation #4
•Be Very Careful About Black Boxing
Logic
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Odd Corners of Verilog
 What does this mean if WIDTH=2?
wire foo = {a, {(2-WIDTH){1’b0}}, b};
• Why is this confusing?
Odd Corners of Verilog
 What does this mean if WIDTH=2?
wire foo = {a, {(2-WIDTH){1’b0}}, b};
• Why is this confusing?
 Does it mean
• {a,b}
• {a,0,b}
• {}
Odd Corners of Verilog
 What does this mean if WIDTH=2?
wire foo = {a, {(2-WIDTH){1’b0}}, b};
• Why is this confusing?
 Does it mean
• {a,b}
• {a,0,b}
• {}
 Verilog standard was ambiguous, tools
disagree!
• This particular issue fixed in SystemVerilog: {a,b}
Language Ambiguity 
False Positive
 Originally synthesized with vendor tool
• FEV tool from same vendor said design fine
• Both tools had same interpretation
 FEV tool from other vendor revealed diff
• Embedded in huge logic cone, hard debug
• Pressure to waive based on vendor FEV
 Finally root-caused with vendor AEs
• Designer intent disagreed with synthesis!
Preventing Language Issues
 RTL Coding standards
 Enforce thru linting tools
• Examples: Synopsys LEDA, Atrenta
Spyglass
 Correct linting would flag ambiguous RTL
 + Avoid Synthesis & FEV from same
vendor
• Increases chance of catching these cases
• Vendors try to push integration though!
Recommendation #5
Make sure RTL is high-quality & fully
linted
Recommendation #6
Ensure Synthesis-FEV
Independence
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Multi-Driven Nets
 Many ways to get driven in Verilog
• assign statements
• Input port to module
• Connect to output of submodule
 What if a net has multiple drivers?
• Combine with some logic function
(AND,OR)?
• Report error?
Surprising Default
 Multi-driven nets treated as Wired AND
•  result is AND of all drivers
• Copied from common synthesis default
 But is this always the intent?
• Maybe it’s an error
• Maybe user expected an OR
• Maybe input accidentaly defined as output
– This really happened in a design near tapeout
– Incorrect logic treated as AND, only caught
luckily thru late inspection!
Multiple Drivers in Conformal
 set wire resolution [AND|OR|WIRE]
• AND, OR = use logical function
• WIRE = create special node (‘E’) and report
– E points become standalone key points
– Usually any occurrence is an error!
• Default is AND
 My recommendation: set to WIRE
• Unless actively intending multi-drives
Recommendation #7
Understand your FEV tool, including
obscure options.
Agenda








Introduction: FEV and False Positives
Danger #1: Constraints
Danger #2: Libraries
Danger #3: Unreachables
Danger #4: Black Boxes
Danger #5: RTL Language Usage
Danger #6: Obscure Tool Behaviors
Advice and Conclusions
Recommendations
1.
2.
3.
4.
5.
6.
7.
8.
Review and formally verify constraints.
Make sure libraries are verified & understood.
Monitor unreachable points carefully.
Be very careful about black boxing logic.
Make sure RTL is high-quality & fully linted.
Understand your FEV tool, including obscure options.
Ensure Synthesis-FEV independence.
Sanity-check FEV with at least some GLS (gate-level
simulation) runs.
• See paper for details
Conclusions
 FEV is a powerful tool, reliable if used correctly!
 But false positives are a real danger
• Issues seen in many projects at Intel
• Very costly, sometimes requiring new stepping
 Useful to recognize common causes
• Misuse of constraints
• Library misunderstandings
• Excluded unreachable points
• Incorrect Blackboxing
 Understand your tools, library, and design!
References / Further Reading
 http://www.aracnet.com/~eseligma/docs/
dvcon_2007.pdf