Paper and Tutorial Presentation Template and Information

Paper and Tutorial Presentation Template and Information

-

English
28 Pages
Read
Download
Downloading requires you to have access to the YouScribe library
Learn all about the services we offer

Description

February 22-24, 2006Guidelines for creating a formal verification testplanThere is no substitute for thinking!Harry Foster - Mentor Graphics CorpLawrence Loh - Jasper Design AutomationBahman Rabii - GoogleVigyan Singhal - Oski Technology1Agenda• Observation• Verification Testplanning Process• Seven Steps of Formal Testplanning• AHB-I2C ExampleHarry 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 criteriaHarry Foster, 2006 4FV for bug hunting or assurance?Bug hunting AssuranceMany RTL assertions One comprehensive specPushbutton tools Semi-automated toolsSuccess: # bugs found Success: ckt meets specTestplan critical!Bugs RateAssuranceBug huntingTimeRev 0 RTL TapeoutHarry Foster, 2006 5Agenda• Observation• Verification Testplanning ...

Subjects

Informations

Published by
Reads 18
Language English
Report a problem

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