Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
373
Fig. 1: Partial Order Reduction Condition (3) Proof Goal
imply guarded independence. These conditions are also standard in the POR
literature [14,37]. The first condition states that instruction i 0 cannot disable i 1
under guard g:
∀ d ∈ D, s ∈ S
2 . (en i1 (s 0 ) ∧ g(s 0 ) ∧ T (s 0 , i 0 , d, s 1 )) =⇒ en i1 (s 1 )
(2)
Intuitively, this condition ensures that we do not remove reachable states by
disabling instructions. The second condition is that executing the instructions
in either order leads to the same final state:
∀d 0 , d 1 ∈ D, s, s
∈ S
3 . (g(s 0 ) ∧ (s 0 = s
0 ) ∧
T (i 0 , d 0 , i 1 , d 1 , s) ∧ T (i 1 , d 1 , i 0 , d 0 , s
)) =⇒ (s 2 = s
2 )
(3)
When applying partial order reduction to concurrent programs, the standard
approach is to check conservative syntactic properties which guarantee conditions
(2) and (3). Synchronous systems do not typically have these syntactic properties, because there is no notion of distinct processes. Instead, we must check
these conditions directly. In real circuits, it is unlikely that (2) will hold over
arbitrary states. However, it is sufficient to prove that it holds for all reachable
states. This can be done with a model checker.
To prove (3), we could encode it as an LTL property or build a monitor
automaton and use a model checker. Alternatively, we have found that we can
often use a straightforward commuting-diagram approach starting from a symbolic initial state, depicted in Fig. 1. We duplicate the system, unroll it twice,
then start both copies in the same symbolic state and check that applying the
instructions in either order results in the same final state. This simple approach
has the disadvantage that a symbolic initial state ignores reachability which
could lead to spurious counterexamples. However, notice that the initial state
is constrained by enabledness assumptions. To apply an instruction it must be
enabled, so both instructions must be enabled in the initial state. We have found
that these enabledness assumptions often constrain the initial state enough to
rule out spurious counterexamples.
373
Fig. 1: Partial Order Reduction Condition (3) Proof Goal
imply guarded independence. These conditions are also standard in the POR
literature [14,37]. The first condition states that instruction i 0 cannot disable i 1
under guard g:
∀ d ∈ D, s ∈ S
2 . (en i1 (s 0 ) ∧ g(s 0 ) ∧ T (s 0 , i 0 , d, s 1 )) =⇒ en i1 (s 1 )
(2)
Intuitively, this condition ensures that we do not remove reachable states by
disabling instructions. The second condition is that executing the instructions
in either order leads to the same final state:
∀d 0 , d 1 ∈ D, s, s
∈ S
3 . (g(s 0 ) ∧ (s 0 = s
0 ) ∧
T (i 0 , d 0 , i 1 , d 1 , s) ∧ T (i 1 , d 1 , i 0 , d 0 , s
)) =⇒ (s 2 = s
2 )
(3)
When applying partial order reduction to concurrent programs, the standard
approach is to check conservative syntactic properties which guarantee conditions
(2) and (3). Synchronous systems do not typically have these syntactic properties, because there is no notion of distinct processes. Instead, we must check
these conditions directly. In real circuits, it is unlikely that (2) will hold over
arbitrary states. However, it is sufficient to prove that it holds for all reachable
states. This can be done with a model checker.
To prove (3), we could encode it as an LTL property or build a monitor
automaton and use a model checker. Alternatively, we have found that we can
often use a straightforward commuting-diagram approach starting from a symbolic initial state, depicted in Fig. 1. We duplicate the system, unroll it twice,
then start both copies in the same symbolic state and check that applying the
instructions in either order results in the same final state. This simple approach
has the disadvantage that a symbolic initial state ignores reachability which
could lead to spurious counterexamples. However, notice that the initial state
is constrained by enabledness assumptions. To apply an instruction it must be
enabled, so both instructions must be enabled in the initial state. We have found
that these enabledness assumptions often constrain the initial state enough to
rule out spurious counterexamples.