Paper and Tutorial Presentation Template and Information

Tom Fitzpatrick

Informations

• Publié par: Shuel
• Nombre de lectures: 18
• Langue: English

Extrait

February 22-24, 2006
Guidelines for creating a formal verification testplan
There is no substitute for thinking!
Harry Foster - Mentor Graphics Corp
Lawrence Loh - Jasper Design Automation
Bahman Rabii - Google
Vigyan Singhal - Oski Technology
1Agenda
• Observation
• Verification Testplanning Process
• Seven Steps of Formal Testplanning
• AHB-I2C Example
Harry Foster, 2006 2Observation
• Successful verification is not ad hoc in nature
– Success depends on methodical verification planning combined with
systematic verification processes.
• The key to success is the verification testplan.
Harry Foster, 2006 3Verification Testplan
• A project’s functional verification testplan is the specification for the
verification process.
– Developing this testplan usually involves the entire engineering team
• architects, designers, and verification engineers
• In general, the verification testplan defines exactly
– what functionality will be verified,
– how it will be verified
• the verification strategy and resource allocation
– when the verification process is complete
• metrics for measuring progress or completion criteria
Harry Foster, 2006 4FV for bug hunting or assurance?
Bug hunting Assurance
Many RTL assertions One comprehensive spec
Pushbutton tools Semi-automated tools
Success: # bugs found Success: ckt meets spec
Testplan critical!
Bugs Rate
Assurance
Bug hunting
Time
Rev 0 RTL Tapeout
Harry Foster, 2006 5Agenda
• Observation
• Verification Testplanning Process
• Seven Steps of Formal Testplanning
• AHB-I2C Example
Harry Foster, 2006 6Where to apply formal?
• Formal verification of properties on RTL designs is a known hard problem
– Formal verification algorithm complexity
• Exponential in the size of the designs
– Naïve application of formal verification
• State-space explosion
• Impractical computer run- times
• Our first step is to identify appropriate blocks for formal
– Prior to creating a formal testplan
Harry Foster, 2006 7Where to apply formal
• One coarse measure of prediction of the tractability
– number of state-holding elements in the cone of influence of the property
Design
Block
Property
Cone of
Influence
Irrelevant
Logic
Harry Foster, 2006 8Where to apply formal
• Real examples include:
- Arbiters of many different kinds
- Interrupt controller
- On-chip bus bridge - Memory controller
- Token generator
- Power management unit
- Credit manager block
- DMA controller
- Standard interface (AMBA, PCI Express, …)
- Host bus interface unit
- Proprietary interfaces
- Scheduler, implementing multiple
- Clock disable unit
virtual channels for QoS
• Common characteristic: concurrency, multiple data streams
Multiple, concurrent streams
Hard to completely verify using simulation
“10 bugs per 1000 gates”
-Ted Scardamalia, IBM
Harry Foster, 2006 9Where not to apply formal
• Examples of designs not appropriate for formal include:
(I’m not talking about theorem proving!)
• Floating point unit
• Graphics shading unit
• Convolution unit in a DSP chip
• MPEG decoder
• Common characteristic:
often sequential in nature, potentially involves some type of data transformation (math)
Single, sequential/functional streams
“2 bugs per 1000 gates”
-Ted Scardamalia, IBM
Harry Foster, 2006 10