Transcript DAC Presentation kit

Can We Really do Without the
Support of Formal Methods in the
Verification of Large Designs ?
Special Session on Formal Verification
DAC 2005 – Anaheim
Jun 16, 2005
Umberto Rossi
STMicroelectronics – Agrate Brianza - Italy
Outline

Progress through the last 10 years from STM view

How Formal Verification is used in STM

Examples of success in STM

How Formal Verification can make the difference

The example of IP Validation

What can help Formal verification to fly

Hints for the future & conclusion
Progress through the last 10 years


The Pentium FP bug made the concept of
“corner case” familiar to an extended community
of designers (1994)
ASIC design, 2 MGate systems, .35m process (1995)
– commercial Formal Verification was limited to
(combinational) Equivalence Checking
– mainly Gate 2 Gate – few 100’s KGate blocks

serious limitations in name mapping
– custom-like designs via Transistor Abstraction
– only one design group was using E.C. in ST

Commercial Property Checking was still to come (98)
Progress through the last 10 years

SoC/SiP, 100’s MGate system, 90nm process

Equivalence Checking is massively used
– 2 commercial products used in ST

Several formal products dealing with
Functional Verification
– 4 different solutions used in ST with little
penetration each
Progress through the last 10 years




Long story of start-up’s, mergers and acquisitions
(Verplex  CADENCE 0-In  MENTOR)
just to mention the latest
The tools in the Formal verification arena have
completely re-shaped themselves
Testbench Automation has dominated the verification
market since the last 90ties both in the IP and the
System Level domains
Functional Verification based on Formal Verification
has not even competed with Testbench Automation
What is in a Formal Verification tool
User Defined Properties
GDL/Sugar, PSL,
SVA/OVA
Formal
Verification
Process
Encrypted Protocol
VIP Libraries
User Solver Control
Solver Schedule
Solver 5
Solver 4
Solver 3
Solver 2
P ro p. 1
P ro p. 2
P ro p. 3
Solv. 1
How Formal Verification is used in STM


Testbench based methodology is by far the most
used for IP validation, especially for protocols
Formal product-I for proof – module level
– 50%: “COPS” package for STBus protocol
checking – IP level
– 50%: custom properties

Formal product-II for bug hunting – IP level

Formal product-III used with ABV features

about 10 people can address Formal Verification
Typical usage of Protocol Checking
Sensor
Comm.
Peripheral Interrupt
Contr.
Contr.
MCU
Data
MCU
Code
FP_ALU
T1
eWarp
GPIOs
eWarp/T1
Bridge
Formal Verification is used on top of Testbench approach
for certain architecture hot spots
Host/I2C
VP
Arbiter
Parallel
Interface
T1
P1
JPEG
P2
CCIR656
CCP1.1
YUV
DMA
T2
T2
RGB/YUV
DMA
T2
T2/SRAM or Memory controller
T2
P2
4.6MHz UIF
T2
Dual
Pixel
Pipe
P1
T1/T2
T2
SPI
Taking advantage of Formal
Verification beyond module level

End-to-End, black-box, “simple” properties
– general functional properties that presumably involve
the whole “block” function

Typically ~10 independent properties
– Data integrity
– Data persistence
– Arbitration

Allows checking robustness of RTL, via reasonable
under-constraining of the environment
Ex: generating transaction scenario
M1
M2
slave 1

– 6 Masters 19 Slaves
– matrix of relations is
incomplete,
each master sees a
fraction of address space
– total utilization < ½ of
available address space
slave 2
M3
slave 3
M4
M5
slave 4
.
.
.
slave 18
M6
Bus infrastructure
slave 19
232
addr 
space

Setup is the same for all
masters
– no need to bias address
generation depending on
{master, slave}
Found a protocol violation
when error is notified
Testbench verification setup

Infrastructure implemented by Multi-Layer AHB
M1
M2
M3
AHB bus
S1
S14
S15
M4
M5
M6

AHB
Matrix
S19
Testbench built by adapting Single Layer V.C.
– avoid building new V.C. tried to re-use existing
– 1st configuration, the violation is missed by monitors !
– 2nd configuration, cumbersome but monitors work
Formal Verification strengths

Exploring a huge scenario of input sequences

Seamless configuration of environment components
– eases reusability of environment blocks
– eases environment component plug-in

Does not need to weight/bias test pattern generation
– like in the case of large address ranges

protocol properties: 6 (master) + 29 (slave)

