370
M. Mann and C. Barrett
– A: a finite set of atomic actions - logically distinct operations of the system
– En = {en a |a ∈ A}: where en a : S → B is a state predicate that holds iff
action a is enabled in a given state
– D: a set of data inputs to the system
– T ⊆ S × (P(A) × D) × S: the state transition relation, where P denotes power
set
For our purposes, an STS instruction can perform multiple atomic actions
simultaneously. We define the system’s instruction set (i.e. the set of actions
that the system can perform in one transition) as I := P(A). We then define the
set of inputs of an STS as Input := I × D. Thus, the transition relation T is a
subset of S × Input × S.
We denote the cardinality of an instruction i as |i|. For s, s
∈ S, in ∈ Input,
T (s, in, s
) holds iff it is possible to reach s
from s by applying input in.
It is often convenient to reason about sequences using vector notation. Let
in ∈ Input
n and s ∈ S
n+1 , with n > 0. We use subscripts to name individual elements of vectors, e.g. s := s 0 , s 1 , . . . . We use the notation T (in, s)
to denote
0≤i
for
some s
∈ S
n . With some abuse of notation, we allow prepending both sequences and single elements. For k > 0, we say that s ∈ S
k is reachable if
∃n ∈ N, s
∈ S
n+1 , in ∈ Input
n+k . Init(s
0 ) ∧ T (in, s
: s).
The set of enabledness predicates En constrain the valid states in which an
action can occur. For an instruction i ∈ I and s ∈ S, let en i (s) :=
a∈i en a (s).
In the remainder of the paper, we only consider transition relations T that respect
the enabledness conditions. That is, we assume ∀ s, i.(en i (s) ↔ ∃ s
, d.T (s, i, d, s
)).
Depending on the context, this can be checked with a model checker or added
as an environmental assumption. We also assume that the existence of a transition does not depend on the data input, that is, ∀ s, i. (∃ d, s
. T (s, i, d, s
) =⇒
∀ d. ∃ s
. T (s, i, d, s
)).
Example 1. We can define an STS for the motivating example. Let BV k denote
the set of all bitvectors of width k. Because there is only a single clock with
no negative edge behavior, we model the system without the clock, where every
transition corresponds to a clock cycle. Define an STS S, Init, A, En, D, T ,
where:
– S = BV 6 × BV 6 × BV 64 × BV 64 × (BV 64 )
64 is the set of values for
x, y, valid, data, mem
– Init is the set containing all states where x = 0, y = 0, valid = 0 and data
= 1
– A = {inc x, inc y}
– En = {en inc x := valid[x] = 1, en inc y := true}
– D = {nil } (here, nil is just a dummy placeholder used to ensure that T is
not empty).
– T is the relation describing the next state updates in Code Snippet 1.
M. Mann and C. Barrett
– A: a finite set of atomic actions - logically distinct operations of the system
– En = {en a |a ∈ A}: where en a : S → B is a state predicate that holds iff
action a is enabled in a given state
– D: a set of data inputs to the system
– T ⊆ S × (P(A) × D) × S: the state transition relation, where P denotes power
set
For our purposes, an STS instruction can perform multiple atomic actions
simultaneously. We define the system’s instruction set (i.e. the set of actions
that the system can perform in one transition) as I := P(A). We then define the
set of inputs of an STS as Input := I × D. Thus, the transition relation T is a
subset of S × Input × S.
We denote the cardinality of an instruction i as |i|. For s, s
∈ S, in ∈ Input,
T (s, in, s
) holds iff it is possible to reach s
from s by applying input in.
It is often convenient to reason about sequences using vector notation. Let
in ∈ Input
n and s ∈ S
n+1 , with n > 0. We use subscripts to name individual elements of vectors, e.g. s := s 0 , s 1 , . . . . We use the notation T (in, s)
to denote
0≤i
for
some s
∈ S
n . With some abuse of notation, we allow prepending both sequences and single elements. For k > 0, we say that s ∈ S
k is reachable if
∃n ∈ N, s
∈ S
n+1 , in ∈ Input
n+k . Init(s
0 ) ∧ T (in, s
: s).
The set of enabledness predicates En constrain the valid states in which an
action can occur. For an instruction i ∈ I and s ∈ S, let en i (s) :=
a∈i en a (s).
In the remainder of the paper, we only consider transition relations T that respect
the enabledness conditions. That is, we assume ∀ s, i.(en i (s) ↔ ∃ s
, d.T (s, i, d, s
)).
Depending on the context, this can be checked with a model checker or added
as an environmental assumption. We also assume that the existence of a transition does not depend on the data input, that is, ∀ s, i. (∃ d, s
. T (s, i, d, s
) =⇒
∀ d. ∃ s
. T (s, i, d, s
)).
Example 1. We can define an STS for the motivating example. Let BV k denote
the set of all bitvectors of width k. Because there is only a single clock with
no negative edge behavior, we model the system without the clock, where every
transition corresponds to a clock cycle. Define an STS S, Init, A, En, D, T ,
where:
– S = BV 6 × BV 6 × BV 64 × BV 64 × (BV 64 )
64 is the set of values for
x, y, valid, data, mem
– Init is the set containing all states where x = 0, y = 0, valid = 0 and data
= 1
– A = {inc x, inc y}
– En = {en inc x := valid[x] = 1, en inc y := true}
– D = {nil } (here, nil is just a dummy placeholder used to ensure that T is
not empty).
– T is the relation describing the next state updates in Code Snippet 1.