FV Interview Questions (V) – Dealing with Complexity by Black Boxing

Other than design reduction, black boxing is another effective approach to deal with FV complexity.

Black boxing can be done in design analyzing phase:

analyze … -bbox_m my_module

Or it can be done in design elaboration phase:

# black box a module
elaborate … -bbox_m my_module

# black box an instance under top module
elaborate … -bbox_i my_instance

By default, the outputs of a black-boxed module always produce a logic X, i.e., the tool ensures a “pessimistic” verification by allowing Xs to take all possible values. However, one can instruct the tool not to treat Xs as free variables:

# treat Xs as 0s
elaborate … -disable_x_handling

# treat Xs as 1s
elaborate … -disable_x_handling -x_value 1

“-disable_x_handling” option should be used with caution, since it may limit the FV space, and hide potential bugs.

In addition, Jasper Gold offers a few more options to black box arithmetic logic and large arrays:

# black box multipliers if the multiplication result exceeds the specified number of bits X
elaborate … [-bbox_mul X]

# black box divide operators if the dividend exceeds the specified number of bits X
elaborate … [-bbox_div X]

# black box modulus operators if the output size exceeds the specified number of bits X
# in operation a%b, the output size is defined as the size of the right operand, b
elaborate … [-bbox_mod X]

# black box power operators if the output size exceeds the specified number of bits X
# in operation a^b, the output size is the smaller of the size a, and the size of (a*(2^b))
elaborate … [-bbox_pow X]

# black box arrays if the size exceeds the specified number of bits X
# for SystemVerilog, black box 2D/3D packed flop array, and 1D/2D/D unpacked flop array
elaborate … [-bbox_a X]