Let say I have three signal : input clk_in , input rst_b, output clk_out. How can I get an assertion to check if clk_out is toggling only after 2 clk_in cycles after the rising edge of rst_b. The assertion should fails if the clk_out is delayed more/less than 2 cycles and the assertion should also fail when clk_out stop toggle before rst_b goes 0. When rst_b ==0, the clk_out should be 0 too.
I have tried this:
property_assert: assert property(@(posedge clk_in or negedge clk_in) $rose(rst_b) |-> ((##[0:3] clk_out == 0) and (##4 (clk_out==clk_in) throughout rst_b)));
From the way you described the requirements, it sounds like clk_out is a gated version of clk_in where gate is the enabling gate control.
When the gate s in the enabling mode, clk_out is exactly clk_in. Thus, sampling clk_out with posedge clk_in does not really sample the value clk_out after the edge of clk_in.
I fell more comfortable creating a delayed version clk_in by 1ns, and use that as the sampling clock for clk_out. I also feel more comfortable writing multiple assertions, and using tasks for complex assertions (see my paper on this topic at SVA Alternative for Complex Assertions Verification Horizons - March 2018 Issue | Verification Academy
module top;
timeunit 1ns; timeprecision 100ps;
logic clk_in=0, clk_ind1, clk_out, gate;
default clocking @(posedge clk_in);
endclocking
initial forever #10 clk_in=!clk_in;
assign #1 clk_ind1= clk_in;
// check if clk_out is toggling only after 2 clk_in cycles after the rising edge of gate.
// The assertion should fails if the clk_out is delayed more/less than 2 cycles
// and the assertion should also fail when clk_out stop toggle before gate
// goes 0. When rst_b ==0, the clk_out should be 0 too.
// Sampled at all cycles
ap: assert property(@ (posedge clk_ind1) $fell(gate) |-> clk_out==1'b0);
// Used to compare clk_in and clk_out when gated ON.
task automatic t_gated_clks();
while(gate!=0)
@(posedge clk_ind1 or negedge clk_ind1)
assert(clk_out==clk_in);
endtask
// Fire the gated comparison after rose(rose).
ap_rose_gate: assert property( @ (posedge clk_in)
$rose(gate) ##2 1'b1 |-> (1, t_gated_clks()) );
always begin // check 2 zero outs for 2 clk periods
wait($rose(gate));
// fire once
ap_at_rose_gate: assert property(@(posedge clk_in)
@(posedge clk_ind1) clk_out == 0 [*2]);
ap_at_rose_gate2: assert property(@(posedge clk_in)
@(negedge clk_ind1) clk_out == 0 [*2]);
end
// Code was not tested, but this should help you with the concepts.
