Chipress

It is not always possible to achieve full proof in the SEC, but there are still a few things we can try for better SEC convergence.

We discussed a few techniques for FPV convergence, including design reduction, black boxing, and abstraction. They can all be applied to SEC as well. In addition, there are a few more techniques unique to SEC.

Apply Waiver

If a mapped point between SPEC and IMP designs is deemed not passing, one can apply waivers to it. For example, in clock gating FV, the clock input to a black box will not match. In SPEC design, that clock input will toggle every cycle, while in IMP design the clock input may be periodically gated.

# waive a signal
check_sec -waive -waive_signals {my_black_box.clk}

# waive a flop by disabling a mapping
check_sec -disable -mapping -spec “my_design.my_flop”

# waive a flop by unmapping it
check_sec -unmap -spec “my_design.my_flop”

One caveat is, use the waiver mechanism with caution, especially if the waiver is invoked with regular expressions. Use waiver with signals / flops hierarchies specified as explicitly as possible.

Conditional Remap

If a mapped point between SPEC and IMP designs only match under certain conditions, one can use the conditional remap mechanism. The commands below shows an example:

# first unmap a flop
check_sec -unmap -spec “my_design.my_flop”

# then remap the flop only when “enable” is 1
check_sec -map -spec “my_design.my_flop” -imp “my_design_imp.my_flop” -map_condition “my_design.enable”

Remove Assumptions

Counter intuitively, SEC works better with fewer or even no assumptions. FPV, on the contrary, works better with assumptions, since they reduce the design space that FV tools need to explore.

Note, however, assumption removal could introduce more noises, or false failures.

Disconnect Driving Logic

Disconnecting driving logic to selected nets and creating “free” nets help with Jasper convergence. Now, the FV tool has total freedom on how to drive the nets. The command below shows an example:

check_sec -map -spec “my_design.my_net” -imp “my_design_imp.my_net” -cut both

In the previous post, we showed that clock gating FV only “cuts” IMP design, not SPEC design. Introducing double-sided cutpoints (“-cut both”) prevents design input assumptions from propagating downstream, and one may need to deal with more false failures.