2 functional properties  Address Map Check
Ex: diagnosing a failure in the field
A system hang occurred in
the real silicon
A block is suspected
bool arm_write : ~nMREQ && nWAIT && nRW &&
ADDR_M0[31:2]==30'h8000000; // `timeout’ address
assert check_reg : check (evn_check_reg);
clock posedge clk {
logic [15:0] reg_val = 16'hffff;
Problem: what are the
generating conditions ?
// register reset
reg_val <= arm_write ? DATA_M0[15:0] : reg_val;
}
event evn_check_reg : timeout==reg_val;
Does the schema work
for all transaction
combinations and
sequences ?
M0 silent - M1 active
BUG:`timeout’ written
by M0 is corrupted on
invalid transaction
Formal Verification capabilities
Temporal
Properties
FIFO full
FIFO empty
End-to-End
Properties
Functional
Intent
Structural Checks
Implied
full_case
parallel_case
Integrity Checks
Out of Bounds Semantic Checks
Assertion
Languages
e PSL
SVA/OVA
Powerful
Extraction
Capabilities
Intent
Mixed
VHDL/VERILOG
Formal Verification capacity
Temporal
Properties
FIFO full
FIFO empty
End-to-End
Properties
Functional
Intent
Full Block
Complex
Infrastr.
Full IP
Structural Checks
Implied
full_case
parallel_case
Integrity Checks
Out of Bounds Semantic Checks
Intent
Full IP
Full Chip
Opportunities for Verification success ?

Cost of masks, exceeding $1M in 90nm
– makes re-spin impossible to sustain

Number of transistors in IP (RTL ‘big’ modules):
– .25m
 30%
– 90nm  90%
– assuring IP quality becomes a key factor to achieve
reusability among different projects

Address the right demanding market
– Automotive: the process qualification requires 2,3
years, so increasing the risk for late bug finding
How to enhance the Verification flow ?
30% Design
vs
70% Verification
is a dream
Design
30%
Verif.
70%
– product groups cannot
afford this rate as far as
engineering resources are
considered
– team managers still feel
more confident with system
level verification but this
makes controllability and
debugging much harder
How to enhance the Verification flow ?


Formal Verification helps simplifying the scenario
generation, e.g. by means of assertion constraints
Harry Foster’s et. al. “line of intent” concept
– formal verification can help in simplifying the ‘how’
and concentrate the effort on the ‘what’

Example: reachability analysis on FSM
type state is (A,B,C,D,E ...);
signal SM: state;
– Reach all states in FSM: cover SM vector
– Reach all arcs in FSM: cover {SM X SM} array
Pervading the Verification flow

Strong point of Testbench Automation
– Scalability (layered verification methodology)
– Coverage metrics

How to obtain better coverage, white box verification
–
–
–
–
–
–
Checking forbidden conditions in state-holding loops
Clock Domain Crossing
Out of Bounds
Bus Contention / Mutual exclusivity
FSM traversal
Cross FSM traversal
The RTL-IP Verification flow
Design
Convention
compliance
Functional
Specification
1
Reset State
Analysis
2
Integrity
Checks
3
Struct/Arch
Checks
4
5
Functional
Validation
What can help Formal Verification to fly


Availability of `Verification Component’ s for
standard I/F, interoperable with simulation
Assertion Based Verification
– it is the simplest way to achieve a unified criterion of
coverage among Simulation and Formal Verification

Provide “approximated” methods that can help to
afford larger capacities – bug hunting
– Bounded Model Checking
– custom exploration capabilities
– Assertion Based Test Generation
Further application areas

Sequential Equivalence Checking
– 90nm technology requires architectural modification
of the RTL module
– a reasonable level of S.E.C. should be made available

RTL vs C formal proof
– Supporting the development of Behavioral Synthesis

Verification of parametric IP’s
– The RTL instance of a parametric IP is verified standalone today, simply because we are not sure that our
configuration works correctly
Open issues


The problem of several assertion languages
– e, PSL, SVA/OVA
Support of mixed HDL language
– VHDL support generally comes very late in
commercial products


Functional coverage from Simulation and Formal
Verification “reasonably” combined
Ways to evaluate property coverage
Conclusions


Formal Methods are already penetrating classical
verification methodology, especially at the low level,
to verify the designer’s “implied intent”
Formal Verification usage model must become closer
to the traditional verification engineer culture
– standard Verification Components interoperable with
simulation  this is an important vendor differentiator
as it requires specific features in the tools !
– integrated coverage measure capabilities among
simulation and formal verification

No room for “gurus” exclusively devoted to FV