Chipress

From Black Box to Behavioral Model, to VIP

We discussed black boxing, but black boxing assumes a logic X at the output ports. One can further add assume properties at black box module outputs, to constrain their behavior.

Designers can wrap these assume properties into a separate module, and this module has the exact same interface as the original RTL module. Now, we have a behavioral model for the black boxed module. During the design analyzing phase, instead of instructing the FV tool to analyze the actual RTL file, we ask the tool to analyze this behavioral model.

Since the behavioral model does not implement the complex datapath and pipeline, it helps with FV convergence. For example, a complex data processing module with Valid-Ready interface with multiple pipeline stages, may have its behavioral model as simple as a few assume properties describing the Valid-Ready interface behavior, and a few more assume properties constraining the legal output data values.

Going one step further, we can even create a VIP (Verification IP) for the black boxed modules. On top of the behavioral model, we can add assert properties to check the input data values within ranges, and to make sure the Valid-Ready interface behavior is compliant with spec.

We can create a “Verification IP” for the black box module. The “Verification IP” will have the same interface as the original RTL module, but instead of implementing the complex datapath and pipeline, it simply includes a set of properties to constrain its behavior.

It is worth pointing out that it is not always straightforward to create a behavioral model / VIP. The more complex a design is, the more design knowledge required and more difficult to create a behavioral model / VIP.

SRAM Abstraction

Not all FV flows require full SRAM storage. For example, in clock gating FV, all we want to prove is, when SRAM read / write enable is high, the SRAM gets toggling clock. Thus a simple SRAM abstract model can be implemented as this:

input re, we;
input [$clog2(DEPTH)-1:0] raddr, waddr;
input [DWIDTH-1:0] wdata;

output logic [DWIDTH-1:0] rdata;

logic [$clog2(DEPTH)-1:0] raddr_fv, waddr_fv;
logic [DWIDTH-1:0] rdata_fv, wdata_fv;

always_ff @(posedge clk)
    if (~resetn)
        raddr_fv <= ‘x;
    else if (re)
        raddr_fv <= raddr;

always_ff @(posedge clk)
    if (~resetn)
        rdata_fv <= ‘x
    else if (re | we)
        rdata_fv <= ‘x;

assign rdata = rdata_fv;

always_ff @(posedge clk)
    if (~resetn) begin
        waddr_fv <= ‘x;
        wdata_fv <= ‘x
    end else if (we) begin
        waddr_fv <= waddr;
        wdata_fv <= wdata;
    end

Configuration Register Abstraction

Sometimes we may want to constrain the configuration registers to a certain value, to limit the FV space. We can first abstract the initial values of the configuration registers by doing:

abstract -init_value top.reg_block.block_enable_reg

“abstract -init_value” command converts a known initial value on the output of a register into an undefined X value, which permits all possible initial values to be explored.

Next, we use assume properties to constrain the configuration register value:

assume property (@(posedge clk) 1 |-> top.reg_block.block_enable_reg == ‘0)

Counter Abstraction

Counters contribute a sizable amount of FV complexity: the larger the counter can reach, the harder for FV tools to exhaust all possibilities and achieve full proof.

Jasper Gold provides a way to automatically abstract counters to reduce their counting impact on proof complexity.

# return a list of counter candidates in the cone of influence of the properties
# and list their “interesting” values
abstract -counter -find

# Apply stopat along with minimum assumptions required for correctness
# e.g., counter always increments, but may increment by more than 1 per cycle
abstract -counter counter_reg

Proofs associated with the counter can typically be converging quickly, using the counter abstraction offered by Jasper Gold.

Note, counter abstraction allows the tool to skip counting values between critical values, as long as it keeps the assumption of incrementing values. It is still a robust methodology, since it is based on stopat + assumptions, and the assumptions are under-constraining the design.

One can always add stopat + assumptions on the counters. However, the better practice is to let the tool handle the abstraction, and the tool can figure out the critical values more structurally.

Design Reduction vs Black Boxing vs Abstraction

The following table shows a comparison among design reduction,  black boxing and abstraction.