In FPV, if an SVA uses a gated clock, it could have false failures. Take the following SVA for example:
// clk_gated does not toggle when block_busy == 0
assert property (@(posedge clk_gated) block_busy |=> $stable(config_regs));
“config_regs” can legally be changed when “block_busy” is low, during which the gated clock does not toggle and the SVA does not check its consequent “$stable(config_regs)”.
When the next time “block_busy” is high, the gated clock toggles again and the SVA expects “config_regs” to remain the same. Obviously, the SVA will fail.
To resolve the false failure, the most straightforward way is to hook up a free running clock to the SVA:
// clk is a free running clock
assert property (@(posedge clk) block_busy |=> $stable(config_regs));
Alternatively, designers can make sure the gated clock can toggle at least 1 cycle after “block_busy” changes from 1 to 0:
always_ff @(posedge clk)
if (~resetn)
block_busy_q <= ‘0;
else if (block_busy != block_busy_q)
block_busy_q <= block_busy;
// clk_gated toggles as long as clock_enable is high
assign clock_enable = block_busy | block_busy_q;
Both of the above solutions require some sort of hierarchical design changes in favor of FPV convergence. It is possible to resolve the false failure without changing RTL significantly.
First, designers can rewrite the SVA by defining and using a “virtual SVA clock”:
logic clk_sva;
assign clk_sva = clk_gated;
assert property (@(posedge clk_sva) block_busy |=> $stable(config_regs));
The “virtual SVA clock” will then be driven by a free running clock in FPV setup:
# define a free running clock
clock clk
# assuming the SVA locates in a module called “block_ctrl”
set block_inst_name [lindex [get_design_info -module block_ctrl -list instance -regexp] 0]
set block_sva_clk “${block_inst_name}.clk_sva”
# drive the free running clock to the virtual SVA clock
# use stopat command to specify an internal signal should be treated as a free input
# -env switch applies the stopat globally
stopat -env $block_sva_clk
clock clk $block_sva_clk
If there are multiple SVAs in multiple modules that require free running clock, designers can use a tcl list, and feed free running clock to all these SVAs in one shot, for example:
set clk_sva_list {}
foreach block_inst_name $block_inst_list {
set block_sva_clk “${block_inst_name}.clk_sva”
stopat -env $block_sva_clk
lappend clk_sva_list $block_sva_clk
}
clock clk $clk_sva_list
Chipress 
Leave a comment