Partial Order Reduction for Deep Bug Finding in Synchronous Hardware
369
Code Snippet 1: Buggy Toy Example
1
module deep_bug(input clk, input inc_x, input inc_y);
2
reg [5:0]
x = 0;
3
reg [5:0]
y = 0;
4
reg [63:0]
valid = 0;
5
reg [63:0]
data = 1;
6
reg [63:0]
mem [63:0];
7
wire
en_x;
8
assign en_x
= valid[x];
9
10
always @(posedge clk) begin
11
if (inc_x & en_x)
12
x <= x + 1;
13
if (inc_y) begin
14
y <= y + 1; valid[y] <= 1’b1; mem[y] <= data;
15
data <= (y+1 == 0) ? 1 : (data << 1);
16
end
17
end
18
19
always @ *
20
assert ((mem[x] == (1 << x)) || ˜valid[x]);
21
endmodule // deep_bug
update logic. In every state, there are 4 possible input combinations. As a result,
there are an exponential number of execution paths. Model checkers routinely
verify hardware designs with an exponential number of reachable states; however,
we have observed that systems such as this which also have an exponential
number of execution paths are difficult for a model checker to manage.
Specifically, all but two of the model checker configurations we tried timed
out at 2 hours before reaching the bug. Since bounded model checking (BMC) is
one of the best approaches for bug-finding, we focus on improvements to BMC
that help reach this bug. We introduce automated, best effort techniques that
reduce the time to hit this bug from over 1000 seconds to 46 seconds by safely
adding temporal symmetry breaking constraints to the system.
2 Background
Before explaining our algorithm, we adapt the standard notion of synchronous
transition systems and review fundamental model checking concepts below. For
a more thorough introduction to model checking, we refer the reader to [14,15].
– S: a set of states
– Init ⊆ S: a set of initial states
Definition 1. A Synchronous Transition System (STS) is a tuple, S, Init, A, En, D, T :