Added constraint support to PDR

[michael-zhang-lambda]

Changes

• Always assert constraints at FROM_STEP
• Assert constraints for TO_STEP in rel_ind and infinite frame propagation steps
• Added new inputs/chiseltest tests with constraints

Soundness

Frame Trace Invariant (HOLDS FOR VANILLA PDR WITHOUT GENERALIZATION)

All blocked cubes in the frame trace must satisfy the constraints.

Asserting Constraints at FROM_STEP

We examine all three cases:

1. In get_bad_cube, we must always assume that the frontier frame (stepped at FROM_STEP) satisfies the constraints. Otherwise, we may yield a bad cube that violates the constraints, leading to unsoundness.
2. In rel_ind, we must always assert that the previous frame $\mathbf{R}_{i - 1}$ satisfies the constraints. Otherwise, an extracted model can violate the constraints and cause unsoundness.
3. In propagate_blocked_cubes, we apply similar reasoning to the second case with regards to propagating finite frame blocked cubes to the infinite frame.

Asserting Constraints at TO_STEP

We first assert that asserting constraints at TO_STEP is UNSOUND in get_bad_cube. To do this, consider the following counterexample:

Suppose we have the circuit

module Counter(input clk);
// Counter register
reg [1:0] count = 2'd0;

// Main logic
always @(posedge clk) begin
  count <= count + 2'd1;
end

// Formal assertions
always @(*) begin
  // Constraint
  assume(count != 2'd2);
  
  // Safety property
  assert(count != 2'd1);
end
endmodule

In this case, $\mathbf{R}_0$ trivially satisfies the safety property. However, at $\mathbf{R}_1$, a concrete counterexample could simply be count == 2'd1. However, since $\mathbf{T}$ is permanently asserted and we constrain the next state to be count != 2'd2, the solver would not find this true counterexample. Therefore, PDR would falsely prove the safety property here.

However, we assert that asserting constraints at TO_STEP is sound for the other cases:

1. All calls to rel_ind are either made on blocked cubes in the frame trace (which must satisfy the invariant) or extracted models from previous rel_ind calls must satisfy constraints (by construction).
2. Similar reasoning as the first case, but with the propagation of finite frame blocked cubes to the infinite frame.

Tests

All regression tests pass. Some tests (Quiz1.btor, Quiz2.unsat.btor, Quiz4.unsat.btor) have been skipped since they hang when run. This is probably due to PDR trying to individually block concrete values of a 16-bit register, which leads to many SMT queries that slow down execution. The most important fix for this issue should be blocked cube generalization.

[ekiwi]

@michael-zhang-lambda : can you use an activation literal for the NEXT step constraints?

[michael-zhang-lambda]

Changes

• Factored out next state constraints into activation literal field in BasePdr (similar to init frame)
• Refactored rel_ind and propagate_blocked_cubes to use the new activation literal
• Explicitly disable the activation literal in get_bad_cube to prevent unneeded search of state space