Verification of Event-Based Synchronization of SpecC Description
Using Difference Decision Diagrams
Thanyapat Sakunkonchak and Masahiro Fujita
Introduction
•
•
•
•
•
Verification Flows
More and more complex and larger VLSI must be designed with shorter time-to-market
SoC needs simultaneous development of both HW and SW
Needs ways to describe HW/SW seamlessly
C-based specification/design languages are promising
SpecC [http://www.SpecC.org]
– Standardized for HW/SW co-design
– Based on ANSI-C and extended
S p ecC S o urce
P ro g ram
V e r ifica tion of S p e c C sy n c h r on iza tion
P a r sed & T ran sla ted (1 )
S p ecC sou r ce is p ar sed an d tran sla ted
in to B o olea n S p ecC an d th en to C + +
a ccom p a n ied w ith D D D . T h en , ch eck for
s yn ch r on iza tion wh eth er it is satisfied . If
it is, ter m in a tes w ith S A T IS F IE D .
O th er w ise, g o to th e n ex t sta g e.
B o o le a n S p ecC
The Verification Problem
V e r ify in g S ta g e:
(cu rr en t im p lem en tation )
P a r sed & T ran sla ted (2 )
• Given SpecC programs, check if specific ordering of executions are guaranteed or not
• Along with well-accepted Boolean comparison techniques for logic designs , this could be a basic verification method
to check if sequential and parallel version of the same SpecC are equivalent or not
(S e q u e n tia l)
C
S e q u e n tia l
S p e cC
P a ra lle l
S p e cC
V e r ifica tion of S p e c C sy n c h r on iza tion
U s er s a dd som e pr op er ties
to be ch eck
S ync hro n izat io n
is
S A T IS FIE D
C + + w ith D D D
C o un te r -e xa m p le & R e fine m e n t S ta ge :
(on -g oin g w or k )
Y es
V er ify:
PASS?
E q u iv a le n ce ch e ck in g
‘S V C ’ an d ‘Pr og ra m S licin g ’ m a y b e
con sid er ed to h elp ver ifyin g an d r efin in g
th e con d ition of p r ed icate C i. If it is n ot
r ealiz a ble, it m ean s th a t th e r esu lt is
con cr ete en ou gh to u se a s th e C O U N T E R E X A M P L E . U N S A T IS F IE D w h en it is
r ealiz a ble, an d D O N ’T K N O W , oth er w ise.
No
SVC
R e fin em en t
Boolean Program (BP)
Difference Decision Diagrams
• Introduce by MΦller, et al.
• Symbolic representation of ‘non-boolean’, such as inequality: less efficient if using BDD
• DDD represents difference constraints (x-y≤c), x,y are integers, c is constant
Represents graph for
¬(x−z<1)Λ(x−y≤0)Λ(y−z≤2)
R ea liz a ble
N O C O U N T E R -E X A M P L E
P ro g ram S lic in g
N ot r ealiz a ble
D O N ’T K N O W
…
• Proposed by Ball and Rajamani under SLAM project at Microsoft Research
• Think of SW like a model (like FSM in HW) and verify it by first abstracting away unnecessary statements with userdefined predicates
• BP abstracts the original program:
if properties on BP hold, so as original one
V er ify
C o nd it io n o n C i
PASS?
C O U N T E R -E X A M P L E
Conclusion and Outlook
• Current implementation:
– Can handle basic SpecC constructs only
– Able to get some properties to be checked
– Verify for Satisfied or Unsatisfied (no error trace): “Don’t know” is don’t know (no support)
• Future plan:
– When verification fails, try to give the counter-examples (error trace)
– Based on error traces, plan to develop automatic “refinement of abstractions”
– Expand capability to support more complex SpecC structure, e.g. loop, functions, recursive
Descargar

Slide 1