Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
377
Fig. 3: Equivalence of original and reduced instruction sequences. Circles represent states.
we have enumerated all possibilities. This algorithm is a specialized ∀∃ decision
procedure that exploits the structure of (5) and additional domain knowledge
about the proof goal. We use a constraint solver as an oracle.
Algorithm 1 ProveRIS(S)
1: S
:= S
, Init
, A
, En
, D
, T
← copy sys(S)
2: I := P(A), I
:= P(A
)
// instruction sets are power sets of actions
3: var i : I, var i
: I
, var a : A
4: var s : S
2 , var s
: S
3 , var d : D, var d
: D
5: add constraint(s0 = s
0 ∧ d = d
∧ i
= i − {a})
6: add constraint(T (i, d, s) ∧ T
(i
, d
, {a}, d
, s
))
7: for c = 2 ... |A| do
8:
while check sat(|i| = c ∧ s1 = s
2 ) do
9:
μ ← get model ()
10:
iμ ← assignment(μ, i)
11:
aμ ← assignment(μ, a)
12:
add constraint(iμ ⊆ i =⇒ a = aμ)
13:
if ¬check sat(i = iμ) then
14:
return false // exhausted all possible decompositions for this instruction
15:
end if
16:
end while
17: end for
18: return true
// every instruction can be decomposed
Algorithm 1 takes an STS, S := S, Init, A, En, D, T and returns true if the
instruction set can be decomposed into an atomic instruction set by delaying a
single action from each instruction.
2 For simplicity, the algorithm assumes (and
we check this assumption separately) that if a complex instruction i is enabled,
then for each a ∈ i, executing i − {a} results in a state where a is enabled.
2 We also implemented a more general version of this algorithm which can drop more
than one action at a time from the instruction i, but this simpler version is sufficient
for the results we report in this paper.