Transcript slides (PowerPoint) - Newcastle University

Combining Decomposition and
Unfolding for STG Synthesis
(application paper)
Victor Khomenko1 and Mark Schaefer2
1School
of Computing Science,
Newcastle University, UK
2Institute of Computer Science,
University of Augsburg, Germany
Asynchronous circuits
 The traditional synchronous (clocked) designs
lack flexibility to cope with contemporary
design technology challenges
Asynchronous circuits – no clocks:
 Low power consumption and EMI
 Tolerant of voltage, temperature and
manufacturing process variations
 Modularity – no problems with the clock skew
and related subtle issues
[ITRS’05]: 22% of designs will be driven by ‘handshake
clocking’ in 2013, and 40% in 2020
 Hard to synthesize efficient circuits
 The theory is not sufficiently developed
 Limited tool support
2
Syntax-directed translation
Idea:
Convert the specification
to a network of standard
handshake components
(Balsa, Tangram)
 Computationally efficient
 Solution is guaranteed
 Produces highly over-encoded circuits, with
large area and low performance
3
Logic synthesis
Idea:
Synthesize the circuit by
exploring the state space
of the specification
 Produces good circuits
 Solution is not guaranteed
 State space explosion: synthesis
based on state graphs is feasible
only for small specifications (2030 signals for BDD-based Petrify)
4
Unfoldings




Alleviate the state space explosion problem
More visual than state graphs
Proven efficient for model checking
Can often synthesize specifications with
100-200 signals
 Still not enough for real-life designs!
5
Decomposition
Idea:
•
Decompose the control path of the
specification into smaller clusters
and synthesize them one-by-one
•
Use syntax-directed translation for
clusters on which synthesis fails
 Can halve the area of the control path and
improve its latency [Carmona, Cortadella
DAC’06]
6
Example: VME Bus Controller
Data Transceiver
Bus
dsr
dtack
VME Bus
Controller
lds
ldtack
dsr+
lds+
dtackd-
ldsdsr-
ldtackdtack+
Device
d
ldtack+
d+
7
Initial partition
dtackd-
ldsdsr-
dsr+
lds+
ldtackdtack+
ldtack+
d+
Include signal triggers
and choices:
• lds: dsr, ldtack, d
• d: ldtack, dsr
• dtack: d
lds
lds: dsr, ldtack, d
dsr
ldtack
d: ldtack, dsr
d
dtack: d
dtack
8
Initial decomposition
dtackd-
ldsdsr-
dsr+
lds+
ldtackdtack+
dtackldtack+
d+
dtackd-
d-
ldsdsr-
ldsdsr-
dsr+
lds+
ldtackdtack+
ldtack+
d+
lds+
ldtackdtack+
dsr+
ldtack+
d+
9
Transition contraction
dsr+
d-
lds-
lds+
ldtack-
dsr-
dtackldtack+
d-
lds
d
d+
Merge similar
components
dtack+
dsr+
d-
Irreducible CSC
lds+
conflict
ldtackdsr-
d+
ldtack+
d+
10
Resolving CSC conflicts
dsr+
d-
lds-
lds+
ldtack-
dsr-
ldtack+
d+
e8
dsr+
e1
e2
e3
e4
e5
dsr+
lds+
ldtack+
d+
dsr-
e7
e11
lds+
dldse9
ldtacke10
11
Resolving CSC conflicts (cont’d)
dsr+
d-
ldscsc-
csc+
lds+
ldtackdsr-
ldtack+
d+
12
Resulting Circuit
Data Transceiver
Bus
d
dtack
dsr
csc
Device
lds
ldtack
13
Implementation
Large STGs
(specification)
structural
(approximate) tests
DESIJ
decomposition
Medium STGs
unfolding-based
(exact) tests
PUNF
decomposition
MPSAT
Small STGs
(components)
synthesis
14
Safeness-preserving contractions
•
•
•
Unfolding is more efficient for safe nets
Decomposition can create unsafe nets
Contractions have to preserve safeness
t
Example
t
t
Structural condition
15
Auto-conflicts
•
•
•
Auto-conflicts appear if too many signals were
removed
Backtracking reinserts signals which remove
the auto-conflict
Unnecessary backtracking increases the
final components
a+
a+
16
Implicit places
•
•
•
•
Implicit places are places the absence of
tokens in which can never be the sole reason
for some transition to be disabled
Such places can be deleted without changing
the behaviour of the STG
Removing such places is essential for
decomposition, because they can
 cause false alarms for other tests
 prevent contractions
Structural test looks for a subset of implicit
places (redundant places, shortcut places)
17
Experimental results
•
Large trees composed of alternating levels of
sequencers and parallelisers were considered
•
Intractable for stand-alone MPSAT and Petrify
18
Experimental results
4500
4000
3500
Time[s]
3000
2500
2000
1500
1000
500
0
0
1000
2000
3000
Signals
4000
5000
19
Experimental results
•
•
•
Outperforms stand-alone
MPSAT and Petrify on large STGs
Some intractable for
stand-alone MPSAT and
Petrify benchmarks were
easily synthesized
Huge STGs can be synthesized, e.g.
SeqParTree-10 with 12598 places, 8188
transitions, and 1025 inputs and 3069 outputs
was synthesized in less then 70 minutes
20
Thank you!
Any questions?
21