In reply to ben@SystemVerilog.us:
You description regarding to the requirement is much clear, especially clarify sc_clk is a gated version of clk by scan_en.
The assertion is also implemented well, I read it and think maybe update is needed as below:
- change clock event from @(posedge clk) to @(negedge clk). Assertion evaluation uses sampled values (pre-clock values), so negedge clk will get sc_clk sampled to be 1 and posedge clk will sample sc_clk to be low.
- add scan_en to the disable condition to disable check in case scan_en asserts to bring up sc_clk running again.
- next cycle implication |=> change to |-> same cycle implication
ap_scan: assert property(@(posedge clk) disable iff (reset); // 50mhz
$fell(scan_en) |=> sc_clk[*N] ##1 !sc_clk);
->
ap_scan: assert property(@(negedge clk) disable iff (reset||scan_en); // 50mhz
$fell(scan_en) |-> sc_clk[*N] ##1 !sc_clk);