368
M. Mann and C. Barrett
and demonstrate dramatic reductions in the time to reach deep bugs on certain classes of synchronous circuits. Moreover, the technique requires only an
interface-level annotation of the circuit, and when fully automated approaches
fail, can be guided by the user. The paper makes the following contributions:
1. We adapt partial order reduction for synchronous hardware verification.
2. We introduce a novel technique for reducing the possible inputs to a circuit
at a single time step, which is crucial for practical application of partial order
reduction to synchronous hardware.
3. We provide a set of sufficient conditions, which, if proven, guarantee that
the proposed techniques maintain the reachable states.
4. We introduce conservative proof techniques for verifying these conditions,
which empirically work well on packet movers.
5. We evaluate our techniques on a set of open-source and commercial packet
mover circuits, demonstrating dramatic speed-ups with minimal manual effort.
The rest of the paper is organized as follows. We first provide a motivating
example, below. Then, in Section 2, we cover relevant background material and
notation. We explain our partial order reduction in Section 3 and our interface
simplification technique in Section 4. We provide an experimental evaluation in
Section 5. Section 6 covers related work, and Section 7 concludes.
1.1 Motivating Example
Throughout this paper we use the running example shown in Code Snippet 1. We
chose this example because: i) it is easy to understand; ii) it resembles real-world
packet mover circuits; and iii) it contains a difficult to reach bug.
The system has a synchronizing clock and takes two 1-bit inputs: inc x and
inc y. The 6-bit registers (state elements) x and y index the valid vector
and are initialized to 0. The 64-bit registers valid and data start at 0 and 1,
respectively. The 64x64 bit memory is uninitialized. If inc x and en x are true,
the system increments the value of x. When inc y is true, the system increments
y, sets the valid bit at index y, writes data to the memory at location y, and
rotates the data vector to the left. Notice that the en x signal ensures that x
never surpasses y (until all bits in valid are set). This incrementing pointer
logic is similar to that found in a circular pointer FIFO. To ensure the asserted
property, the code attempts to maintain the invariant: data = 1 << y.
At first, it appears that the asserted property should hold based on this
invariant, but it does not. There is a bug that can first occur at cycle 65: the
overflow check in the data update uses integers, which are assumed to be 32bits. Since y is zero-extended to be 32-bits, y+1 can never be equal to 0. Thus,
when y has the value 63 and is incremented, data, which is supposed to be
one-hot, is set to 0.
Although the system is small, this is a surprisingly difficult bug to reach using
model checking. We believe this is due in part to the non-determinism in the
M. Mann and C. Barrett
and demonstrate dramatic reductions in the time to reach deep bugs on certain classes of synchronous circuits. Moreover, the technique requires only an
interface-level annotation of the circuit, and when fully automated approaches
fail, can be guided by the user. The paper makes the following contributions:
1. We adapt partial order reduction for synchronous hardware verification.
2. We introduce a novel technique for reducing the possible inputs to a circuit
at a single time step, which is crucial for practical application of partial order
reduction to synchronous hardware.
3. We provide a set of sufficient conditions, which, if proven, guarantee that
the proposed techniques maintain the reachable states.
4. We introduce conservative proof techniques for verifying these conditions,
which empirically work well on packet movers.
5. We evaluate our techniques on a set of open-source and commercial packet
mover circuits, demonstrating dramatic speed-ups with minimal manual effort.
The rest of the paper is organized as follows. We first provide a motivating
example, below. Then, in Section 2, we cover relevant background material and
notation. We explain our partial order reduction in Section 3 and our interface
simplification technique in Section 4. We provide an experimental evaluation in
Section 5. Section 6 covers related work, and Section 7 concludes.
1.1 Motivating Example
Throughout this paper we use the running example shown in Code Snippet 1. We
chose this example because: i) it is easy to understand; ii) it resembles real-world
packet mover circuits; and iii) it contains a difficult to reach bug.
The system has a synchronizing clock and takes two 1-bit inputs: inc x and
inc y. The 6-bit registers (state elements) x and y index the valid vector
and are initialized to 0. The 64-bit registers valid and data start at 0 and 1,
respectively. The 64x64 bit memory is uninitialized. If inc x and en x are true,
the system increments the value of x. When inc y is true, the system increments
y, sets the valid bit at index y, writes data to the memory at location y, and
rotates the data vector to the left. Notice that the en x signal ensures that x
never surpasses y (until all bits in valid are set). This incrementing pointer
logic is similar to that found in a circular pointer FIFO. To ensure the asserted
property, the code attempts to maintain the invariant: data = 1 << y.
At first, it appears that the asserted property should hold based on this
invariant, but it does not. There is a bug that can first occur at cycle 65: the
overflow check in the data update uses integers, which are assumed to be 32bits. Since y is zero-extended to be 32-bits, y+1 can never be equal to 0. Thus,
when y has the value 63 and is incremented, data, which is supposed to be
one-hot, is set to 0.
Although the system is small, this is a surprisingly difficult bug to reach using
model checking. We believe this is due in part to the non-determinism in the