Black Boxes and Cut Points

Sometimes the logic in the cone of a property is too complex for the tool, or not available at all: an analog model, a memory macro, encrypted third-party IP. A cut point replaces a signal with a free value that the tool may choose in every cycle; a black box does the same for every output of a module. The property is then checked for any value the cut signal could take, which is more than the real design can produce. This article explains when that is sound, shows a false failure it causes, and how to constrain a cut to fix it.

9 min read | Intermediate

What You'll Learn

• Explain cut points and black boxes and how they shrink the cone of influence
• Explain why a pass with a cut is valid for the real design
• Recognize a false failure caused by a cut
• Constrain a cut with assumptions that the cut-out logic guarantees

Cutting Logic Out

A cut point turns a signal into an input of the formal problem. Everything that only drives that signal leaves the cone of influence. A black box cuts every output of a submodule at once, so the tool never looks inside it.

In SymbiYosys the simplest way is a formal-only declaration with the Yosys attribute (* anyseq *), which gives a value the tool may choose freely in every cycle. A `define switches between the real logic and the cut:

`ifdef CUT_MULT
  // cut point: the product is a free value, chosen by the tool in every cycle
  (* anyseq *) reg [2*W-1:0] prod;
`else
  wire [2*W-1:0] prod = a * b;
`endif

Commercial tools offer commands for the same, typically to declare a signal a cut point or a module a black box from the tool script, without editing the RTL.

Why a Pass Is Still Valid

With the cut, the tool checks the property for every possible value of the cut signal in every cycle. The real logic produces only some of those values. So if the property holds for all of them, it holds for the real ones too. A pass with a cut is a pass for the real design.

A failure is different. The tool may have chosen a value that the real logic can never produce. Every failure with a cut must be checked: is the cut value possible?

The Design: a Multiply-Accumulate Unit

module mac_ctl #(parameter W = 12) (input clk, input rst, input go, input [W-1:0] a, input [W-1:0] b,
                                     output reg [2*W-1:0] acc, output reg ovf, output reg [3:0] ops);
  wire [2*W-1:0] prod = a * b;                     // replaced by the cut when CUT_MULT is defined
  wire [2*W:0]   sum  = {1'b0, acc} + {1'b0, prod};
  always @(posedge clk)
    if (rst) begin
      acc <= 0; ovf <= 1'b0; ops <= 4'd0;
    end else if (go) begin
      acc <= sum[2*W-1:0];
      if (sum[2*W]) ovf <= 1'b1;
      if (ops != 4'd15) ops <= ops + 4'd1;
    end
endmodule

Two properties about the accumulation logic:

// a zero operand leaves the accumulator unchanged
a_zero: assert property (@(posedge clk) disable iff (rst) go && (a == 0 || b == 0) |=> $stable(acc));
// ovf never rises without a carry out of the accumulator
a_ovf:  assert property (@(posedge clk) disable iff (rst) $rose(ovf) |-> $past(go && sum[2*W]));

A False Failure

Without the cut, both properties pass. With the cut, a_ovf still passes, as it should: it holds for any product. But a_zero fails at step 3. The trace has a = 0, b = 0, and a product of 1. The accumulator goes from 0 to 1.

That product is impossible: zero times anything is zero. The cut allowed it because a free value knows nothing about multiplication. The property a_zero depends on a fact about the multiplier, so cutting the multiplier removed the fact.

Constraining the Cut

The fix is to add back exactly the facts the property needs, as assumptions on the cut signal:

// constrain the cut with what the multiplier guarantees: a zero operand gives zero
always @(*) if (a == 0 || b == 0) assume (prod == 0);

Now a_zero passes again. The assumption is a promise of the cut-out logic, and like every assumption it must be true: here, a fact about multiplication. When the cut-out block is a real module, its assumptions should be proven as assertions on that module, the assume-guarantee pattern.

When to Cut

• The logic behind a signal is too hard for the solver: wide arithmetic compared with arithmetic, cryptography, large lookup tables.
• The logic is not available for formal: analog models, memory macros, encrypted IP. These are black boxes by necessity.
• You want the result to hold for any behavior of a neighbor, for example a property of a controller that must work whatever the datapath computes.

In the MAC above, the solver handled the 16-bit multiplier without trouble, because neither property compares it with another multiplication. That is common with modern solvers: an unrelated multiplier in the cone is often cheap. Cut points pay off when the cut logic is really hard, or not there at all.

Running It in ChipVerify Lab

The example below is the MAC with both properties and the cut switch, with the cut off. Run it, then add `define CUT_MULT at the top of the file and run again to see the false failure. Then add the constraint.

Common Mistakes