ASPDAC/VLSI 2002 Tutorial
Functional Verification of System on Chip - Practices,
Issues and Challenges
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
1
Presenters: Subir K. Roy (Co-ordinator),
Synplicity Inc.,
935 Stewart Drive,
Sunnyvale CA 94085,
USA
Tel. : 408-215-6049
Fax. : 408-990-0296
Email: [email protected]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
2
Presenters: S.Ramesh
Dept. of Computer Sc. & Engg.,
IIT-Bombay, Powai,
Mumbai 400 076
Tel. : +91-22-576-7722
Fax. : +91-22-572-0290
Email: [email protected]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
3
Presenters: Supratik Chakraborty,
Dept. of Computer Sc. & Engg.,
IIT-Bombay, Powai,
Mumbai 400 076
Tel. : +91-22-576-7721
Fax. : +91-22-572-0290
Email: [email protected]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
4
Presenters: Tsuneo Nakata,
Fujitsu Laboratories Limited,
1-1, Kamikodanaka, 4-Chome,
Nakahara-ku, Kawasaki,
211-8588, Japan
Tel. : +81-44-754-2663
Fax. :+81-44-754-2664
Email: [email protected]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
5
Presenters: Sreeranga P. Rajan,
Fujitsu Labs. Of America,
595 Lawrence Expressway,
Sunnyvale CA 94086-3922,
USA
Tel. : 408-530-4519
Fax. : 408-530-4515
Email: [email protected]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
6
Tutorial Outline
• Motivation & Introduction to SoC Design & Re-use.
• System Verification
• Techniques for Module Verification : Formal, SemiFormal
• Techniques for System Verification : Simulation,
Hybrid, Emulation
• Quality of Functional Verification : Coverage Issues
• Academic & Research Lab Verification Tools
• Case Studies
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
7
Tutorial Outline (contd.)
• Commercial Tools
• Issues and Challenges / Future Research Topics
• Summary & Conclusions
• Bibliography
• Appendix
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
8
Tutorial Outline (Contd.)
• Motivation & Introduction to SoC Design & Re-use
(Subir K. Roy)
• Motivation, Verification Heirarchy, System Level
Design Flow, SoC Design, SoC Core Types, SoC
Design Flow, Implications on Verification.
• System Verification (S. P. Rajan)
• Current Design Cycle, Design Cycle with System
Verification.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
9
Tutorial Outline (Contd.)
• Techniques for Module Verification
• Formal Approaches (S. Ramesh)
• Introduction to Formal Verification
• Formal Models, Modeling Languages, Formal
Methods, Formal Specification, Temporal
Logics, CTL, Automatic Verification, Theorem
Proving.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
10
Tutorial Outline (Contd.)
• Implementation of Formal Approaches
(S. Chakraborty)
• Binary Decision Diagrams, Combinational
Equivalence Checking, Sequential
Equivalence Checking, Commercial
Equivalence Checkers, Symbolic CTL Model
Checking of Sequential Circuits, Forward &
Backward Reachability, State of the Art,
Related Techniques.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
11
Tutorial Outline (Contd.)
• Techniques for Module Verification(contd.)
• Semi-Formal Approaches
• Semi-Formal Verification (S. Chakraborty)
• Interface Specification for Divide & Conquer
Verification (T. Nakata)
• Techniques for System Verification
• Symbolic Simulation & Symbolic Trajectory
Evaluation (S. Chakraborty)
• Hybrid Verification (S. P. Rajan)
• Emulation (Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
12
Tutorial Outline (Contd.)
• Quality of Functional Verification (Subir K. Roy)
• Coverage Metrics – Informal, Semi-Formal,
Formal.
• Academic & Research Lab Verification Tools
• Verification Tools – 1 (S. Ramesh)
• VIS, SMC, FC2toolset, STeP
• Verification Tools – 2 (S. P. Rajan)
• Fujitsu High Level Model Checking Tool,
VeriSoft.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
13
Tutorial Outline (Contd.)
• Case Studies
• Case Study – 1 (S. P. Rajan)
• ATM Switch Verification
• Case Study – 2 (T. Nakata)
• Semi-Formal Verification of Media Instruction
Unit
• Commercial Tools (Subir K. Roy)
• FormalCheck, Specman Elite, ZeroIn-Search,
BlackTie
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
14
Tutorial Outline (contd.)
• Issues and Challenges / Future Research Topics
• High Level Specification & Modeling using UML
(T. Nakata)
• Research Issues ( S. Chakraborty)
• Future Research Directions (S. P. Rajan)
• Summary & Conclusions
• Summary ( S. Chakraborty)
• Conclusions (Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
15
Tutorial Outline (contd.)
• Bibliography
• Papers, Books, Important Web Sites,
Conferences, Journals/Magazines.
• Appendix
• Linear Temporal Logic, w-Automata based
Formal Verification (S. Ramesh)
• Neat Tricks in BDD Packages (S. Chakraborty)
• More Research Tools – SPIN, FormalCheck
(S. Ramesh)
• More on UML (T. Nakata)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
16
SoC Design & Re-use
(Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
17
Motivation
• Pentium SRT Division Bug : $0.5 billion loss to Intel
• Mercury Space Probe : Veered off course due to a
failure to implement distance measurement in
correct units.
• Ariane-5 Flight 501 failure : Internal sw exception
during data conversion from 64 bit floating point to
16 bit signed integer value led to mission failure.
• The corresponding exception handling
mechanism contributed to the processor being
shutdown (This was part of the system
specification).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
18
Verification Hierarchy
Higher-Order Theorem Proving
Coverage/
Expressive
Power
First-Order Theorem Proving
Temporal Logic Based
Model Checking
Assume-Guarantee based
symbolic simulation/Model Checking
Equivalence Checking
Equivalence Checking of
structurally similar circuits
Simulation
Degree of Automation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
19
System Level Design Flow
• Interface Definition
• Component Selection
• ASIC & Software Implementation
• Glue Logic Implementation
• PCB Layout Implementation
• Integration & Validation of Software into System
• Debugging
• Board - Manufacturing & Test
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
20
SoC Design
• Core based design approach
• Design Complexity
• Time To Market
Core : A pre-designed, pre-verified Silicon circuit
block. Eg. Microprocessor, VPU, Bus Interface,
BIST Logic, SRAM, Memory.
• Core Integration
• Re-usable cores : different types, different
vendors
• User defined logic
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
21
SoC Design
• Designing Cores for integration
• Parameterization
• Customizable soft cores. Core provider supplies essential set of pre-verified parameters.
• Functionality
• Single core - preferable
• Multiple core - Needs good partitioning
• Interface
• Support std. buses to ease integration.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
22
SoC Core Types
[Anderson, 2001]
• Cell/Macro Library elements
• DSPs, Microcontrollers
• Implementation of Standards
• Function (MPEG, JPEG, CRC, PicoJava,…)
• Interconnects (PCI, SCSI, USB, 1394, IrDA,
Bus Bridges)
• Networking (10/100 ethernet, ATM etc.)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
23
SoC Core Types
• Soft Cores : Technology Independent Synthesizable
Description. White Box Implementation - Visible &
Modifiable. Core can be extended functionally.
• Firm Cores : Technology Dependent Gate Level
Netlist. Internal implementation of core cannot be
modified. User can parameterize I/O to remove
unwanted functionality.
• Hard Cores : Layout & Timing Information provided.
Cannot be re-synthesized. Integration is simple &
can result in highly predictable performance.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
24
SoC Design Flow
• Co-design approach : Software + Hardware
• Design exploration at behavioral level (C, C++,
etc.) by system architects
• Creation of Architecture Specification
• RTL Implementation (Verilog/VHDL) by hardware
designers
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
25
SoC Design Flow
• Drawbacks
• Specification Errors - susceptible to late
detection
• Correlating validations at Behavioral & RTL level
difficult
• Common interface between system & hw
designers based on natural language
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
26
SoC Implementation Approaches
• Vendor Based Approach : ASIC Vendor/Design
service group carries out implementation
• Partial Integration : System Designer implements
proprietary & application specific logic. ASIC
Vendor integrates above with their cores
• In house : ASIC Vendor designs specialized cores.
System Designer implements proprietary & application specific logic, integrates cores & verifies
integrated design
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
27
Multiple Sources for IP Reuse
• Semiconductor houses
• I/O Pad, Processor Core, Custom Logic, Memory,
Peripheral Interface
• IP/Core Suppliers
• Processor Core, Peripheral Interface, Analog
/Mixed Signal blocks (DAC, ADC, PLL)
• System Designer
• Controller, Custom Logic, AMS blocks
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
28
Advantages of Core/IP based approach
• Short Time To Market (pre-designed)
• Less Expensive (reuse)
• Faster Performance (optimized algorithms and
implementation)
• Lesser Area (optimized algorithms and
implementation)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
29
Implications on Verification
• [Mosensoson, DesignCon 2000]
• Verification Focus
• Integration Verification & Complexity.
• Bug Classes
• Interactions between IP/Core/VC blocks
• Conflicts in accessing shared resources
• Deadlocks & Arbitration
• Priority conflicts in exception handling
• Unexpected HW/SW sequencing
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
30
Implications on Verification
• Need to capture complexity of an SoC into an
executable verification environment
• Automation of all verification activities
• Reusability of verification components of unit
Cores/IPs/VCs
• Abstraction of verification goals (Eg., Signals to
Transcations, End to End Transactions)
• Checkers for internal properties
• Interface Monitors (BFM, Integration Monitors)
• Coverage monitors
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
31
Implications on Verification
• Implication
• Rigorous verification of each individual SoC
component seperately
• Extensive verification of full system
• Requirements
• Efficient Verification Methodologies
• Efficient Tools
• High Level of Automation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
32
System Verification
(S. P. Rajan)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
33
Current Design Cycle
RTL Description
(from Spec/Doc)
Simulation +
Formal Verification
Modify RTL Source
RTL/logic Synthesis
Modify Script
Timing Analysis
NOT OK
OK
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
34
Current Design Cycle
• Methodology
• fixed parameter modeling
• large-scale simulation (expensive)
• synthesis
• large-scale validation (expensive)
• Design cycle iteration expensive for changes in
design parameters
• Does RTL Description satisfy Specification?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
35
Design Cycle with System Verification
Cycle Accurate Behavior
Validate
Generic Parameters
Instantiation
Cycle Accurate Behavior
Fixed Parameters
Cycle Accurate Behavior
Fixed Parameters
High/RT-Level Synthesis
Gate-Level
Gate-Level
(Small)
(Large Design)
Validate
Logic Synthesis
Chip
Chip
Validate = Formally Verify + Simulate
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
36
Design Cycle with System Verification
• Parametric Design Methodology:
-- Higher abstraction level
-- Reusable generic parametric model
-- small-scale simulation (low cost)
-- formal verification viable
-- Automatic high-level synthesis
-- validation on a small scale (low cost)
• Formal verification early in design cycle
• Drastic reduction in design cost, time-to-market
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
37
Techniques for
Module Verification
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
38
Formal Verification
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
39
Formal Methods
• Functional verification
• SOC context: block level verification, IP Blocks
and bus protocols
• Formally check a formal model of a block against
its formal specification
• Formal - Mathematical, precise, unambiguous,
rigorous
• Static analysis
• No test vectors
• Exhaustive verification
• Prove absence of bugs rather than their presence
• Subtle bugs lying deep inside caught
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
40
Three-step process
• Formal specification
• Precise statement of properties
• System requirements and environmental
constraints
• Logic - PL, FOL, temporal logic
• Automata, labeled transition systems
• Models
• Flexible to model general to specific designs
• Non-determinism, concurrency, fairness,
• Transition systems, automata
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
41
Three-step process (contd.)
• Verification
• Checking that model satisfies specification
• Static and exhaustive checking
• Automatic or semi-automatic
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
42
Formal verification
• Major techniques
• Equivalence checking
• Model checking
• Language containment
• Theorem proving
Model
Spec
Logic
Tr. Systems/
Automata
Model Checking
Automata/
Tr. Systems
Lang. Containment
Obs. Equivalence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Logic
Th. Proving
Eq. Checking
43
EQUIVALENCE CHECKING
•
•
•
•
•
•
•
•
Checking equivalence of two similar circuits
Comparison of two boolean expressions - BDDs
Highly automatic and efficient
Useful for validating optimizations, scan chain
insertions
Works well for combinational circuits
Limited extension to sequential circuits
Most widely used formal verification technique.
Many commercial tools:
• Design VERIFYer (Chrysalis), Formality
(Synopsis), FormalPro (Mentor Graphics),
Vformal(Compass), Conformal (Verplex), etc.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
44
Model checking/Language Containment
• Another promising automatic technique
• Checking design models against specifications
• Specifications are temporal properties and
environment constraints
• Design models are automata or HDL subsets
• Checking is automatic and bug traces
• Very effective for control-intensive designs
• Commercial and Academic tools: FormalCheck
(Cadence), BlackTie (Verplex), VIS (UCB),
SMV(CMU, Cadence), Spin (Bell labs.), etc.
• In-house tools: IBM (Rulebase), Intel, SUN, Fujitsu
(Bingo), etc.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
45
Theorem proving
•
•
•
•
•
•
•
Theoretically most powerful technique
Specification and design are logical formulae
Checking involves proving a theorem
Semi-automatic
High degree of human expertise required
Mainly confined to academics
Number of public domain tools
• ACL2 (Nqthm), PVS, STeP, HOL
• ACL2 used in proving correctness of
floating point algorithms
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
46
Formal verification (experiences)
• Very effective for small control-intensive
designs-blocks of hundreds of latches
• Many subtle bugs have been caught in designs
cleared by simulation
• Strong theoretical foundation
• High degree of confidence
• Hold a lot of promise
• Require a lot more effort and expertise
• Large designs need abstraction
• Many efforts are underway to improve
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
47
Systems verified
• Various microprocessors (instruction level
verification):
• DLX pipelined architectures, AAMP5 (avionics
applications), FM9001 (32 bit processor),
PowerPC
• Floating point units:
• SRT division (Pentium), recent Intel ex-fpu, ADK
IEEE multiplier, AMD division
• Multiprocessor coherence protocols
• SGI, sun S3.Mp architectures, Gigamax,
futurebus+
• Memory subsystems of PowerPC
• Fairisle ATM switch core
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
48
State of the art
•
•
•
•
FSM based methods : ~ 500 registers
STE: ~ 10 - 20k registers
Equivalence checking : ~ million gates designs
Simulation : million gates capacity
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
49
Challenges of formal verification
• Complexity of verification
• Automatic for finite state systems (HW,
protocols)
• Semi-automatic in the general case of infinite
state systems (software)
• State explosion problem
• Symbolic model checking
• Homomorphism reduction
• Compositional reasoning
• Partial-order reduction
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
50
Formal Modeling
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
51
Models
•
•
•
•
High level abstractions of real systems
Contain details of relevance
Full Systems detailed and complex
Physical components and external components
• e.g. buses, schedulers, OS/network support software
• Modeling
• Modeling is a (pre-) design activity
• Models relatively easier to build
• Higher level than behavioral models (C models)
• early detection of bugs,
• design space exploration and verification,
• prototypes and synthesis
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
52
Formal Models
• Mathematical description of models
• Precise and unambiguous
• Consistent and complete
Formal Verification
• Applies to mathematical models and not to real
objects (hence called Design Verification)
• Faithful models essential
• False negatives (Spurious Errors)
• False positives (Models pass but System fails)
• Simulation/Testing cannot be dispensed with!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
53
Formal Modeling Languages
•
•
•
•
Enable abstract and high level descriptions
Real languages often ambiguous
Variation in HDL semantics
Real languages require more details and effort
Features
Limited and High Level Data Types
• Nondeterminism (arising out of abstractions)
• Concurrency (to structure large systems)
• Communication (for internal and external interaction)
• Fairness (abstraction of real concurrency and
schedulers)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
54
Example Modeling Languages
• Finite State Machines
• CSP, CCS, SDL, Promela (for Asynchronous
Systems and Protocols)
• Esterel, CFSM (Embedded Controllers)
• Statecharts, UM L (System level models)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
55
Models of Hardware
• Hardware blocks are reactive systems:
• Reactive systems exhibit infinite behavior
• Termination is a bad behavior
• Timing/Causality information important
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
56
Finite State Machines
• Well-known model for describing control or
sequential circuits
• An example (3-bit counter)
• State labels describe bit status
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
57
Another Example
• A Traffic Light Controller
•
•
•
•
States HG - Highway green, FY – Farm road Yellow
C - Car in Farm road,
S,L - Short and long timer signal
TGR - reset timer, set highway green and farm road
red
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
58
States and Transitions
• States are abstract description of actual machine
states
• decided by the states of latches and registers
• Finite no. of States
• No final state - reactive systems not supposed to
terminate
• Edge labels - input/condition and output/action
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
59
States and Transitions
• Many Flavors of State Machines
• edge labeled - Mealy machines
• state labeled - Kripke structures
• state and edge labeled - Moore machines
• Labels
• Boolean combination of input signals and
outputs
• communication events (CSP, Promela)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
60
Semantics of Finite State Systems
• The above description is syntactic
• Semantics associates behaviors
• Branching Time semantics
• the tree of states obtained by unwinding
the state machine graph
• possible choices are explicitly
represented
• Linear Time Semantics
• the set of all possible `runs' in the
system
• the set of all infinite paths in the state
machine
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
61
Non-determinism
•
•
•
•
•
•
2-master arbiter,
reqi - request from Master i
This machine is nondeterministic
In Idle state when req1 and req2 arrive.
Non-determinism due to abstraction
More than one behaviour for a given input
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
62
Concurrency
• A concurrent (and hierarchical) description of
Counter
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
63
Concurrent Descriptions
•
•
•
•
•
•
Compact and easy to understand
Natural model for hardware and complex systems
Clear semantics required
Interleaved model and synchronous models
Appropriate communication primitives
Concurrent machines composed to a single
global machine
• Global machine captures all possible executions
• Exponential blow-up
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
64
Fairness Constraints
• In general, not every run in a state machine is a
valid behavior
• Arbiter example
• the run in which master 2 is never granted
the resource
• But all runs are included in transition systems
• Fairness constraints rule out certain runs
• Modeling abstraction of real-time or schedulers
Example
• Every request eventually considered
• The clock tick arrives infinitely often
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
65
Fairness Constraints
•
•
•
•
Not required with a more concrete description
But concrete description too complex to verify
A given property may not require concrete details
For verification, abstract designs are preferable.
• proof is simpler
• proof is robust under alternate implementations.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
66
Generating Formal Models
• Pre-design activity
• Automatic Translation from circuits/HDL designs
• States decided by the latches/registers in the ckt.
• Exponential blow-up in the size (State-explosion
problem)
• Usually abstractions required
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
67
Design errors
Deadlock
•
•
• Look at state (1,1)
Unspecified Receptions
• State (1,1)
• P1 can send message 2
• P2 cannot receive this
Non executable interaction - 'Dead code‘
• State 3 of P1 cannot be reached at all
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
68
Live lock/Divergence
• An example:
• Formal Verification generalizes early approaches
to detection of such errors!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
69
Formal Specification
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
70
Formal Specifications
• Verification involves checking that a design model
meets its specification.
• Specification states what the system is supposed to
do
• Design describes how this is done
Specification
• Describes unambiguously and precisely the
expected behavior of a design.
• In general, a list of properties.
• Includes environment constraints.
• Symbolic logic or automata formalisms
• Consistency and Completeness
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
71
Specification of Hardware blocks
• Properties and Constraints specify possible
states and transitions
• They state set of possible valid `runs'
• Valid runs are infinite sequences (or trees) of
states and transitions
• Formal specifications are finitistic and precise
descriptions
Classification of Properties:
Safety properties
• "undesirable states are never reached",
• "desirable things always happen".
• Progress or Liveness Properties
• "desirable state repeatedly reached"
• "desirable state eventually reached"
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
72
Examples
Safety Properties
• A bus arbiter never grants the requests to two
masters
• Message received is the message sent
• Elevator does not reach a floor unless it is requested
• At any time traffic is let either in the farm road or on
the highway
• every received message was sent
Liveness Properties
• car on the farm road is eventually allowed to pass
• Elevator attends to every request eventually
• every bus request is eventually granted
• every sent message was received
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
73
Specification Formalisms
• Properties and Constraints specify permissible
behaviours
• Behaviours are infinite runs (reactive systems)
• They are infinite objects, in general.
• We need finitistic representation of such infinite
objects for precision
• Two Major formalisms:
• Symbolic Logics: Linear and Branching
Temporal Logics,
• Automata
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
74
Temporal Logics
• Logics well-known for precise specification,
• amenable to symbolic manipulations.
• used in a variety of contexts:
• Propositional Logic/Boolean algebra for
combinational HW
• Predicate logics for software
• Higher order logics for language semantics.
• Temporal logic for hardware and protocols.
• Qualitative temporal statements
• Examples:
• If it is cloudy, eventually it will rain
• It never rains here
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
75
Properties of Hardware blocks
• Temporal in nature
• At any time only one units is accessing the
bus
• every request to access the bus is granted
ultimately.
• Two Kinds of TL
• Linear Temporal Logic (LTL):
• Time is a linear sequence of events
• Branching time temporal logic (CTL, CTL*):
• Time is a tree of events
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
76
Computational Tree Logic (CTL)
• CTL formulae describe properties of Computation
Trees
• Computation Trees are obtained by unwinding the
transition system model of blocks
• Branching structure due to nondeterminism
• CTL is the simplest branching temporal logic
• CTL* is more powerful, includes CTL and LTL
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
77
Syntax of CTL
• Every atomic proposition is a CTL formula
• If f and g are formulae then so are
• f, (f  g), (f  g), (f  g), (f  g)
• AG f - in all paths, in all state f (in all future, f)
• EG f - in some path, in all states f
• AF f - in all paths, in some state f (in every future f)
• EF f - in some future f
• A(f U g) - in all paths, f holds until g
• E(f U g) - in some path, f holds until g
• AX f - in every next state, f holds
• EX f - in some next state f holds
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
78
Examples




AG ¬ (farm_go  high_go_B)
AGAF (farm_car  AF(farm_go))
AG (mem_wr U mem_ack)
EF (req0 U grant0 )
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
79
Model Checking
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
80
Automatic Verification
• Model Checking and Language Containment
• For finite state systems like Hardware blocks,
protocols and controllers.
• Systems modeled as transition systems or automata
• Specifications temporal formulae (LTL, CTL) or
automata
• Verification:
• Model Checking: A finite state system or automaton
satisfies a temporal logic specification iff it is a
model of the formula.
• Language Containment: An automaton model (M) of
the system satisfies an automaton specification (S)
if the language of M is contained in that of S.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
81
CTL model checking
(Clarke and Emerson, Quielle and Sifakis)
M╞ F
• M Transition System and F, CTL formulae
• M defines a tree (unwind the Transition System)
• F specifies existence of one or all paths
satisfying some conditions.
• Verification involves checking whether these
conditions hold for the tree defined by M.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
82
EXAMPLE
• Which of the following hold ?
• AG p, EF¬q, AX p, AG ¬q, EG ¬q, AX(p  q)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
83
CTL Verification by Explicit Enumeration
• Iterative labeling algorithm that labels all the states
with sub formulae.
• Start from the initial labels of atomic propositions
• Iteratively add sub formulae as labels with each
state based on the following equations:
EF p = p  EX p  EX(EX p) 
EG p = p  EX p  EX(EX p)  
E (q U p) = p  (q  EX p)
 (q  EX(q  EX p))

ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
84
CTL Verification
• Iteration terminates since states and subformulae
are finite.
• If initial states are labeled with the given formula
then the model checking succeeds
• if it fails, counterexample can be generated
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
85
Illustration
• To compute EF p which is:
• EF p = p  EX(p)  EX(EX(p))  . . .
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
86
Illustration contd.
Iterative computation
• I step :
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
87
Illustration contd.
• II step :
• III step :
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
88
Illustration contd.
• Computation terminates
• EF p Holds in all striped states
• Computation involves backward breadth first
traversal and calculation of Strongly Connected
Subgraphs (cycles)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
89
2. Compute EG p in
EG p = p  EX p  EX(EX p)  . . .
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
90
Illustration contd.
Start with
I iteration
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
91
Illustration contd.
II iteration
III iteration
Iteration terminates
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
92
Complexity of CTL model checking
•
•
•
•
Algorithm involves backward traversal
Linear on the sizes of both formulae and model
Size of the model exponential in size of latches
Reduction Techniques:
• Symbolic Model checking Techniques
• Compositional Verification
• Symmetry based reduction
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
93
Verification
by
Theorem Proving
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
94
Theorem Proving
• Classical technique
• Most general and powerful
• non-automatic (in general)
Idea
• Properties specified in a Logical Language
(SPEC)
• System behavior also in the same language
(DES)
• Establish (DES  SPEC) as a theorem.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
95
A Logical System
• A language defining constants, functions and
predicates
• A no. of axioms expressing properties of the
constants, function, types, etc.
• Inference Rules
A Theorem
• `follows' from axioms by application of inference
rules has a proof
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
96
Proof
• Syntactic object
A1, A2, . . . , An
• A1: axiom instance
• An: theorem
• Ai+1 - Syntactically obtainable from
• A1, . . . , Ai using inference rules.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
97
Examples
•
•
Propositional logic and its natural deduction
system
Prove SNi=1 i = N(N + 1)/2, using Peano's axioms
and mathematical induction
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
98
Full Adder
• sum := (x  y)  cin
• cout := (x  y)  ((x  y)  cin)
Theorem: sum = x + y + cin – 2 * cout
Proof : Use properties of boolean and arithmetic
operators.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
99
Problems with the approach
• Verification is a laborious process
• Manual proofs could contain error
• If proof exists, system is correct otherwise, no
conclusion.
Interactive Theorem Provers
• Ease the process of theorem proving
• Proof-Checking
• Decision Procedures
• Proof Strategies
• Theory building
• Many systems are available: Nqthm, PVS, HOL,
Isabelle, etc.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
100
Binary Decision Diagrams
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
101
Boolean Function Representation
• Boolean logic: Foundation of digital design
• Need to represent and manipulate Boolean
functions efficiently
• Common representations:
• Truth table, Karnaugh map, Canonical sumof-products
• Size always 2n for n-arguments
• Operations (e.g. AND, NOT) inefficient
• Inappropriate for practical applications
• E.g., representing carry-out function of
64-bit adder
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
102
Binary Decision Diagrams (BDDs)
• A graphical representation [Bryant ’96]
• Allows efficient representation & manipulation
of Boolean functions
• Worst-case behavior still exponential
• Example: f = x1.x2 + x3’
1
0 x
• Represent as binary tree
1
x2
x2
• Evaluating f:
• Start from root
x3
x3
x3
• For each vertex xi
left branch if xi = 0
0 1
1
0 1
0 1
else right branch
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
103
x3
1
BDDs
• Underlying principle: Shannon decomposition
• f(x1, x2, x3) = x1.f(1, x2, x3) + x1’.f(0, x2, x3)
= x1. (x2 + x3’) + x1’. (x3’)
• Apply recursively to
x1
f(1, x2, x3) and f(0, x2, x3)
x2
x
2
• Extend to n arguments
x3
x3
x3
• Number of nodes can be
0 1
1
0 1
0 1
exponential in number of
f = x1.x2 + x3’
arguments
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
104
x3
1
Restrictions on BDDs
• Ordering of variables
• In all paths from root to leaf, variable labels of
nodes must appear in specified order
• Reduced graphs
x1
• No two distinct vertices
x2
x3
represent same function
x2
x2
x3
• Each non-leaf vertex has
distinct children
0 1
1
0 1
0 1
f = x1’.x2’ + x1.x2 + x1.x3’
REDUCED ORDERED BDDs (ROBDDs): DAG
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
105
x3
1
ROBDDs
x1
• Example: f = x1.x2 + x3’
x2
x3
• Properties
• Unique representation of f for given 0
1
variable ordering
• Checking f1 = f2: ROBDD isomorphism
• Shared subgraphs: size reduction
• Every path might not have all labels
x1
x2
• Every non-leaf vertex has
x2
path(s) to 0 and 1
x3
x3
x3
So far good !
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
1
0
1
0 1
0
1
106
1
Variable Ordering Problem
f = x1.x2 + x3.x4 + x5.x6
1
Order 1,3,5,2,4,6
5
5
5
4
3
5
2
2
2
2
Order 1,2,3,4,5,6
3
3
1
4
2
5
4
6
6
0
1
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
0
1
107
Variable Ordering Problem
• ROBDD size extremely sensitive to variable ordering
• f = x1.x2 + x3.x4 + … + x2n-1.x2n
• 2n+2 vertices for order 1, 2, 3, 4…2n-1, 2n
• 2n+1 vertices for order 1, n+1, 2, n+2,…n, 2n
• f = x1.x2.x3….xn
• n+2 vertices for all orderings
• Output functions of integer multipliers
Exponential size for all orderings [Bryant ‘91]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
108
Variable Ordering Problem
• Determining best variable order to minimize BDD
size
• NP-complete [Bollig, Wegener ‘96]
• Heuristics:
• Static and dynamic ordering [Fujita et al ‘92,
Rudell ‘93]
• Sampling based schemes [Jain et al‘98]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
109
Operations on BDDs
Operation
• Reduce
• G reduced to canonical form
Complexity
O(|G|)
• Apply
O(|G1||G2|)
• Any binary Boolean op: AND, XOR …
• Compose
O(|G1|2|G2|)
• g1(x1, x2, x5) composed with g2(x3, x4)
at position of x2: g1(x1, g2(x3,x4), x5)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
110
Operations on BDDs (Contd.)
Operation
• Satisfy-one
• Assignment of x1, … xn
for which f(x1,… xn) = 1
• Restrict
• ROBDD for f(x1, x2, …,1, ... xn)
or f (x1, x2, … 0 … xn)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Complexity
O(n)
O(|G|)
111
Operations on BDDs
• Operators: Take ROBDD arguments, return
ROBDD result.
• Complexity polynomial in BDD size
• BDD size limiting factor in most applications
• Ongoing research on avoiding BDD blowup
• Variable ordering, Partitioned BDDs,
Implicitly conjoined BDDs etc.
• Quantification with BDDs
•  x1. f(x1, x2, x3) = f(0, x2, x3) + f(1, x2, x3)
•  x1. f(x1, x2, x3) = f(0, x2, x3) . f(1, x2, x3)
• Useful in Symbolic Model Checking
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
112
BDD Packages/Libraries Out There
• CUDD package (Colorado University)
http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
• Carnegie Mellon BDD package
http://www-2.cs.cmu.edu/
afs/cs/project/modck/pub/www/bdd.html
• TiGeR BDD library (commercial package)
• CAL (University of California, Berkeley)
http://www-cad.eecs.berkeley.edu/
Respep/Research/bdd/cal_bdd/
• BuDDy
http://www.itu.dk/research/buddy
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
113
BDD Packages/Libraries Out There
• ABCD
http://i10www.ira.uka.de/armin/abcd/index.html
• BDDNOW
http://www.diku.dk/students/lordtime/bddnow.tar.gz
• PPBF
http://www-2.cs.cmu.edu/~bwolen/software/ppbf/
• ...
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
114
Applications of BDDs
• Extensively used in CAD for digital hardware
• Some applications (partial listing)
• Combinational logic verification through
equivalence checking
• Sequential machine equivalence
• Using combinational equivalence of nextstate logic
• Symbolic model checking
• Automatic test pattern generation (ATPG)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
115
Applications of BDDs
• Timing verification
• Representing false paths in circuits
• Representing discrete time encoded in
binary
• Symbolic simulation
• Assigning symbolic values to circuit inputs
and determining symbolic output values
• Symbolic trajectory evaluation
• Checking temporal properties over
sequences of symbolic values
• Logic synthesis and optimization
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
116
Combinational Equivalence
Checking
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
117
Combinational Equivalence Checking
Design 1
Design 2
• Given two combinational designs
• Same number of inputs and outputs
• Determine if each output of Design 1 is functionally
equivalent to corresponding output of Design 2
• Design 1 could be a set of logic equations/RTL
• Design 2 could be a gate level/transistor level
circuit
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
118
Right Fit for ROBDDs
• ROBDD for every function is canonical
• Construct ROBDDs for each output in terms of inputs
• Use same variable order
• Check if the graphs are isomorphic
• ROBDD isomorphism is simple
• Alternatively
Design 1
Design 2
F
Designs functionally equivalent
if and only if F is identical to 0
(0 for all inputs)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
119
ROBDDs in Equivalence Checking
• Problem reduces to checking F for unsatisfiability
• If ROBDD has a non-leaf vertex or a 1 leaf, F is
satisfiable
• But there are problems …
• For 32 bit multiplier, there are 64 inputs and
BDD blows up
• Same is true for other real-life circuits
• Interestingly, several of these are actually
easy to check for equivalence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
120
ROBDDs in Equivalence Checking
• Something smarter needed …
• Worst case must still be exponential
complexity
• Unsatisfiability: co-NP complete!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
121
Using Structural Information
• Structural similarities between designs help
A1
B1
A2
B2
• If A1 equivalent to A2 & B1 equivalent to B2,
Design1 equivalent to Design2
• Simplifies equivalence checking
• But consider
A1
B1
A2
B2
B1 not equiv to B2, but Design 1 equiv to Design 2
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
122
Using Structural Information
• False negative
Analysis indicates designs may not be equivalent, but
designs are actually equivalent
• Use logical implication to reduce false negatives
• If out1 is not equivalent to out2, out1 out2 is satisfiable
• Express out1 out2 in terms of internal signals in
design1 and design2
Design 1
F
Internal
signals
Design 2
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
123
Method of Implication
• Derive set of internal signals that must be not
equivalent if out1 out2 is satisfiable
• Propagate implications back towards inputs
• Stop when
• Primary inputs reached
• Two primary inputs never equivalent
• So, out1 out2 is satisfiable
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
124
Method of Implication
• Stop when
• Internal signals reached are known to be
equivalent
• Conclude out1 out2 is unsatisfiable
• So, out1 is equivalent to out2
• Some pairs of signals can be quickly identified as
not equivalent by random simulation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
125
Structural Simplifications
• Once two internal signals are found equivalent,
the circuit can be simplified
• Suppose outputs of corresponding AND gates
are equivalent
Helps reduce size of circuit to deal with later
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
126
An Efficient Equivalence Checker
• Finds pairs of equivalent signals in two designs
[Matsunaga ‘96]
Start
Random simulation  CEP list
More pairs
to verify?
NO
YES
Verify pair, update VEP list
and CEP list,
Restructure circuit
End
CEP: Candidate
equivalent
pairs
VEP: Verified
equivalent
pairs
Check if primary output
pair is in VEP list
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
127
Some Observations
• Most non-equivalent pairs filtered by random simulation
• Equivalent pairs identified early by proper choice of
internal variables when propagating implications
backwards
• If pair under investigation is expressed in terms of
already known equivalent pairs, we are done!
• Leverage Automatic Test Pattern Generation (ATPG)
techniques to detect when a pair is not equivalent
Targets implementation error, error due to translation or
incremental modification, NOT design error
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
128
Checking Arithmetic Circuits
• Equivalence checking of multipliers acknowledged to
be hard
• ROBDD blowup for bit-level representation
• Multiplicative Binary Moment Diagrams (*BMDs)
[Bryant, Chen ‘95]
• Boolean assignment of variables maps to a
number (integer, rational)
• Canonical representation of linear functions, e.g.
integer multiplication
• Word level representation of function
• Allows efficient verification of multipliers and other
arithmetic circuits
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
129
Sequential Machine Equivalence
• Restricted case: Reduces to combinational
equivalence
• Given machines M1 and M2 with correspondence
between state and output variables
• Checking equivalence of M1 and M2 reduces to
equivalence checking of next-state and output
logic
Comb
Logic1
Comb
Logic2
FF
FF
Given Equivalence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
130
Equivalence Checking - Extensions
• For best results, knowledge about structure
crucial
• Divide and conquer
• Learning techniques useful for determining
implication
• State of the art tools claim to infer information
about circuit structure automatically
• Potentially pattern matching for known
subcircuits -- Wallace Tree multipliers,
Manchester Carry Adders
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
131
Equivalence Checkers Out There
• Commercial equivalence checkers in market
• Abstract,
• Avant!,
• Cadence,
• Synopsys,
• Verplex,
• Veritas (IBM internal) ...
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
132
Symbolic Model Checking
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
133
Model Checking Sequential Circuits
• Given:
• A sequential circuit
• Finite state transition graph
MODEL
• Flip-flops with next-state logic
• Transition relation between present and
next states
• A property in specialized logic
SPECIFICATION
• Prove that MODEL satisfies SPECIFICATION
• In case of failure, counterexample desirable
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
134
Example: 3-bit Counter
x2
X2
X1
x1
X0
x0
Clk
Model
State transition graph
defined by
X0 = NOT(x0)
X1 = XOR(x1, x0)
X2 = XOR(x2, x0. x1)
Property
State x0, x1, x2 = 111
is reached infinitely
often starting from
state 000
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
135
Basic Approaches
• Explicit state model checking
• Requires explicit enumeration of states
• Impractical for circuits with large state spaces
• Useful tools exist: EMC, Murphi, SPIN, SMC …
• Symbolic model checking
• Represent transition relations and sets of states
implicitly (symbolically)
• BDDs used to manipulate implicit representations
• Scales well to large state spaces (few 100 flip flops)
• Fairly mature tools exist: SMV, VIS, FormalCheck ...
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
136
Model Checking
• Reachability analysis
• Find all states reachable from an initial set S0
of states
• Check if a safety condition is violated in any
reachable state
• CTL property checking
• Express property as formula in Computation
Tree Logic (CTL)
• Check if formula is satisfied by initial state in
state transition graph
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
137
Symbolic Model Checking
• For 3-bit counter, set of states x0, x1, x2 = {000,
010, 011, 001} can be represented by S (x0, x1,
x2) = S(x) = x0’.
x0
BDD:
1
0
• Set of state transitions can be represented
by N (x0, x1, x2, X0, X1, X2) = N (x, X) =
(X0
x0’) (X1
x1
x0) 
(X2
x2
(x1. x0))
BDD:
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
x0
1
0
138
Forward Reachability
• Start from set S0 of states
• Set of states reachable in at most 1 step:
S1 = S0  { X |  x in S0  N(x, X) = 1}
S1
S0
Expressed as Boolean functions:
Given S0 (x0, x1, x2),
S1 (X0, X1, X2) = S0 (X0, X1, X2) 
 x0, x1, x2 . [S0 (x0, x1, x2) 
N(x0, x1, x2, X0, X1, X2)]
Given BDDs for S0 and N, BDD for S1 can be obtained
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
139
Forward Reachability
• Compute S1 from S0, S2 from S1, S3 from S2, …
• Predicate transformer F: Si+1 = F (Si)
• Continue until Sk+1 = F (Sk) = Sk
• Least fixed point of F
• Sk = Set of all states reachable from S0
• Computed symbolically -- using BDDs
• Very large state sets can be represented compactly
S0
Reachable
states
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
140
Backward Reachability
• Give a set Z0 of states
• Compute set of states from which some state
in Z0 can be reached.
• Analogous to forward reachability with minor
modifications
Z0
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
141
Checking Safety Conditions
• Safety condition must ALWAYS hold
• E.g. Two bits in one-hot encoded state cannot be 1
• Z = set of states violating safety condition
• Given S0 = set of initial states of circuit,
• Compute R = set of all reachable states
• Determine if Z intersects R, i.e. (Z  R)  0
• If YES, safety condition violated
Satisfying assignment of (Z  R): counterexample
• If NO, circuit satisfies safety condition
• All computations in terms of BDDs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
142
Checking Safety Conditions
• Start from Z = set of “bad” states
• Find by backward reachability set of states B that
can lead to a state in Z
• Determine if S0 intersects B
S0
S0
B
R
Z
Forward Reachability
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Z
Backward Reachability
143
CTL Properties
• “Once req goes high, grant eventually goes high”
• Not expressible as safety property
• Use formulae in Computation Tree Logic (CTL)
• CTL formulae at state S0
S0
Atomic proposition: x1 = x2 = x3 = 0
AG f: In all paths from S0, f holds globally
AF f: In all paths from S0, f holds finally
AX f: In all paths from S0, f holds in next
state
Computation tree
A[f U g]: In all paths from S0, g holds
of states
finally, and f holds until then
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
144
More on CTL
• EG f, EF f, EX f, E [f U g] defined similarly
• “There exists a path from current state …”
• f and g can themselves be CTL formulae
• E.g., AG AF (x1  x2)
• x1 or x2 is satisfied infinitely often in the future
• Recall 3-bit counter example:
• “ The state x0, x1, x2 = 111 is reached infinitely
often starting from 000”
• x0’  x1’  x2’  AG AF (x0  x1  x2)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
145
CTL Model Checking
• Clarke, Emerson, Sistla proposed algorithm for
CTL model checking on explicit state graph
representation [Clarke et al ‘86]
• Linear in graph size and formula length
• Burch, Clarke, Long, McMillan, Dill gave algorithm
for CTL model checking with BDDs [Burch et al’94]
• Suffices to have algorithms for checking EG f, EX f,
and E [f U G]
• Other formulae expressed in terms of these
• EF f = E [true U f]
• AF f =  (EG (  f))
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
146
Symbolic CTL Model Checking
• Given a model with set S0 of initial states and a CTL
formula f
• To determine if f is satisfied by all states in S0
• Convert f to g that uses only EX, EG, E[p U q]
• CHECK(g) returns set of states satisfying g
• If g = atomic proposition (e.g., x1. x2 + x3), CHECK
returns BDD for g
• If g = EX p, EG p, E[p U q], CHECK uses reachability
analysis to return BDD for set of states
• Worst-case exponential complexity
• Finally, determine if S0  CHECK(g)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
147
State of the Art
• Techniques to address memory/runtime bottlenecks
• Partitioned transition relations
Addresses BDD blowup in representing transitions
• Early quantification of variables
Addresses BDD blowup during image computation
• Iterative squaring
Exponential reduction in number of steps to fixed
point
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
148
State of the Art
• Techniques to address memory/runtime bottlenecks
(contd.)
• Use domain knowledge to order BDD variables and
order quantified variables
• Modified breadth first search
To explore state space of loosely coupled systems
• Active ongoing research …
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
149
State of the Art
• Symbolic model checkers can analyze sequential
circuits with ~ 200 flip flops
• For specific circuit types, larger state spaces have
been analyzed
• Frontier constantly being pushed
• Abstract, Avant!, IBM, Cadence, Intel & Motorola
(internal) ...
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
150
State of the Art
• Specifying properties in specialized logic often daunts
engineers
• Better interfaces needed for property specification
• Monitor-based model checking
• Monitor observes system states and flags when
something “bad” happens
• Property to check: “Does monitor ever raise flag?”
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
151
Related techniques
• Model checking for bugs
Prioritize state space search to direct it towards bugs
• Start from error state and current state
• Compute pre-image of error states & image of
current state
• Choose states for further expansion in order of
their “proximity” to pre-image of error states
• Proximity metrics: Hamming distance, tracks,
guideposts [Yang, Dill ‘98]
• Helps find bugs in erroneous circuits quickly
• No advantages if circuit is bug-free
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
152
Related techniques
• Approximate Model Checking
Representing exact state sets may involve large BDDs
Compute approximations to reachable states
• Potentially smaller representation
Buggy states
• Over-approximation :
• No bugs found  Circuit verified correct
• Bugs found may be real or false
Reachable states
• Under-approximation :
• Bug found  Real bug
• No bugs found  Circuit may still contain bugs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
153
Related techniques
• Bounded model checking
• Check property within k steps from given set S0 of
states
• S0
F(S0)
F2(S0)
… Fk(S0)
• Unroll sequential machine for k time steps
PI
PO
PS
NS
PI1
PI2
PI0
S1
S0
S2
S3
• To check property Z, test satisfiability of
(S0  Z) 
 (S0  Z) 
(S1  Z)
 … (Sk  Z)
• Leverages work done on SAT solvers
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
154
Semi-formal Methods
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
155
Semi-formal Verification
• Formal verification still a bottleneck
• Simulation and emulation not keeping up with
design complexity
• Designs with bugs being produced
• FV methods haven’t yet been able to scale to
all types of industry designs
• Fundamental complexity limits restrict how
much FV can do
• Need some viable alternative
• Use a hybrid of testing, simulation and formal
methods to fill the gap
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
156
Semi-formal Verification
Simulation
Driver
Simulation
Engine
Simulation
Monitor
Symbolic
Simulation
Guided vector
generation
Diagnosis of
Unverified
Portions
Conventional
Coverage
Analysis
Extension
Devadas and Keutzer’s proposal:
A pragmatic suggestion for SOC verification
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
157
Semi-formal Verification
• Smart simulation:
• Maximize chances of detecting bugs at small cost
• Coverage metrics crucial
• Code based (conditionals/assignments in HDL)
• Circuit-structure based (node toggle)
• State-space based (states reached)
• Functionality based (user defined event sequences)
• More to come ...
• Use metrics to determine
• Unexercised parts of design: Guide vector generation
• Adequacy of verification: When to stop?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
158
Semi-formal Verification
• Metric Coverage
• Measure of how adequately design is
exercised
• A measure of controllability
• Observability is another major issue
• Must propagate a mismatch in an internal
signal value (which can cause problems later
on) to the observable outputs
• “White Box” techniques help
Assertion checkers [0-In]
• Techniques from testing can be borrowed
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
159
Semi-formal Verification
• Coverage + observability can be used to direct
simulation
• Test generation
• Model design errors by fault model (e.g. stuckat)
• Generate tests automatically that maximize
coverage metric per test simulation cycle
• Sequential ATPG methods can be used
• But hard problem in general!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
160
Semi-formal Verification
• Test generation (contd.)
• Generate tests for FSMs (deep inside design)
using model checking techniques
• Map test inputs of FSM deep inside design
to design inputs
• User guided
• Automatic using sequential ATPG
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
161
Semi-formal Verification
• Test Amplification
• Make use of interesting test cases already
generated by ATPG or user
• Explore behavior “near” tested region of state
space
• Rationale: Generated tests may take the
design into an error-prone corner but may
not detect any/all errors there.
• Goal : Detect as many “near-miss” bugs as
possible by looking around paths taken by
known tests
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
162
Semi-formal Verification
• Partial model checking
• When BDDs start to blow up, delete part of state
space from consideration
• Choose parts to delete such that maximum
number of states can be explored with given
resources
• Hash tables in explicit model checking to prevent
blow-up of state space
• Aliasing problem
• Suitable choice of hashing function gives very
low alias prob
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
163
Interface Specification
for
Divide & Conquer Verification
(T. Nakata)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
164
Constraints in Module Verification
Properties
Input
constraints
Module
under
verification
Verification engine
• Constraints problem in a case study
• Not specified by the designers
• Defined by verification team through verification process
Result: # of constraints=1818, # of properties=118
(# of constraints < 50 if correctly specified)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
165
Two Ways to Define Constraints
Module
under
verification
Module
under
Interface
verification
specification
language
// PSE_BGN
// PSE_ERR
[ data == ‘CLD ]
[ data != ‘CB ]{,1}
[ data == ‘CB ]
// PSE_END
Add pseudo module
to inputs
Specify constraints by
a certain language
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
166
Category of I/F Spec. Languages
• Verification languages
e, VERA, TestBuilder, …
• Special syntax in HDLs or system description
languages
SystemC, SpecC, VHDL+, …
• Dedicated languages for I/F specification
OwL, CWL, …
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
167
Design and Verification Support
I/F
specification
Sim. pattern
generation
Coverage
criteria
Checker
generation
I/F
Synthesis
Verification support
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Spec. sheet
generator
Design support
168
Verification Support (1)
• Checker generation
• Input constraint checker that rules out invalid
transactions
• Output checker that checks consistency to
specification
Error
Module
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
169
Verification Support (2)
• Simulation pattern generation
• Random pattern generator in conformance
with input constraints
Good
pattern
Module
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
170
Verification Support (3)
• Abstraction level converter for verification scenarios
• Conversion between transaction-level and signal-level
scenarios*
* e.g. TestBuilder TVM generator
do {
wait();
} while
(!grant);
m1.write(d);
Scenario
Comparison
Module
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Level
converter
171
Example of I/F Specification Language
CWL (Component Wrapper Language)
• Jointly developed by Hitachi and Fujitsu
• Hierarchical description aimed at abstraction
level conversion
• Support for split transactions
• Support for useful interface patterns
• Arrays
• FIFOs
• Priority queues
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
172
Hierarchical Description: Base
clk
rst
en
ad[9:0]
a
wait
dt[7:0]
d
I
N
signalset all =
N
:
I
:
Q(a):
W
:
S(d):
endsignalset
Q(a)
W
W
S(d)
N
{clk,rst, en, ad,wait,dt};
{ R, 1, 1, x, 1, x};
{ R, 0, x, x, 1, x};
{ R, 1, 0, a, 1, x};
{ R, 1, 1, x, 0, x};
{ R, 1, 1, x, 1, d};
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
173
Hierarchical Description: Transaction
clk
rst
en
ad[9:0]
a
wait
dt[7:0]
d
I
N
reset nop
Q(a)
W
W
read(a,d)
S(d)
N
nop
word;
nop
: N ;
reset
: I ;
read(a,d) : Q(a) W* S(d) ;
endword
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
174
Hierarchical Description: Sentence
clk
rst
en
ad[9:0]
a
wait
dt[7:0]
d
I
N
reset nop
Q(a)
W
W
read(a,d)
S(d)
N
nop
sentence
sentence;
reset [ nop | read ]+ ;
endsentence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
175
Split Transactions
I
N
reset nop
N
Q1 Q2 S1 Q3 S2 S3
nop read1
read1
read2
read2
read3
read3
sentence;
INITIAL:
reset;
FOREGROUND:
read;
BACKGROUND:
nop;
endsentence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
176
Summary
• Interface specification is crucial in module
verification
• Design and verification support from I/F spec.
• Activities in I/F specification languages
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
177
Techniques for
System Verification
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
178
Symbolic Simulation
and
Symbolic Trajectory Evaluation
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
179
Symbolic Simulation
• Conventional simulation
• Combinational circuits: Output for a given set of
inputs
• Sequential circuits: Output for a given initial state
and sequence of inputs
• Inputs and initial state are specified constants
• Output is also a constant
• # Constant input combinations too large!
• Alternative approach
• Allow symbolic variables as inputs and initial state
• Compute outputs & states as symbolic expressions
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
180
Symbolic Simulation
• A symbolic expression represents a set of values
• Inputs: x = a, y = b, c = b’
• Output: f(x,y,z) = a + b’ represents set of values at
output on applying 001, 010, 101 and 110 to inputs
• Result of multiple simulations in one pass
• Examine expression for outputs to see if desired
property is satisfied
Primary outputs
a, 1, a
a’, b, a + b
Initial state S
Sequential
Circuit
F1(a,S), F2(a,b,S), F3(a,b,S)
Next states
G1(a,S), G2(a,b,S), G3(a,b,S)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
181
Low-level Symbolic Simulation
• Symbolic simulation at gate and MOS transistor level
• Variables can take value {0, 1, X}
• X represents an unknown state of the signal
• Boolean functions extended to operate on {0, 1, X}
• AND(0, {0,1,X}) = {0}
• AND(1, {1,X}) = {1,X}
• AND(X, {X})
= {X}
• Common use of X: Representing uninitialized state
variables
• Outputs can be checked to see if desired value
appears
• Simulators: COSMOS, Voss, Innologic, Intel Labs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
182
Low-level Symbolic Simulation
• {0, 1, X} encoded in binary
0: 00
1: 11
X: 01
• Two binary variables used to represent each symbolic
variable
• Extend operations to pairs of binary variables
• AND( (a,b), (c,d) ) = (AND(a,c), AND(b,d))
• Each signal value now represented using two BDDs
• Generalizing, a vector of BDDs encodes a symbolic
expression
• Operation on symbolic expressions = Operation on
BDD vectors
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
183
High-level Symbolic Simulation
• Variables: boolean, bitvectors, int, reals, arrays …
• Operations:
• Arithmetic, logical, bitvector operations
• Uninterpretted functions, equality, disequality
• Final expression contains variables and operators
• Decision procedures needed to check whether final
expression is as desired
• Final expressions can also be manually checked for
unexpected terms/variables, flagging errors -- e.g. in
JEM1 verification [Greve ‘98]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
184
High-level Symbolic Simulation
• Manipulation of symbolic expressions done with
• Rewrite systems like in PVS
• Boolean and algebraic simplifiers along with
theories of linear inequalities, equalities and
uninterpretted functions
• Extensively used along with decision procedures
in microprocessor verification
• Pipelined processors: DLX
• Superscalar processors: Torch (Stanford)
• Retirement logic of Pentium Pro
• Processors with out of order executions
• JEM1 (no decision procedures used) ...
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
185
Symbolic Trajectory Evaluation (STE)
• Trajectory : Sequence of values of system
variables
• c = AND (a, b) and delay is 1
• A possible trajectory : (a,b,c) = (0, 1, X), (1, 1, 0),
(1, 0, 1), (X, X, 0), (X, X, X) and so on
• Express behavior of system model as a set of
trajectories I and express desired property as a
set of trajectories S
• Determine if I is inconsistent with S
Inconsistent: I says 0 but S says 1 for a signal
at time t
Consistent: I says 0 but S says X or 0 for a signal
at time t
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
186
STE
• Several success stories with STE
• Verification of memories, TLBs in Power PC
• Verification of instruction length decoder in
Intel x86 architecture
• Verification of Intel FP adder
• Microprocessor verification, ...
• Enables efficient analysis of much larger state
spaces than symbolic model checking
• However, properties that can be checked are
restricted compared to CTL
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
187
Hybrid Verification
(S. P. Rajan)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
188
Hybrid Verification
• Formal Verification using
• Theorem Proving + Model Checking (PVS)
• PVS = Prototype Verification System (SRI
International)
• Tight integration of theorem prover and model
checker
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
189
Hybrid Verification
Model Checker
Model-Check
Simplify
Hardware
Specification Decision
Procedures
data-structures
Rewrite
Assert
Properties
to be
Verified
Basic
Decision
Procedures
BDD
Arith
Rewriter
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
190
PVS System Overview
• Powerful specification language
• Based on typed-higher-order logic
• Can express VHDL/verilog specifications
• Parametric specifications
• Combines theorem proving and model checking
(using BDDs)
• Currently, there is no tool that can match PVS in
the combined features of specification &
verification
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
191
PVS System Overview
• Decision procedures including BDDs and modelchecking in PVS
• Support for verification strategies and quick
proof prototyping
• Support for quick debugging: theory extensions
on the fly
• PVS used to verify commercial designs (AAMP-5,
Rockwell Collins)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
192
PVS Drawbacks
• Developing semi-automatic proof strategies
difficult
• Large designs might challenge PVS resource
usage
• VHDL/verilog to PVS translators yet to be
developed (significant effort needed)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
193
Emulation
(Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
194
Emulation Systems
• Systems using hardware emulators to do physical
prototyping.
Hardware emulators : Specially designed h/w & s/w
systems using reconfigurable h/w such as FPGAs.
Implements a design by mapping it to these FPGAs,
which are mounted in fixed arrays on PCBs in a
dedicated piece of equipment that communicates
with the design environment.
• Prototype Design – Checked for functional
correction
• In Circuit Emulation - Emulator can also be
connected to target system.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
195
Emulation Systems
• Emulation justified when
• Absolute real time performances not required
• Simulation is extremely slow
• Design complexity significant
• Few bugs related to system integration remain
• Though accelerates simulation runs, debug and
design iterations can be long due to setup costs.
• Usually follows static functional verification of
modules.
• Emulation requires an additional design flow
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
196
FPGAs as logic emulators
• ~ Several trillion gate evaluations/sec.
• Efficient high end synthesis tools available.
• Multiple FPGA board architectures give >5 million
gates (can be extended to 10 –15 million gates) –
Can target entire SoC designs.
• Same architecture can be re-used for other designs.
• Programmable interconnect makes it possible to
achieve optimal mapping of partitioned RTL
behaviors to different FPGAs.
• Can be tested by ICE or by test vectors.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
197
Emulation Flow
Error
Verilog
RTL
Code
Behavioral
Simulation
Netlist
Synthesis
Gate
Level
Simulation
•Import Netlist
•Generate Memory
•Clock Analysis
•Constraint
•Design Partition
•System Setup
•Vector Translation
•Vector Debugging
•ICE Setup
•Target Interface
•Logic Analyzer Setup
Emulator Environment
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
In Circuit
Emulation
198
Total Emulation System
Host
Emulation
Hardware
LAN
Target
Interface
Module
WorkStation
PC
Target
Board
Clock
Source
Power
Target
System
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
ViewStore
199
Emulation Systems - Major components
• Hardware in emulation box
• Multiple PCBs & specialized parallel architecture
around FPGAs/board.
• 1 CPU/board : Hyb. Emln, Behav. Test Bench
• Interconnect : Programmable Crossbars,
Nearest Neighbor Time Multiplexing I/Os.
• Memories : SRAMs, DRAMs, SDRAMs
• Target Interface h/w : ICE cable & interface.
• Logic Analyzer or specialized h/w to capture o/p
response.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
200
Emulation Systems - Major components
• Software
• Specialized compiler/synthesizer for mapping
flattened RTL/gate netlists to emulation
hardware.
• Mapper uses Multiway, Multilevel partitioning
s/w to Multi-FPGA, Multi-Board emulator
target architecture.
• Specialized timing analysis for clocking
issues related to Multi-FPGA mapping.
• Execution software.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
201
Emulation Systems - Drawbacks
• Expensive & Proprietary hardware.
• Additional Design flow
• High designer skill in vendor specific tools.
• Design iterations can be time consuming.
• Requires high performance workstations
• On board memories require logic wrappers. DRAMs
& SDRAMs impose proper refresh strategies at
lower emulation speeds
• Needs careful attention to setup & hold times when
exercising test vectors.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
202
Emulation Systems - Drawbacks (contd.)
• Data buffers susceptible to overruns & underruns.
• Debugging difficult as errors can also arise due to
data interfaces to emulation model.
• Proprietary simulator
• ICE can impose target h/w to be slowed down.
• Inflexible due to interconnect architecture.
• SoCs will be limited by interconnect capacity.
• Facing competition : Simulation farms, Cheaper
Rapid Prototyping Systems.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
203
Commercial Emulators [Butts & Keutzer,’99]
• Cadence/Quickturn Mercury : 10M gates, Xilinx
FPGA, Two level time multi-plexed crossbar
interconnect, PowerPC/board (Verilog h/w
accelerator).
• IKOS VirtualLogic : 5M gates, Xilinx FPGAs, Nearest
neighbor time multiplexed interconnect (Virtual
Wires), Compiler analyzes clock trees to
synchronize time multiplexing.
• Axis Excite : FPGAs on PCI cards, Tightly coupled
to proprietary Verilog simulator.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
204
Quality of Verification
(Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
205
Quality of Verification
• Motivation
• Has verification been done comprehensively?
• All expected behavior excited & observed?
• Compare runs based on different approaches.
• Semi-Formal (Simulation + Model Checking)
• Stopping criteria (Intelligent Simulation)
• Formal (Model Checking)
• Adequacy of set of properties?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
206
Coverage Metric - Informal
• Coverage Metric helpful in detecting
• Useful structures in a design
• Useful classes of behavior
• Classification : Based on abstraction and level of
design representation [Dill, Tesiran, ICCAD 99].
• Code (HDL code)
• Circuit structure (Netlist)
• State space (STG)
• Functional (User defined tasks)
• Specification (Executable)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
207
Coverage Metric - Informal
• Different Coverage Metrics :
• Branch
• Expression
• FSM Arc
• Functional
• Hardware Code
• Path
• Signal
• Statement
• Toggle
• Triggering
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
208
Coverage Metric - Informal
• Desirable Qualities [Dill, Tesiran, ICCAD 99].
• Direct correspondence between metric & design
errors or bugs.
• Tolerable computational overhead to measure
coverage
• Reasonable analysis overhead
• Data interpretation
• High Coverage
• Stimuli generation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
209
Coverage Metric - Semi-formal
• Informal Coverage Metrics – Ad-hoc.
• Is it possible to formalize metrics for certain
classes of designs?
• Semi-formal [Gupta et. al. DAC 97]
• Mixes formal verification and simulation
approaches.
• Generate : Test model - Simple ( Formal Verification). Implementation model - Complex
(Simulation)
• Use FV to drive test set (test vector seqs.)
• Coverage : Defined on Test model.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
210
Coverage Metric - Semi-formal
• Can coverage on test model be translated into good
coverage on implementation model?
• Coverage of design behavior
• Coverage of design errors
• Guarantees w.r.t. completeness of validation.
• Test model derived from Implementation model
through abstraction of data path & control part. Can
this be made more precise?
• Gupta et. al. show under a reasonable set of
assumptions one can define metrics formally.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
211
Coverage Metric - Semi-formal
• New Coverage Metric(TTM) : Based on Transition
Tour on test model
• Transition Tour : A test set that covers each
transition in a FSM.
• Transition tours can catch all errors if there
exists an input which produces a unique
output in each state, & causes the FSM to
stay in the same state.
• Test model based on Mealy machine.
• Test generator – Uses FV techniques to
traverse reachable state space for desired
target coverage.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
212
Coverage Metric - Semi-formal
• Limitation : Does not cover all sequences (path
coverage). Not all errors exposed. Transition tour
metric can excite errors, but may not expose errors.
• Complete test set generation rules
• Application
• TTM used in processor verification
• General Purpose Processors
• Digital Signal Processors
• Case Study - DLX RISC Processor.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
213
Coverage Metric - Formal
• Formal Verification : Is system correct with respect
to a specification?
• How complete is the set of specification?
• Coverage Metric captures relevance of different
parts of the system for the verification process
when modifications are effected in the System
Under Verification (SUV)
• What does it mean for a specification Φ to cover a
system/circuit S?
• Does Φ describes S exhaustively?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
214
Coverage Metric - Formal
• Intuitively, uncovered part of S amenable to
modification without falsifying Φ in S.
• Different definitions of coverage implies different
ways in which parts of S can be modified.
• Captures errors in the modeling of a system
• Vacuous satisfaction of specification
  AG(req  AF grant)
• Captures errors in validity of specification
• Sanity checks for constraint validation (Eg.
Enabling conditions, Variable values & usage).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
215
Coverage Metric - Formal
• Completeness of Specifications
• Erroneous behavior not caught if no spec
captures this behavior
• Fully describe all possible behavior of system
• Check if system contains redundancies
• Simplify system
• Analyzing coverage in MC can find portion of
design not relevant for verification to
succeed.
• Coverage check – Feedback mechanism.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
216
Coverage Metric - Formal
• Approaches in Temporal Logic MC [Katz et. al., ‘99]
• Compare SUV with Tableau of spec Φ [An abstract system satisfying Φ and subsuming all
behavior allowed by Φ.]
• Detects portions irrelevant to satisfaction of Φ :
Behaviors indistinguishable by Φ & those
allowed by Φ but not generated by SUV
• Drawbacks : Imposes severe restriction on system
& its tableau, Supports only ACTL
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
217
Coverage Metric - Formal
• [Hoskote et. al., DAC 99] Coverage : Effect of modifications in system on satisfaction of the specs.
• Given, System : Modeled by a Kripke Structure, K;
Spec, Φ : A formula satisfied in K; q : Signal; w : A
state in K.
• Defn. : w in K is q-covered by Φ if K' derived from K
by flipping value of q in w no longer satisfies Φ.
• q-cover(K, Φ) : Set of states q-covered by Φ in K.
• CM Computation : Naïve – Perform model checking
of Φ in K' for each state w of K. {Acceptable ACTL }.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
218
Coverage Metric - Formal
• [Chockler et. al., CHARME 2000]: Distinction between ways to model a system.
• State based : Design Level (Hoskote et. al.)-System
modeled as a circuit with state space 2 v .
• Logic based : Implementation Level - Signal value
fixed to 0, 1, or X everywhere, then model check for
satisfaction of Φ.
• Closed system : No env. inputs (Kripke Structure).
• Open System : Inputs from environment + Outputs
supplied by system to environment; Modeled by
sequential machines; Coverage metric w.r.t. o/ps.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
219
Coverage Metric - Formal
• Coverage Metric Computation
• Naïve approach : Find set of covered states
(state based approach), or set of covered signals
(logic based approach) by model checking
every modified system.
• Alternative approaches
• Find uncovered parts of system
• Utilize overlaps among modified systems:
Each modification involves small change in
system.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
220
Coverage Metric - Formal
• Presentation of Output : What do we do after we
detect portions of system (or circuit) S that are not
covered w.r.t. a signal x?
• Compute : X = {x-cover(S, Φ) / for several x in O};
Coverage = | x-cover(S, Φ) | / |States in S|.
• Analysis : Is x-cover(S, Φ) empty? - Implies vacuity
(X can be used for generating uncovered computations). s in S not in x-cover(S, Φ)?- Implies Φ fails
to distinguish between S & S‘; Implies errors arising
out of erroneous values of signal x in s are not
captured by spec.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
221
Coverage Metric - Formal
• Advantages
• Applicable to full CTL.
• CM not sensitive to abstraction.
• CM is compositional
• Drawbacks
• Complexity of computing CM much greater
than that of model checking.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
222
Academic & Research Lab
Verification Tools
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
223
Verification Tools – 1
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
224
Verification tools
• A large number of tools exist
• Exhaustive review impossible
• For a comprehensive list and details:
• Formal Methods Home Page:
http://www.comlab.ox.ac.uk/archive/formalmethods.html
• Centre for Formal Design and Verification of
Software (CFDVS) at IIT Bombay
http://www.cfdvs.iitb.ac.in
• BRIEF review of a VERY FEW model-checking tools
in order now!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
225
VIS
• VIS Home page:
http:// www-cad.eecs.berkeley.edu/ Respep/Research/vis/
•
•
•
•
•
Verification Interacting with Synthesis.
A research prototype tool (Proof of Concept)
U. California, Berkeley (Brayton et. al.)
U.Texas, Austin, U.Colorado, Boulder
VIS integrates verification, simulation and synthesis
of finite state HW system.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
226
Modeling Language
• A subset of Verilog
• VHDL and Esterel planned
• The back-end language is BLIFF-MV
Specification Language
• CTL, CTL* and Automata
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
227
Verification
•
•
•
•
Symbolic Model Checking
Language Emptiness Check
Equivalence Checking of Combinational designs
Speciality:
• Simulation and Synthesis
• Various representations of Boolean functions
(BDD, MDD, etc.)
• variable ordering heuristics
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
228
Specification Examples
• AG ((bit[0] = 1)  AX (bit[0] = 0))
Flipping of the zeroth bit in a counter.
• AG ((Req = 1)  AF (Ack = 1) )
Every Req is greeted with an Ack eventually
• AG (EX:5 (State = TRST))
Always state TRST is reached in 5 steps.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
229
SMV
• Home page:
•
•
•
•
•
•
• http://www-cad.eecs.berkeley.edu/ kenmcmil/smv/
Experimental Research tool from Cadence Berkeley
Labs. (McMillan)
Originally from CMU (McMillan's Ph.D.thesis)
Modelling Language: Interacting State Machines,
Synchronous Verilog
Specification Language: CTL, LTL
Verification Approach: Symbolic Model Checking
Compositional and Symmetry-based Verification
Strategy
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
230
Modeling language
• Interacting state machines
• synchronous and asynchronous concurrency
• allow modular and hierarchical description of
finite state systems
• finite data types: Booleans, scalars, fixed arrays
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
231
Examples:
1.
MODULE MAIN
VAR
request : boolean;
state : {ready, busy}
ASSIGN
init(state):=ready;
next(state):=case
state=ready&request: busy
1 : {ready,busy } ;
esac;
SPEC
AG (request ® AF state = busy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
232
Examples:
1. Old Syntax
• `request' unconstrained (input)
• non-deterministic assignment
• OBDD representation of tr. reln. constructed and
SMC performed.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
233
Example - 3bit counter
MODULE main
VAR
bit0 : counter cell(1);
bit1 : counter cell(bit0, carry-out);
bit2 : counter cell(bit0, carry-out);
SPEC
AG AG bit2. carry-out
MODULE counter cell(carry-in)
VAR value : boolean;
ASSIGN
init(value) :=0;
next(value) := value+carry-in mod 2;
DEFINE
carry-out : = value & carry-in
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
234
Example - 3bit counter
• Assign sections of bit0, bit1 and bit2 execute in
parallel
• Data dependence respected
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
235
FC2toolset
Home page:
http://www-sop.inria.fr/meije/verification/
• Automatic Verification of Finite State
Communicating systems
• Form the basis for Esterel verification
• Developed at INRIA and Ecole de Mines, Sophia
Antipolis
• Based upon process algebra notation
• Modeling Language: CSP/CCS, Esterel (Xeve
tool)
• Specification language: abstract state machines
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
236
Verification Approach
• Comparison of specification machine with the
model after abstraction: use of Observational
Equivalence, Symbolic Bisimulation
• Compositional Minimization and Abstraction
• A very powerful notion of abstraction
(re-labeling complex sequence into a single label)
• Explicit and BDD representation of state machines
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
237
Example
DLX Controller
• An Esterel model
• 100s of states
• abstracted using FC2tools:
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
238
STeP
Homepage :
http://rodin.stanford.edu/
• Stanford Temporal Prover
• Interactive theorem proving tool for verification of
concurrent and reactive systems
• Combines model-checking and deductive
approaches and verifies
• parameterized(N-component) circuit designs
• parameterized(N-process) programs and
• programs with infinite data-domains
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
239
STeP
• Modeling Language: SPL and fair Transition
Systems
• Specification Language: LTL and First Order
Logic
• Verification Approach: Theorem Proving and
Model-checking
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
240
STeP overview
Reactive System
(SPL) Program
Temporal Logic
Formula
Hardware
Description
Fair Transition System
User
Automatic Prover
Model
Checker
Verification Rules
Strengthening
of Invariants
Propagation
P- valid
Counter example
P- valid
Bottom-up Invarient
Generator
First-order Prover
Simplification
Decision procedures
Interactive
Prover
Debugging Guidance
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
241
Verification in STeP
•
•
•
•
Very powerful theorem prover
Automatic Invariant Generation,
Collection of Simplification rules
Decision procedures for linear arithmetic, arrays,
bit vectors, etc.
• Generation of Verification Conditions
• BDD simplification
• Rich set of tactics and tacticals
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
242
An example SPL Program
main ::
[
in a : int where ((a 127) ^ (a > - 128))
in b : int where ((b<127) ^ (b > - 128))
out c, d : int
if (a > 0 ^ b > 0) then [
if (a > b) then [ 12 : skip;c:= a-b]
else [ 13 : skip;c:=b-a]
]
else if (a < 0 ^ b <0) then [ 14:skip;c:= -(b + 1)]
else [15: skip; c:=a + b ]
]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
243
Specification file
SPEC
PROPERTY
P1 : l2  ((a – b)  127 )  ((a – b)  - 128)
PROPERTY
P2 : l3  ((b – a)  127 )  ((b – a)  - 128)
PROPERTY
P3 : l4  (-(b + 1)  127 )  (-(b + 1)  - 128)
PROPERTY
P4 : l5  ((a + b)  127 )  ((a + b)  - 128)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
244
Examples
• Leader-Election algorithms
• Needham-Schroeder Security protocol
• Ricart and Agrawala's mutual exclusion algorithm
• Bus scheduler verification
http://rodin.stanford.edu/case-studies/index.html
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
245
Verification Tools – 2
(S. P. Rajan)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
246
Fujitsu’s High-Level Model Checking Tool
• A high-level symbolic safety property checker
based on Stanford Validity Checker (SVC)
decision procedures
• Has a state-transition input language that extends
SVC expression syntax
• Provides code to translate XE VHDL synthesis
tool's ADDs into HMC input
• HMC has been applied for verification of portions
of Fujitsu ATM switch specified in VHDL
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
247
HMC Basics: Pre- and Back-Image
• Representing sets and relations with their
characteristic functions:
• PreImage[Q] = l s.  s’. R(s,s') And Q(s')
• PreImage corresp. to EX Q in CTL.
• BackImage [Q] = ls. s’. R(s,s') => Q(s')
• BackImage (aka. Weakest Precondition) corresp.
to AX Q in CTL.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
248
Basics: Fixpoints and Safety Properties
• Z0 = Q
• Zi+1 = Q And BackImage [Zi]
• If [  k. Zk = Zk+1] then [Zk = nZ. (Q And
BackImage [Z])]
• This fixpoint corresp. to AG Q
• If initial states Q0 is a subset of Zk, then Q is a
safety property.
• Otherwise, a counterexample trace exists,
starting in Q0 \ Zj,
• where Zj is the first Zi s.t. Q0 is not a subset of
Zi
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
249
HMC: Data-Type and Expression Support
• Quantifier-free first order logic with linear
arithmetic and uninterpreted functions
• Built-in theories in SVC: uninterpretted functions
under equality, linear arithmetic, stores, records,
bitvectors.
• Approach equally applicable to other decision
procedures.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
250
VeriSoft from Lucent Bell Labs
• A New “Model Checking” approach.
• A New Approach to Communication Software
Analysis
• What is VeriSoft?
• How does it work?
• Industrial applications.
• Related work and discussion.
• Project status and conclusions.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
251
What is VeriSoft?
• Concurrent Reactive System Analysis
• Each component is viewed as a ``reactive''
system, i.e., a system that continuously interacts
with its environment.
• Precisely, we assume:
• finite set of processes executing aribitrary
code (e.g., C, C++, Java, Tcl, ...);
• finite set of communication objects (e.g.,
message queues, semaphores, shared
memory,...).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
252
What is VeriSoft? (contd.)
• Problem:
• Developing concurrent reactive systems is
hard! (many possible interactions); Traditional
testing is of limited help! (poor coverage);
Scenarios leading to errors are hard to
reproduce!
• Alternative: Systematic StateSpace
Exploration
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
253
How does VeriSoft work?
• VeriSoft looks simple! Why did we have to
• wait for so long (15 years) to have it?
• Existing statespace exploration tools are
restricted to the analysis of models (i.e., abstract
descriptions) of software systems.
• Each state is represented by a unique identifier.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
254
How does VeriSoft work?(contd.)
• During statespace exploration, visited states are
saved in memory (hashtable, BDD,...).
• With programming languages, states are much
more complex!
• Computing and storing a ``unique identifier'’ for
each state is unrealisitc!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
255
StateLess Search
• Idea: perform a stateless search!
• still terminate when state space is acyclic
• Equivalent to ``statespace caching'' with an
empty cache: this search technique is terribly
inefficient! [H85,JJ91]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
256
An Efficient StateLess Search
• [GHP92]: Redundant explorations due to statespace caching can be strongly reduced by using
Sleep Sets [G90], and ``partialorder methods'' in
general [G96].
• VeriSoft: original algorithm combining stateless
search, sleep sets [G90,GW93], conditional
stubborn sets [V90,GP93,G96].
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
257
An Efficient StateLess Search(contd.)
• Theorem : For finite acyclic state spaces, the
above algorithm can be used for the detection of
deadlocks and assertion violations without
incurring the risk of any incompleteness in the
verification results.
• Observation : When using this algorithm, most of
the states are visited only once during the search.
• Not necessary to store them!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
258
VeriSoft -- Summary
• VeriSoft is the first tool for systematically
exploring the state spaces of systems
• Composed of several concurrent processes
executing arbitrary (e.g., C or C++) code.
• Originality: Framework, Search, Tool [POPL'97].
• The key to make this approach tractable is to use
smart statespace exploration algorithms!
• In practice, the search is typically incomplete.
• From a given initial state, VeriSoft can always
guarantee a complete coverage of the state space
up to some depth.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
259
Industrial Applications
• Examples of Applications: (within Lucent
Technologies)
• 4ESS HeartBeat Monitor analysis (debugging,
reverseengineering).
• Wavestar 40G integration testing (testing).
• Automatic Protection Switching analysis
(interoperability protocol testing).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
260
Conclusion
• VeriSoft (tool + approach) can find bugs in
nontrivial concurrent/reactive software system.
• 1. Concurrent/reactive/realtime software is hard
to design and test.
• 2. Traditional testing techniques are not adequate
(poor coverage, lack of observability and
controllability).
• 3. Systematic testing using an approach specially
developed for detecting race conditions and
timing issues can rather easily expose previously
unknown bugs.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
261
Case Studies
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
262
Case Study 1
(S. P. Rajan)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
263
Motivation: Real Buggy Chip
• Bug identified in a real chip design ATM Switch:
156 MHz, 111000 gates.
(B. Chen, M. Yamazaki, and M. Fujita)
• Field test showed abnormal behavior after several
seconds
• Data disappeared/duplicated
• Simulation prohibitively expensive (100 million
cycles required)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
264
Motivation: State Explosion
• Formal Verification to find bugs
• Symbolic Model Checking using SMV for controlblock verification
• State-space explosion (large datapath)
• Abstraction to reduce state-space
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
265
Motivation: Abstraction Expensive
• Too much abstraction revealed no bugs 8 bit to 1 bit; Single module verification
• Trial-and-error method to come up with right
abstraction:
• 8 bits to 2 bits
• Bug revealed: Reset incomplete!
• Coming up with right abstraction: Tedious
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
266
Motivation: Design Change
•
•
•
•
Changes in design require revalidation
Revalidation expensive
TAT too long
Design cycle cost expensive
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
267
Typical ATM Switch Fabric
2 x 2 Switch
2 x 2 Switch
2 x 2 Switch
2 x 2 Switch
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
268
ATM Switch Architecture
HW_clk|SW_clk: Multiple Clocks
iHW0/1
oHW0/1
S/P
Write
Control
(WC)
Cell FIFO
RAF0
RAF1
P/S
Read
Control
(RC)
WAF
Cell Counter
(wBC)
Copy Cell
Flag ccf
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
269
ATM Switch Highlights
• 2 X 2 switch
• multiple clocks: faster external HW_clk; slower
internal SW_clk
• 1 cell-buffer shared by 2 ports
• address-FIFO for supplying cell addresses
• addresses recycled
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
270
ATM Switch: Generic Parametric description
• Modification of existing fixed parameter highlevel description in VHDL
• Parametrized the external/internal clock ratio:
• synthesized designs with specific
ratios by simple instantiation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
271
ATM Switch Generic Parametric Description
• Parametrized the number of switch input/output
ports:
• synthesized designs with specific number of
ports by simple instantiation
• Parametrization of cell-buffer size also possible
• Reusable generic model
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
272
Complexity of Design Spec
• ~ 20 Communicating Processes
• ~1500 lines of VHDL code at high-level
• ~20000 lines of VHDL at gate-level after synthesis
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
273
Behavior Partitioning
• Partitioning based on
• clock: Faster HW_clk; slower SW_clk
• functionality: Serial/Parallel (S/P); Write
Control (WC); Read Control (RC)
• throuput requirement: pipeline latency
• Modeling: VHDL process for partition
• “wait until clk = 1” for control step
• Define interface between partitions
• eg: clk conversion in S/P & P/S
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
274
Generic ATM VHDL Model
entity: atm_sw is
generic (
-- ext/int clk ratio
of input/out ports
);
port ( ... );
end atm_sw
begin
n: integer,
m: integer -- number
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
275
SP conversion module 1: VHDL
iHW_sp1: process
begin
for i in 1 to n loop
iHW_bword(1)(i) <= iHW_cell_word;
if i = 1 then ... elsif i = n then
iHW_cycle_counter <=
iHW_cycle_counter (n downto 2) & '1'; ...
endif;
wait until (HW_clk'event and HW_clk = '1');
end loop;
end process iHW_sp1;
• Stores the incoming word and updates cycle
counter
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
276
SP Conversion Module 2: VHDL
iHW_sp2: process
begin
for i in 2 to n loop ...
iHW_bpc(i) <= iHW_bpc(i-1);
for j in 1 to n loop
iHW_bword(i)(j) <= iHW_bword(i-1)(j);
end loop;
wait until (HW_clk'event and HW_clk='1');
end loop;
end process iHW_sp2;
• Shifts contents of registers by one place
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
277
SP conversion module: VHDL model
to_FIFO: process begin
... for j in 1 to n loop
iHW_word(j) <= iHW_bword(index-1)(j);
header_parity_check := bit_or(iHW_bpc(j));
end loop;
wait until (sw_clk'event and sw_clk='1');
end process;
• The proper word is fetched to the FIFO from the
shift-register
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
278
Synthesis: Generic Clock Ratio
Clk Ratio
Ports
Nets Cells
3
4
118
59362 52243
93580
223
118
62578 55259
97506
223
5
118
118
66245 58688
102208
223
69203 61376
107484
223
6
Area (bc) delay (ns)
Area and delay of synthesized ATM switches different clock ratios
 Fujitsu CS35R technology
 Number of ATM input ports = 2 and ouput ports = 2

ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
279
Synthesis: Generic Clock Ratio
Clk Ratio
Ports
Nets Cells
3
4
118
59362 52243
93580
223
118
62578 55259
97506
223
5
118
118
66245 58688
102208
223
69203 61376
107484
223
6
Area (bc) delay (ns)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
280
Synthesis: Generic number of in/out ports




Area and Delay of Synthesized ATM Switches
Varying number of input/output ports
Fujitsu CS35 technology
Clock ratio = 3
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
281
Formal Verification



Overall correctness property - Input cells
switched to proper output ports,- The order of
input cells is maintained at the output.
ATM is a complex design:-- Compositional
verification technique: verify ATM modules
separately and compose
Verification of the generic parametric model
automatically implies the verification of a family
of ATM designs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
282
Formal Verification : Bugs found





Address pointers to WAF not initialized to 0
Analysis by model checking in PVS
Mistake due to hidden assumptions in synthesis
Counter-example generated
Combined with other verified modules
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
283
SP conversion: PVS Spec
sp_conversion_theory[n: posnat]: THEORY BEGIN
IMPORTING signal,signal[n],
[email protected]_extractors, ...
register_array: TYPE = ARRAY ...
iHW0_bword: [nat -> register_array]
iHW0_cell_word: signal[16]
forloop0(t,i,n): bool = % i indexes rows
….
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
284
SP conversion: PVS Spec
…...
iHW0_bword(t)(0,i) = iHW0_cell_word(t) AND
IF n > 1 THEN
(i = n-1 IMPLIES iHW0_cycle_counter(t+1) =
iHW0_cycle_counter(t)^(n-1,1)
o b1)
ELSE iHW0_cycle_counter(t+1) = b1
ENDIF
END sp_conversion_theory
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
285
SP Conversion: PVS Spec
loop0(t,i,m): RECURSIVE bool =
IF i = n THEN TRUE
ELSE
iHW0_cycle_counter(t) = bvec0 AND
(forloop0(t,i,n) AND loop0(t+1,i+1,n))
ENDIF
MEASURE n-i
sp(0,n) = ...
to_fifo(n,n) = ...
• VHDL to PVS translation non-trivial
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
286
SP Conversion:Formal Verification
• theorem2: THEOREM % When clk rising edges
are synchronized
FORALL (n:posnat):FORALL (i:nat|i<n):
sp(0,n) AND to_fifo(n,n) IMPLIES
iHW0_word(n)(i) = iHW0_cell_word(i)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
287
SP Conversion:Formal Verification
• Finaltheorem: THEOREM % When clk rising
edges need not be synchronized
FORALL (n:posnat): FORALL (i:nat|i<n):
sp(0,n) AND to_fifo(n,n) IMPLIES
EXISTS (t:time | n <= t AND t <= 2 * n)
iHW0_word(t)(i) = iHW0_cell_word(i)
• Proof by induction and rewriting:
14.8 Secs on Sparc-20, 64 Meg RAM
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
288
Address Recycle Verification
Theorem :
FORALL (t: time),
(ptr: {ptr: address_type |
RAF0_tptr(t) <= ptr AND
ptr <= RAF0_hptr(t)}):
whileloop(t) AND more(t) AND
RAF0_hptr_tptr_update(t) AND
RAF1_hptr_tptr_update(t)
IMPLIES
iHW0_write_addr(t) /=
MEM(t)(ptr)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
289
Address Recycle Verification
• Symbolic Model-Check proof strategy in PVS
used
• Theorem not proved
• Counter-example evident from the proof script
• 19 Seconds cpu time on Sparc-20 / 32 Meg
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
290
Address Recycling: Bug Found
• WAF_hptr and WAF_tpr not initialized to 0
• Bug found easily by model checking original
VHDL description in an integrated theorem
proving and model checking framework
• Another error suspected in cell buffer update
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
291
Conclusions
• Introduced formal verification early in the
design cycle to remove bugs
• Serious bugs found in initialization related
to address recycling
• High-level parametric validation reduces
cost of formal verification: small-scale
gate-level validation suffices for sign-off
• Drastic reduction in cost and time-tomarket
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
292
Case Study 2
[Formal meets semi-formal]
(T. Nakata)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
293
Outline
• Target design: media instruction unit (MU) of a
VLIW multimedia processor core
• Verification strategy: divide-and-conquer
• Right tool in the right place
• Specification language
• Formal verifier
• Semi-formal verifier
• Logic simulator
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
294
Divide-and-Conquer Verification
• Isolate a module using formal I/F specification
• Verify a module by integrated verification tools
MPU
DSP
Module
I/F
I/F specification
Pattern/property gen.
ROM
DRAM
I/O
GDC
Integrated
Module verification
engine
Checker
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
295
Verification Tools
• Interface specification toolkit (in-house)
• Language based on regular expression
• Pattern/property/checker generator
• Formal verifier (in-house)
• Model checker
• Automatic/semi-automatic design abstraction
tool
• Semi-formal verifier
• 0-In Search & Checkerware
• Logic simulator
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
296
Verification Flow
Design
under
verification
Black-box
spec.
I/F spec.
White-box
spec.
Verification
scenario
I/F specification language
Design
model
Input
constraints
Properties
Scenarios
Integrated verification engine
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
297
Verification of MU
• MU
• Pipeline for media instruction
• RTL model: 14,000 lines in Verilog
• 2,000 registers in total
• Basic strategy
• As formal as possible*
• Semi-formal verification for the whole unit
• Formal verification for an important unit:
instruction decoder
* Simulation completed before this attempt
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
298
Verification of MU (1st)
41 constraints
4 properties
I/F spec.
HDL
Test
Testpatterns
pattern
augmented
by
0-In Search
MU
Insufficient
constraints
Result: Many design errors detected, but all from input
patterns that do not satisfy input constraints
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
299
Verification of MU (2nd)
Pseudo models
(I/F spec. lang. and HDL)
Test
Testpatterns
pattern
augmented
by
0-In Search
I/F spec.
HDL
MU
Result: A known error in interlock logic and
an unknown error in decoder detected
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
300
Detected Error
• Indicator of no hazards “e-wait” may be asserted
under a certain hazard condition
• Length of augmented* patterns: 7 cycles
* By 0-In Search
clock
m0_valid
m1_valid
i0_valid
m0_rd
xxx
0xf
m0_rs1
xxx
0x0
m1_rd
0x0
i0_rd
xxx
0x0
e_wait
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
301
Summary of MU Verification Flow
M-Unit
(HDL)
Properties Constraints
(I/F spec)
(I/F spec)
Pseudo
(HDL)
Test
vectors
Converter
Properties/constraints
(HDL+0-In Check)
0-In compile
Design
database
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
0-In Search
302
Verification of Instruction Decoder
• Instruction decoder
• Complete verification required
Model checker
• 200 registers
• Property and constraints
• Property: detection of unsupported
instructions
• Constraints: valid instructions
• Described in I/F spec. language (460 lines)
• Results
• Two errors detected
• Correctness proven after revision
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
303
Decoder Verification Flow
M-Unit
decoder
(HDL)
Properties Constraints
(I/F spec)
(I/F spec)
Model checker
Note:
No abstraction/
reduction required
in this example
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
304
Statistics
• Verification team: 3 people
• Term: 4 months
• Build specification: 2 months
• Apply semi-formal verification: 3 months
• Apply model checker: 2 months
• Sources for verification
Lines
MU (HDL)
14,320
Pseudo (HDL)
1,518
Constraints (I/F spec. lang.)
1,818
Properties (I/F spec. lang.)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
118
305
Conclusions
• Interface specification essential
• For module isolation
• For a single source for verification tools
• Formal/semi-formal verification mandatory
• Serious bugs may leak from simulation
• Earlier collaboration among designers and
verification team will produce better results
• For extracting good constraints/properties
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
306
Commercial Tools
(Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
307
Commercial Tools
• Several tools available as commercial offerings.
• Different approaches taken. Most are based on
• Simulation
• Formal Verification
• Semi-Formal Verification
• Most support IP-verification re-use (intuitive, but
can be formally related to compositional
techniques).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
308
Assume & Guarantee - Basic Idea
Global Property defined on o2
o1
i1
P
o2
Q
i2
Decompose
Guarantee
o1
Assumption
o1
P
Q
i2
Assumption
i2
Guarantee
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
309
Smarter Simulation
[Gupta, Malik & Ashar, DAC 97]
Design Spec
(Behav Level
Description)
Behavioral
simulator
=?
Function Test Set
Test
Set
Generator
RTL
simulator
Validation
Design Implmt
(RTL Level
Description)
Test Model
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
310
FormalCheck
• Model Checking based on COSPAN from Bell Labs
• Integrated debug environment with back references
to HDL source codes
• Property specification (Queries) based on template
approach with user guidance
• Two reduction technologies for large designs
• Supports hierarchical + IP + Re-use verification
• Assumptions stated as constraints on environment
using same format as behaviors or properties
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
311
Block
Constraints
Target
Blocks
Block
Properties
=
System
Properties
Interface
FormalCheck
System
Blocks
=
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
System
Constraints
312
FormalCheck Architecture
Chip, Blocks, IP Models
In Verilog or VHDL
Gates
Template-Based
Query Inputs
RTL
Autorestrict
Probabilistic
Large Model
Query
Capture
Formal Model
Query-Specific
Reduction
Query
Template
Library
Early Model
Results &
Error Traces
Results Display
Inputs
Outputs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
313
Specman Elite - Verisity
• Simulation & Spec-Based Verification (executable)
• White Box – Drive & Test Internal Signals
• On the Fly Test Generation
• Test Checking is automatic : On the Fly
• Supports metrics to track progress of verification
effort & measure coverage of functional test plan
• To verify temporal behavior & protocols - Constantly monitors design by sensing for triggers
signaling beginning of a sequence and follow it to
verify conformance to temporal/protocol rules.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
314
Specman Elite - Verisity
• New & Powerful temporal constructs to easily
specify complex checkers – Less Time Consuming
• Supports data checks &coverage based feedback
mechanism.
• Allows executable checkers around boundary of IP.
• Allows checks for arbitrarily complex, mode independent, multi-cycle scenarios that IP vendor
specifies.
• Allows boundary checks to ensure correctness of
integration process.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
315
Specman Elite - Verisity
• Allows Internal Checks - Provides a handle to the IP
integrator to analyze failures in IP after integration.
SPEC
CONSTRAINTS
Protocols
I/O Relationships
Context Dependencies
Input Definition
Next Cycle’s Stimulus
TEST
CONSTRAINTS
Target Areas
Weights/Probabilities
Corner Case Tests
Structured Sequences
CONSTRAINT
SOLVER
HDL SIMULATION
Current Cycle’s HDL
Signal & Register Values
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
316
Specman Elite - Verisity
e-language
e-language
Bus Functional Model
Monitor
&
Protocol Checker
e-language
Verilog
BLOCK
Monitor
&
Protocol Checker
e-language
e-language
Coverage
Collector
e-language
Verilog
BLOCK
Monitor
&
Protocol Checker
Coverage
Collector
e-language
Coverage
Collector
Bus Functional Model
e-language
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
317
ZeroIn-Search
• Semiformal verification based on formal techniques & simulation -- Sweeps formal techniques
through a larger state space by extensively exploring around each state in a “seed’’ trace. “Seed’’
comes from functional simulation test.
• Two step process
• Embedded Checkers - written in HDL (No seperate property or assertion language needed)
• Protocol Checkers - provides verification environment (reports errors by models stimulating IP)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
318
ZeroIn-Search
0_In Check Tool
• Instruments the Core/IP/VC with embedded checkers automatically based upon comments in RTL
code (increases observability & detects bugs at
source).
• 0_In provides CheckerWare Library of checkers
for internal design structures & interfaces + preverified protocol monitors for standard buses PCI, PCI-X, Utopia. (Formal techniques try to find
new ways to fire embedded checkers.)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
319
ZeroIn-Search
• More than 50 embedded checkers
• Checkers for datapath elements, FSMs & other
control flow elements, buses and interfaces.
• Approach finds bugs, not just new coverage.
• If a checker fires in simulation, then a bug is
present. If amplification finds a new way to fire a
checker, it detects a bug.
• Stress tests interface to design interactions.
• Checkers & monitors track coverage statistics &
corner cases.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
320
0_inSearch Verification Flow
Verilog RTL
with
Directives
Checker
Library
Verilog RTL
with
Checkers
Verilog Tests
&
Test Benches
Checker
Generator
Verilog
Simulator
Simulation Files
with Checkers
Captured
Seed
Values
Semiformal
Amplification
Tool
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Firing
Messages
in
Verilog o/p
Information
on
New Firings
321
BlackTie - Verplex
• Based on Formal Verification
• Allows full system level integration verification
(Multimillion gate capacity tool)
• Free open source assertion monitor library (Verilog)
• Simulation (through any Verilog simulator) & Formal Verification (BlackTie) can operate seamlessly
• With BlackTie no test vectors, exhaustive coverage,
automatic diagnosis.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
322
BlackTie - Verplex
• Automates checking of global & common place
errors. Automatic generation of checkers for,
• Contention Problems.
• Asynchronous Clock Domain Crossings
• Dead-End States
• Conflicting values loaded to Multi-Port Registers
• Simultaneous Set & Reset conditions
• Mutual Exclusivity Checks
• Tri-state stuck in a particular state.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
323
Issues & Challenges
&
Future Research Topics
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
324
High Level Specification and Modeling
(T.Nakata)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
325
Why Specification?
• Specification errors/misunderstandings take 50% of
SoC design man-power.
• Verification tools can’t handle such errors enough.
Verif.
tools
Design man-power for SoCs
Wrong Misunderstanding Simple
Verification 70%
Spec.
Of Spec.
mistakes
Others
Spec.
design
support
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
326
Issues in Specification and Verification
Idea and/or
requirement
Specification
Design data
Validation
Wrong
Does
specification
specification
Misunderstanding
Formalization
Isof
specification
defined
specification
match requirement?
clearly?
SoC
We need:
• Methodology for specification analysis
• Standard language with formal semantics
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
327
UML
UML is:
• Standard in object-oriented software design
• Devised and designed under the object-oriented
analysis theory
• A set of diagrams that represent components of a
system and relationships among them
• Modeling a system from multiple angles with
use-case/class/object/state/sequence/
activity/collaboration/component/deployment
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
328
Object-Oriented Analysis
• For system architect to understand “WHAT” to
design not “HOW”
Requirement
Interview with
customers
Use-case
Scenario
Analysis
Structure
Docs on existing
systems
Behavior
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
329
UML and Object-Oriented Analysis
Use-case
diagram
Requirement
Interview with
customers
Class
Docs
on diagram
existing
systems
Sequence
diagram
Use-case
Scenario
Analysis
Structure
Behaviour
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Use-case
Scenario
Structure
State diagram
Behavior
330
Case Study
• Objectives --- getting answers to:
• Is object-oriented analysis by UML effective?
• Is there a way from UML to implementation?
• Example: error correction with two code types
• Bit-wise error correction: Code A
• Word-wise error correction: Code B
• Claims before analysis
• Two code types are similar
• HW implementation cannot be shared though
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
331
Error Correction
Message
Sent word
Received word
Channel
Noise
Encoder
Systematic
code
Decoder
Errors
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
332
Analysis and Design Flow
•
•
•
•
Step 1
Step 2
Step 3
Step 4
Extract concepts
Build structure
Enumerate scenarios
Identify hardware modules
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
333
Analysis and Design Flow
• Step 1
Extract functions
• Inputs: requirement from users
• Flow:
• Find actors that cause stimulus
• Define use-cases from viewpoints of actors
• Relate use-cases and actors
• Output: use-case diagram
• Step 2
Build structure
• Step 3
Enumerate scenarios
• Step 4
Identify hardware modules
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
334
Use-Case Diagram of Error Correction
Encode
Sender
<<extend>>
Encode A
<<extend>>
Send
Encode B
Receiver
Receive
Decode A
<<extend>>
Decode
Channel
Decode B
<<extend>>
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
335
Analysis and Design Flow
•
•
•
•
Step 1 Extract functions
Step 2 Build structure
• Input: use-case diagram
• Flow:
• Refine use-cases
• Extracting concepts --- candidates of
classes
• Define and relate classes
• Output: class diagram
Step 3 Enumerate scenarios
Step 4 Identify hardware modules
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
336
Use-case Refinement
• Example: decoding code A
• Refine a use-case with natural language
• Extract important nouns
1. Calculate syndrome from received word and
received code polynomial
2. Judge as no errors detected if syndrome is 0
3. Calculate coefficients of error location polynomial
4. Calculate roots as many as degrees of error
location polynomial
5. Correct word by flipping bits designated by roots
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
337
Concept Extraction
• Classifying classes and properties
Received word
Decoded word
Message length
Code word
Error location polynomial
Syndrome polynomial Code Degree
Root
Syndrome Generator polynomial Coefficient
Properties
Generator
matrix Parity Error Block code
rather than
Galoisclasses
field Element LFSR Code length
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
338
Relationships among Classes
Vector
{Word-wise}
Code B
Code word
{Bit-wise}
Code word Code A
Code A is a special
case of Code B.
Message
word
Systematic
code
Data structure is deduced
from relationships.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
339
Class Diagram
Decode
Coefficient *
Polynomial
Root *
Received word
Input
Galois field
Syndrome
Received
code
polynomial
Error location
polynomial
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
340
Analysis and Design Flow
•
•
•
•
Step 1 Extract functions
Step 2 Build structure
Step 3 Enumerate scenarios
• Inputs: use-case sentences, class diagram
• Flow:
• Describe sequence diagrams
corresponding to refined use-cases
• Define methods and properties from
sequence diagrams
• Outputs: sequence diagram, class diagram
with methods
Step 4 Identify hardware modules
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
341
Sequence Diagram for Decode
r1:received word
Receive
Input
:received polynomial
:error location polynomial
Assign(r1)
Generate()
s1: syndrome
IsZero()
Calc_coef(s[])
Calc_loc(coef)
Correct (location, value)
Calc_error(root)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
342
Complete Class Diagram
Decode
Input for A
Input
+Receive()
Input for B
+Receive()
Galois field
Coefficient *
+Receive()
Polynomial
Root *
+Assign(val)
Received word
Received
code
polynomial
-Code length
-Corrections
+Correct(loc, val)
Error location polynomial
+Order
+sum()
+multiply()
+divide()
+exp(power)
+IsZero()
Syndrome
+Calc_coef(syndrome)
-Calc_loc(coef)
*
-Index
-Value
Error loc. poly. for A
-Calc_error(root)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Error loc. poly. for B
-Calc_error(root)
343
Analysis and Design Flow
•
•
•
•
Step 1 Extract functions
Step 2 Build structure
Step 3 Enumerate scenarios
Step 4 Identify hardware modules
• Input: class diagram
• Flow
•
•
•
•
Correspond methods to hardware modules
Define messages from relationships among
modules
Define interfaces from messages
Outputs: class diagram, block diagram (in
hardware design context)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
344
Methods to Hardware Modules
• Disband classes
• Map each methods to modules
• Re-bundle modules if possible
Error loc. poly.
Coefficient calculator
+Calc_coef(syndrome)
-Calc_loc(coef)
Error loc. calculator
Galois field
+Order
+sum()
...
+IsZero()
Galois adder
Galois 0 checker
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
345
Initial Block Diagram
Decode
Assignment module
for received poly.
Receiver
Receiver
for Code A
Receiver
for Code B
Correction
module
Error info
-Location
-Value
Galois
adder
Galois
adder
Galois
Galoisadder
adder
Received
word
-Code
length
-Corrections
Error
calculator
Error calculator
for Code A
Coefficient
calculator
Syndrome
-Index
-Value
Root
Error calculator
for Code B
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Coefficient
Location
calculator
346
From Messages to Interface
Assignment module for
received polynomial
Received word
- Code length
- Corrections
+clock: input
+received
word: input
+syndrome:
+reset:
inputoutput
+enable: input
+received word: input
+syndrome: output
Syndrome
- Index
- Value
HW
design
C++ / HDL
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
347
Block Diagram of Decoder
Correction
Code A
receiver
Code B
receiver
enable
Assignment
Coefficient
calculation
Error location
calculation for
Code A
Location
calculation
Error location
calculation for
Code B
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
348
Conclusions
• Is object-oriented analysis by UML effective?
• For common understandings
• For validation
• For analyses of specification changes
• Is there a way from UML to HW implementation?
• For design optimization
• For verification
Already proven in software designs
Proven this time (partially)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
349
Verification Issues
• For simulation-based verification
• Develop a systematic way to co-verification
models
• Generate corner case scenarios from existing
use-cases and scenarios
• Prioritize verification scenarios for efficient
verification
• For formal verification
• Build up mathematical model
• Define important properties for system level
designs
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
350
Issues & Challenges
(S. Chakraborty)
(S. P. Rajan)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
351
Where do we stand?
Model
checking
C
o
v
e
r
a
g
e
Based on Dill and Tesiran’99
FSM-based
generation
Symbolic
simulation
Manual test
w/ coverage
Scale (gates)
1 FSM
50K
250K
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
Random
simulation
2M
352
Research Issues
• Fundamental complexity hurdles in scaling
formal verification methods with design sizes
• Approximate verification methods, semi-formal
methods will be important tools in future
• Approximate methods:
• Model approximations should be driven by
property being checked
• Available computing resources can be used to
guide nature of approximation
• Verification should give some coverage metric
on termination
• “Out of memory” after 48 hours not of any
use!
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
353
Research Issues
• Abstraction of system behavior crucial for
analyzing large designs
• Must employ right degree of abstraction
automatically or semi-automatically
• More research needed
• Different degrees of abstraction at different levels
of hierarchical designs
• Can this be done automatically?
• Approximate and semi-formal methods
•
•
•
•
“Test of the pudding” is on large real examples
Most published examples are small
A lot of ideas -- no clear winners so far
An active area of research
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
354
Research Issues
• With IP based designs, supplier of IP must
provide hints on how to verify IP core
• RTL with assertion checks
• Hints on exercising combinations of inputs
• IP verification test suite with coverage metric
• Formal verification of IP-based SOCs will be
challenging
• Success constrained by verifiability,
controllability and observability of IP-core
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
355
Research Issues
• Runtime/memory bottlenecks of existing formal
verification methodologies must be addressed to
scale them to larger designs
• Active field of ongoing research
• Suitable combination of techniques (random
simulation, model checking, theorem-proving …)
to be selected for each verification task
• Understanding which techniques work well
under what circumstances
• Can this be automated?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
356
Research Issues
• Sequential verification still very limited to under
500 latches
• Concurrent system verification very difficult
without abstraction
• Real-time systems verification not yet practical
• Formal verification at RTL and above not in the
main stream
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
357
Future Research Directions
• How to come up with a verification framework
which involves different verification methods
cooperating in a single environment?
• What should be the data structure?
• Design for Verifiability -- is it viable and practical?
• How do we integrate formal verification with
conventional simulation and testing?
• How do we integrate verification tools with
synthesis tools?
• How do we generate counter-examples for
sequential, concurrent, and real-time systems
verifiers?
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
358
Summary & Conclusions
(S. Chakraborty)
(Subir K. Roy)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
359
Summary
• Formal verification of SOCs has brought hardcore engineers and theoreticians on a common
platform
• Model checking most successful so far
• Equivalence checking successful in restricted
cases, catching up fast
• The gap between VLSI advancements and
advancements in FV techinques can be filled to
some extent by semi-formal methods
• Hard to measure “success” for such
techniques?
• I might not have detected one out of 100000
bugs, but this might be the killer bug
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
360
Summary
• SOC verification will be an important area in
future
• Simulation and emulation still predominant
techniques used in industry and justifiably so
• However, formal methods ARE NEEDED when
applicable and when one can’t afford to miss a
bug
• Success stories: Protocols, FSMs, specific
processors, floating point arithmetic etc.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
361
Conclusions
• Functional verification of SoCs critically dependent
on verification re-use of Cores/IPs/VCs.
• Semi-Formal approach based on application of different combinations of verification technologies
seem important. No single approach will suffice.
• Formal & executable specifications have to be used
at all levels of design hierarchy.
• High degree of automation will be needed to overcome complexities inherent in SoCs.
• Exciting Area for Research.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
362
Bibliography
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
363
Papers
•
•
•
•
•
•
•
•
•
•
•
S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS:
Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96.
C.-J. H. Seger, "An Introduction to Formal Verification", Technical Report 92-13, UBC,
Department of Computer Science, Vancouver, B.C., Canada, June 1992.
Aarti Gupta, "Formal Hardware Verification Methods: A Survey", Formal Methods in
System Design, Vol. 1, pp. 151-238, 1992.
E. Clarke and J. Wing, Formal Methods: State of the Art and Future Directions, CMU
Computer Science Technical Report CMU-CS-96-178, August 1996.
A. U. Shankar, "An Introduction to Assertional Reasoning for Concurrent Systems",
ACM Computing Surveys, Sept. 1993, Vol 25, No. 3, pp. 225-262.
D. Dill, "What's Between Simulation and Formal Verification?", slides from a
presentation by Prof. Dill, Stanford University at DAC'98.
D. Dill, "Alternative Approaches to Formal Verification (Symbolic Simulation)", slides
from a presentation at CAV 1999.
M.C. McFarland, "Formal Verification of Sequential Hardware: A Tutorial", IEEE Trans
Comput.-Aided Des. Integr. Circuits Syst, Vol 12, No 5, pp. 633-54, May 1993.
S. Owre and S. Rajan and J.M. Rushby and N. Shankar and M.K. Srivas, “PVS:
Combining Specification, Proof Checking, and Model Checking”, 411-414, CAV96.
D. L. Dill, “The Mur Verification System”, 390-393, CAV96.
T. L. Anderson, “Accelerating Bug Discovery with White-Box Verification”, Proc. Of
DAC 2000.
VLSI/ASPDAC : Tutorial on
Functional Verification of SoCs
364
Papers
•
•
•
•
•
•
•
•
•
C. Kern and M. Greenstreet, "Formal Verification in Hardware Design: A Survey", ACM
Transactions on Design Automation of E. Systems, Vol. 4, April 1999, pp. 123-193.
H. Iwashita and T. Nakata, `` Forward Model Checking Techniques Oriented to Buggy
Designs'', Proceedings of ICCAD, pp. 400-404, 1997.
K. Takayama, T. Satoh, T. Nakata, and F. Hirose, ``An approach to Verify a Large Scale
System-on-a-chip Using Symbolic Model Checking'', Proceedings of ICCD, 1998.
S. K. Roy, H. Iwashita and T. Nakata, ``Data Flow Analysis for Resource Contention
and Register Leakage Properties'', Proceedings of the 13th International Conference
on VLSI Design, January 2000.
S. Berezin, S. Campos and E. M. Clarke, ``Compositional Reasoning in Model
Checking'', Technical Report - CMU-CS-98-106, School of Computer Science,
Carnegie Mellon University, February, 1998.
T. Schlipf, T. Buechner, R. Fritz, M. Helms and J. Koehl,``Formal Verification Made
Easy'', IBM Journal of Research and Development, Vol. 41, No. 4/5, pp. 567-576,
July/September 1997.
D. D. Gajski, ``IP-Based Design Methodology'', Proc. of the 36th Design Automation
Conference, pp. 43, New Orleans, June 1999.
M. Kaufmann, A. Martin, and C. Pixley, "Design Constraints in Symbolic Model
Checking", Proc. CAV-98, pp. 477-487, 1998.
K. L. McMillan, "Fitting formal methods into the design cycle", Proceedings of the
31st Design Automation Conference, pp. 314-19, 1994.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
365
Papers
•
•
•
•
•
•
•
•
•
A. Gupta, S. Malik and P. Ashar, ”Toward Formalizing a Validation Methodology Using
Simulation Coverage”, Proceedings of DAC, 1997.
S. Devadas, A. Ghosh and K. Keutzer, " An Observability-Based Code Coverage
Metric for Functional Simulation”, Proceedings of ICCAD, 1996.
H. Chockler, O. Kupferman, and M. Y. Vardi, "Coverage Metrics for Temporal Logic
Model Checking", TACAS 2001, LNCS 2031, Springer-Verlag, pp. 528-542.
Y. Hoskote, T. Kam, P. Ho and X. Zhao, ``Coverage Estimation for Symbolic Model
Checking'', Proc. of the 36th Design Automation Conference, New Orleans, June 1999.
S. Katz, O. Grumberg and D. Geist, ``Have I written enough properties? - A method of
comparison between specification and implementation'', Technical Report, IBM Haifa
Research Laboratory, Haifa, Israel, 1999.
S. Campos, E. Clarke, W. Marrero and M. Minea, ``Verifying the Performance of the PCI
Local Bus using Symbolic Techniques'', Technical Report - CMU-CS-96-147, School of
Computer Science, Carnegie Mellon University, June, 1996.
S. Chakraborty, D. L. Dill and K. Y. Yun, "Min-max Timing Analysis and an Application
to Asynchronous Circuits", Proc. of the IEEE, Vol. 87, No. 2, pp. 332-346, Feb 1999.
R. Hersemeule, B. Clement, E. Lantreibecq, P. Coulomb, B. Ramanadin, and F.
Pogodalla, ”Fast Prototyping : A System Design Flow applied to a complex SystemOn-Chip Multiprocessor Design", DAC 1999.
A. J. Hu, “Formal Hardware Verification with BDDs : An Introduction”, ACM
Transactions on Programming Languages and Systems, 1997.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
366
Papers
•
•
•
•
•
•
•
•
•
K. L. McMillan, "A compositional rule for hardware design refinement", Computer
Aided Verification (CAV97), O. Grumberg (Ed.), Haifa, Israel, pp. 24-35, 1997.
T.A.Henzinger, S. Qadeer, and S.K.Rajamani, "You assume, We guarantee :
Methodology and Case Studies" CAV98: Computer Aided Verification, Lecture Notes
in Computer Science, Springer-Verlag, pp. 440-451, 1998.
M. C. Browne, E. M. Clarke and D. L. Dill and B. Mishra, ``Automatic Verification of
Sequential Circuits using Temporal Logic'', IEEE Transactions on Computers, Vol. C35, No. 12, pp 1035-1043, Dec. 1986.
E. M. Clarke, E. A. Emerson and A. P. Sistla, ``Automatic Verification of Finite-State
Concurrent Systems Using Temporal Logic Specifications'', ACM Trans. on
Programming Language and Systems, Vol.8, No.2, pp 244-263, April 1986.
G. Mosensoson, “Practical Approaches to SoC Verification”, DATE 2000.
J. L. Nielsen, H. R. Andersen, G. Behrmann, H. Hulgaard, K. Kristoffersen and K. G.
Larsen, “Verification of Large State/Event Systems using Compositionality and
Dependency Analysis”, Proceedings of TACAS 1998, LNCS 1384, April 1998.
S. Bose and A. Fisher, “Verifying Pipelined hardware using symbolic logic
simulation”, ICCD 1989.
D. Geist, G. Biran, T. Arons, M. Slavkin, Y. Nustov, M. Farkas, and K. Holtz, “A
Methodology for the verification of a System on Chip”, Proc. Of DAC 1999, pp. 574579.
A. Evans, A. Silburt, G. Vrckovnik, T. Brown, M. Dufresne, G. Hall, T. Ho and Y. Liu,
“Functional Verification of Large ASICs”, Proc. Of DAC, 1998.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
367
Papers
•
•
•
•
•
•
•
•
S. Taylor, M. Quinn, D. Brown, N. Dohm, S. Hildebrandt, J. Higgins and C. Ramey,
“Functional Verification of a Multiple-issue, Out-of-Order, Superscalar Alpha
Processor – the DEC Alpha 21264 Microprocessor”, Proc. Of DAC, 1998.
S. Ramesh and P. Bhaduri, “Validation of Pipelined Processor Designs using Esterel
Tools: A Case Study”, Proc. of CAV '99, LNCS Vol. 1633, 1999.
J. R. Burch, E. M. Clarke, D. Long, K. L. McMillan, D. L. Dill, “Symbolic Model
Checking for Sequential Circuit Verification”, IEEE Trans. Computer Aided Design, 13,
1994, 401-424.
E. M. Clarke, R. P. Kurshan, “Computer Aided Verification”, IEEE Spectrum, June
1996, 61-67.
D. Cyrluk, S. Rajan, N. Shankar and M. K. Srivas, “Effective Theorem Proving for
Hardware Verification”, pp. 287-305, TPCD94.
S. J. Garland and J. V. Guttag, “An Overview of LP: the Larch Prover”, Proceedings of
the Third International Conference on Rewriting Techniques and Applications, 1989,
Springer-Verlag.
J. Staunstrup and M. Greenstreet, “Synchronized Transitions”, Formal Methods for
VLSI Design, 1990, IFIP, North-Holland.
R. Vemuri, “How to Prove the Completeness of a Set of Register Level Design
Transformations”, Proceedings of the 27th ACM/IEEE Design Automation Conference,
1990, 207—212.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
368
Papers
•
•
•
•
•
•
•
Jeffrey J. Joyce and Carl-Johan H. Seger, “Linking Bdd Based Symbolic Evaluation to
Interactive Theorem Proving”, Proceedings of the 30th Design Automation
Conference, 1993.
S. P. Rajan, N. Shankar and M. Srivas, “An Integration of Model-Checking with
Automated Proof Checking”, 7th Conference on Computer-Aided Verification, July,
1995.
R. E. Bryant, “Graph Based Algorithms for Boolean Function Manipulation”, IEEE
Transactions on Computers, Vol. C-35-8, pp. 677- 691, August 1986
R. E. Bryant, “On the Complexity of VLSI Implementations and Graph
Representations of Boolean Functions with Application to Integer Multiplication”,
IEEE Transactions on Computers, Vol. 40, No. 2, pp, 205-213, February 1991
B. Bollig and I. Wegener, “Improving the variable ordering for OBDDs is NPcomplete”, IEEE Transactions on Computers, Vol. 45, No. 9, pp. 993-1002, September
1996
M. Fujita, H. Fujitsawa and Y. Matsunaga, “Variable Ordering Algorithms for Ordered
Binary Decision Diagrams and their Evaluation”, IEEE Transactions on ComputerAided Design of Integrated Circuits and Systems, Vol. 12, No. 1, pp. 6- 12, January
1993
R. Rudell, “Dynamic Variable Ordering for Ordered Binary Decision Diagrams”,
Proceedings of ICCAD 1993, pp. 42- 45
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
369
Papers
•
•
•
•
•
•
•
•
•
J. Jain, W. Adams and M .Fujita, “Sampling Schemes for Computing OBDD Variable
Orderings”, Proceedings of ICCAD 1998, pp. 331-338
J. Jain, R. Mukherjee and M. Fujita, “Advanced Verification Technique Based on
Learning”, Proceedings of DAC 1995, pp. 420-426
Y. Matsunaga, “An Efficient Equivalence Checker for Combinational Circuits”,
Proceedings of DAC 1996, pp. 629-634
A. Kuehlmann and F. Krohm, “Equivalence Checking using Cuts and Heaps”,
Proceedings of DAC 1997, pp. 263-268
C. H. Yang and D. L. Dill, “Validation with Guided Search of the State Space”,
Proceedings of DAC 1998
R. E. Bryant, “Symbolic Simulation -- Techniques and Applications”, Proceedings of
DAC 1990
A. Jain, “Formal Hardware Verification by Symbolic Trajectory Evaluation”, Ph.D.
Thesis, Dept. of Electrical and Computer Engineering, Carnegie Mellon University,
August 1997
C.-J.H. Seger and R.E. Bryant, “Formal Verification by Symbolic Evaluation of
Partially Ordered Trajectories”, Formal Methods in System Design, Vol. 6, No. 2, pp.
147-190, 1995
R. E. Bryant, D. L. Beatty and C.-J.H. Seger, “Formal Hardware Verification by
Symbolic Trajectory Evaluation”, Proceedings of DAC 1991
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
370
Papers
•
•
•
•
•
•
•
•
•
D. Greve, “Symbolic Simulation of the JEM1 Microprocessor”, Proceedings of FMCAD
1998, pp. 321-333
D.L. Dill and S. Tesiran, “Simulation meets Formal Verification”, Embedded Tutorial at
ICCAD 1999
R.B. Jones, M.D. Aagard and C.-J.H. Seger, “Formal Verification using Parametric
Representations of Boolean Constraints”, Proceedings of DAC 1999, pp. 402-407
R.B. Jones, “Applications of Symbolic Simulation to the Formal Verification of
Microprocessors”, Ph.D. Thesis, Computer Systems Laboratory, Stanford University,
August 1999
J.U. Skakkebaek, R.B. Jones and D.L. Dill, “Formal Verification of Out-of-Order
Execution using Incremental Flushing”, Proceedings of CAV 1998, pp. 98-109
R.B. Jones, C.-J.H. Seger and D.L. Dill, “Self Consistency Checking”, Proceedings of
FMCAD 1996, pp. 159-171
M.D. Aagard, R.B. Jones and C.-J.H. Seger, “Combining Theorem Proving and
Trajectory Evaluation in an Industrial Environment”, Proceedings of DAC 1998, pp.
538-541
C.W. Barrett, D.L. Dill and J.R. Levitt, “A Decision Procedure for Bit-Vector
Arithmetic”, Proceedings of DAC 1998
J.R. Burch and D.L. Dill, “Automatic Verification of Pipelined Microprocessor
Control”, Proceedings of CAV 1994
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
371
Papers
•
•
•
•
M.N. Velev, “Automatic Abstraction of Memories in the Formal Verification of
Superscalar Microprocessors”, Proceedings of Tools and Algorithms for the
Construction and Analysis of Systems (TACAS) 2001, pp. 252-267
M.N. Velev, “Formal Verification of VLIW Microprocessors with Speculative
Execution”, Proceedings of CAV 2000, pp. 296-311
M. Pandey, “Formal Verification of Memory Arrays”, Ph.D. Thesis, School of
Computer Science, Carnegie Mellon University, May 1997
J.X. Su, D.L. Dill and C.W. Barrett, “Automatic Generation of Invariants in Processor
Verification”, Proceedings of FMCAD 1996
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
372
Books
•
•
•
•
•
•
•
•
K. L. McMillan, ``Symbolic Model Checking'', Kluwer Academic Publishers, 1993.
Z. Manna and A. Pnueli, Temporal Specification and Verification of Reactive Systems Vol. I
and II, Springer 1995.
Ching-Tsun Chou, "The Mathematical Foundation of Symbolic Trajectory Evaluation",
Springer-Verlag 1999.
Thomas Kropf: "Introduction to Formal Hardware Verification", (Springer Verlag; ISBN:
3540654453, 299 pages, January 2000)
E. M. Clarke, O. Grumberg and D. Peled, "Model Checking", (MIT Press; ISBN: 0262032708;
330 pages; January 2000)
L. Bening and H. Foster, “Principles of Verifiable RTL Design: Functional Coding Style
Supporting Verification Processes in Verilog”, published by Kluwer Academic Publishers,
2000.
M. Yoeli, "Formal Verification of Hardware Design", IEEE Computer Society Press, 1991.
(Book containing a collection of papers)
R. P. Kurshan, “Computer Aided Verification of Coordinating Processes”, Princeton
University Press, 1994.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
373
Books
•
•
•
•
G. J. Holzmann, “Design and Validation of Computer Protocols”, Prentice Hall, 1991.
M. P. Fourman, “Formal System Design”, Formal Methods for VLSI Design, IFIP, 1990,
North-Holland.
C. Meinel and T. Theobald, “Algorithms and Data Structures in VLSI Design”, SpringerVerlag, 1998.
M. Kaufmann, P. Manolios, and J S. Moore, "Computer-Aided Reasoning: An Approach",
(Kluwer Academic Publishers, June 2000; ISBN 0792377443)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
374
Important web-sites:
•
http://www.comlab.ox.ac.uk/archive/formal-methods.html
•
http://www.csl.sri.com
•
http://dimacs.rutgers.edu/Workshops/SYLA-Tutorials/program.html
•
http://www-cad.eecs.Berkeley.edu/ vis
•
http://godel.ece.utexas.edu/texas97-benchmarks/
•
http://citeseer.nj.nec.com/
•
http://www.rational.com/uml (Universal Modelling Language HOME-PAGE)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
375
Conference Proceedings
•
Computer Aided Verification (CAV)
•
Formal Methods in Computer Aided Design (FMCAD)
•
International Conference on Computer-Aided Design (ICCAD)
•
International Conference on Computer Design (ICCD)
•
Design Automation Conference (DAC)
•
Asia South Pacific Design Automation Conference (ASPDAC)
•
International Conference on VLSI Design (VLSI)
•
Advanced Research Working Conference on Correct Hardware Design and
Verification Methods (CHARME)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
376
Journals/Magazines
•
IEEE Design and Test of Computers
•
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
•
IEEE Transactions on Computers
•
IEEE Transactions on VLSI Systems
•
ACM Transactions on Design Automation of ELectronic Systems
•
Formal Methods in System Design
•
Formal Aspects of Computing
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
377
Appendix
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
378
Formal Modeling
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
379
Non-determinism (another example)
•
•
•
•
3- floor elevator controller, Si - in floor i
ri - request from floor i
This machine is also nondeterministic
In S2 state when r1 and r3 arrive.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
380
Formal Specification
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
381
Linear Temporal Logic
Syntax
• Atomic propositions are formulae
• If f, g are formulae then so are
• ¬f, f  g, f  g, f  g, f  g
• □ f - Henceforth f
• ◊ f - Eventually f
• f U g - f until g
• f W g - f unless g
• Of - next f
• state formulae - no temporal operators
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
382
Semantics
• Formulae interpreted over infinite sequences of
states
• States evaluate state formulae
• Let s = q0, q1 , … be a sequence
• Each qi assigns truth values to atomic
propositions
• Semantic definition defines when a formula
satisfies a sequence
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
383
Semantic Definition
• Notation: s ╞ A
stands for A holds in s.
• s ╞ A iff (s ,0) ╞ A
• (s , j) ╞ A - defined inductively
• Base case:
(s , j) ╞ f for any state formula f iff f holds in
the state s [j]
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
384
Semantics of Temporal Operators
• □(s , j) ╞ □f iff k j, (s, k) ╞ f
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
385
Semantics Contd.
• (s , j) ╞ ◊f iff k  , ( s ,k) ╞ f
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
386
Semantics Contd.
• (s , j) ╞ f U g iff k  j : (s, k)╞ g and
i s.t. j  i < k, (s, i)╞ f
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
387
Semantics Contd.
• (s , j) ╞ f W g iff (s , j) ╞ f U g or
(s , j) ╞ □ f
• (s , j) ╞ Ο f iff (s , j + 1) ╞ f
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
388
Examples
• p  □q
If p holds in the beginning then q holds always
• □(p  □q)
Whenever p holds there is a future instant in
which q holds
• □◊p
p holds infinitely often
• ◊□p
p holds at all but finitely many positions
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
389
Examples - Properties
• □¬(farm_go high_go)
• □ (farm_car  ◊ farm_go)
• □ (mem_rd  ◊ mem_ack)
• □ (mem_rd  mem_rd W mem_ack)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
390
w- Automata
• An alternate formalism for specifying infinite objects
• Extension of Finite Automata to specify properties
about infinite runs
• The simplest kind is Büchi automaton:
< Q, S, , q0 , A >
• Q - finite no. of states
• S - Edge labels
• q0 - initial state
•  Q x Sx Q
• A  Q, Accepting (not final) states
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
391
Behavior of w- Automata
•
•
•
•
starts from the initial state,
`runs forever'
accepts infinite sequences over label alphabet
s = l0, l1, l2, . . . is accepted by the automaton,
provided there exists q0, q1,… s.t.
• (qi, li, qi+1) Є  for i = 0, 1, …
• there is an accepting state that occurs infinitely
often in s.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
392
Examples
• All sequences containing only 1.
• An infinite set of infinite sequences!
• But finite description
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
393
Examples contd.
• All sequences that has at least one occurrence of
1
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
394
Examples contd.
• Sequences containing all but finitely many
occurrences of 1s
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
395
Examples contd.
• All sequences containing infinitely many 1s
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
396
Features of w- automata
•
•
•
•
useful for specifying properties and constraints
precise and unambiguous
consistency can be checked (Emptiness of automata)
has many properties useful for verification:
• w - languages closed under union, intersection
and complementation
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
397
Model Checking
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
398
LTL Model Checking
(Pnueli, Lichtenstein, Vardi, Wolper)
M╞ F
Read: M `contains' only models of F
• M a finite state system or an w-automaton
• F a linear TL formula
• M defines a set of infinite state sequences LM and
F another set of sequences LF .
• Checking M╞ F amounts to checking LM  LF
• Hence referred to as language containment
problem
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
399
Illustration
Which of the following hold for all the sequences
generated by the above
• ◊p, ◊¬q, □p, □ (p  q)
• ◊(p q), ◊ (p  q), □◊(p  q),
• ◊ □p, (p  ◊q).
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
400
LTL Verification Method
• Two related Methods:
• Tableau – based
• Automata – based
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
401
Automata based Method
• Obtain an w-automaton for the negation of the
formula
• Take the product of system model and wAutomaton
• Check whether the resulting automaton accepts
any string at all (Emptiness Check).
• Existence of an accepting cycle in the product
graph
• If no cycle then original property holds.
• A cycle gives a counterexample - an execution
trace that violates the formula; useful for
debugging
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
402
Example
1. To check whether this is a model for □ P,
construct first a w- Automata for ◊¬p
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
403
Example contd.
 Construct the product of the two automata:
•
No reachable accepting cycle
•
It is a model of □ p.
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
404
Another Example
 Check whether the following automaton satisfies □
◊¬p
w- Automata for : ¬( ◊ □ ¬p)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
405
Product Automata
• There is a cycle and hence the automaton is not a
model
• If state 4 is the only accepting state then the formula
holds
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
406
Complexity of LTL model-checking
• Linear on model size and exp. on formula size
• Formulae are generally small!
• Model size exponential on block size (no. of storage
elements).
• State Explosion Problem
• Various Reduction Techniques:
• Nested depth first search for cycles
• On the fly checking
• Partial order reduction
• Clever hashing techniques
• OBDD based Symbolic techniques
• Compositional Verification
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
407
Binary Decision Diagrams
(S. Chakraborty)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
408
Neat Tricks in BDD Packages
• Shared BDDs (SBDDs)
• Multiple functions represented simultaneously
as a multi-rooted DAG.
• Each root and descendants form an ROBDD
• Different roots can share subgraphs
• Representing functions using ITE operator
• if-then-else (x, y, z) = x.y + x’z
• Natural implementation using BDDs
• Can express any binary Boolean operation :
NAND(x, y) = ITE(x, y’, 0); NOT(x) = ITE(x, 0, 1)
• Efficient algorithm for computing ITE with
BDDs exists
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
409
Neat Tricks in BDD Packages
f = x1.x2 + x3’
• Complement edges
x1
x2
• If a vertex is reached by a
complement edge, take the
x3
complement of the function
0
1
represented by the vertex
f = (x1.x2’x3’ + x1’x3)’
• Simplifies complementation
• Saves duplication of computation
x1
• Hash Tables and Caches
x2
• Facilitates identifying ROBDD node
x3
for an already computed function
0
1
• Avoids computation duplication
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
410
Academic & Research Lab
Verification Tools
(S. Ramesh)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
411
Spin
• Home page:
http://netlib.bell-labs.com/netlib/spin/whatispin.html
•
•
•
•
•
Bell Labs. (G. Holzmann)
Verification of asynchronous protocol descriptions
Modeling Language: PROMELA
Specification Language: LTL
Verification Approach: Automata Containment
(Explicit Model Checking)
• Symbolic verification (recent addition)
Promela (Protocol Modeling Language)
• Concurrent and nondeterministic processes
• Process communication: messages via buffered
and non buffered channels
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
412
An Example Promela Program
chan in = [size] of {short}
chan out1 = [16] of {short}
chan out2 = [16] of {short}
proctype split()
{short x
do :: in?x ®
if :: (x>=100) ® out1!x
:: (x<=100) ® out2!x
fi
od
}
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
413
An Example Promela Program
proctype merge()
{ short y
do :: if
:: out1?y
:: out2?y
fi;
out!y
od
}
init {run split(); run merge() }
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
414
Spin Features
• Random Simulation
• Deadlock detection and Formal verification
• A clever implementation of on-the- fly model
checking algorithm
• A number of powerful reduction techniques:
• Supertrace algorithm: bit state hashing
• Partial order reduction
• Symbolic techniques
• Many telecommunication protocols have been
verified
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
415
More on FormalCheck
Home page:
http://www.cadence.com/datasheets/formalcheck.html
• Commercial model-checking tool (Cadence)
• Originated from COSPAN (Bell Labs.)
• Modeling languages: synthesizable subsets of
Verilog and VHDL
• Specification Language: FQL – FormalCheck Query
language (A variant of LTL, Syntax same as HDL)
• Verification Approach: Automata Containment
• Powerful compositional reduction strategies
• Clever representation for specifications
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
416
Example Specifications
• after { Req == 1 }
eventually { Ack == 1 }
• after { Timer.Start == 1 }
always { Timer.counting == 1 }
unless { Timer.Restart == 1 }
After timer starts, counting is on unless it is
restarted
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
417
Example contd.
• never { TAP.State == TRST }
within -delay 0 -duration 6
{ Clock.rising }
• States that it is not possible to reach the TRST
state in 5 steps.
• after { Counter.bit[0] == 1 }
eventually { Counter.bit[0] == 0 }
within -delay 0 -duration 2
{Clock.rising }
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
418
FQL Formulae
•
•
•
•
•
•
•
after( ) always/never( ) [unless[ after]( )] [within(m,n)]
always/never( ) [unless[ after]( )]
after( ) eventually( ) [unless( )] [within(m,n)]
eventually( ) [unless( )]
after( ) eventually always( ) [unless( )] [within(m,n)]
eventually always( ) [unless( )]
if repeatedly( ) eventually always( )
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
419
Appendix
High Level Specification and Modeling
(T. Nakata)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
420
UML : Use-Case Diagram
• Define system functions from users’ view
Actor
Vending machine
Use-case
Buy a juice
Customer
Refill products
Supplier
Gather changes
Services
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
421
UML : Sequence Diagram
• Describe a scenario --- an instance of a use-case
• Specify interactions among objects in order of
time
Scenario: buy juice
:Panel
:Container
:Emitter
Inject a coin
Send
Choose juice
Equal to price
Emit a can of juice
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
422
UML : Class Diagram
• Describe static aspects of a system by
relationships among classes
• A class represents a “concept” in a system
Employee
Name: string
ID: integer
PC
uses
Name: string
0..1
1..* CPU: string
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
423
UML : State Diagram
• Describe states and their transitions of objects
• Almost the same as hierarchical FSMs
Ground
floor
Up(fl)
Ascend
to floor fl
Arrived
Up(fl)
Descend Arrived
to floor fl
Stop
Down(fl) timer=0
inc timer
[timer=time_out]/Down(0)
ASPDAC / VLSI 2002 - Tutorial
on "Functional Verification of
424
Descargar

No Slide Title