A assertion for reset where the reset is active low , the reset should dessert asynchronously , and after two clock cycle it should assert synchronously .
I tried in this way
property reset_sync(bit clk ,rst);
(@(negedge rst) 1’b1 |-> (@(posedge clk) ##1 $stable(rst)[*2] ##1 @(posedge clk) !($stable(rst))));
endproperty
@ben2 @dave_59 can you help me with this ,for the above assertion it is failing in some cases, can you correct it as per the requirement
I had a hard time understanding your requirements. SO I passed what you wrote to perplexity.ai and it gave me this:
This type of reset signal has two key characteristics:
Asynchronous Deassertion: The reset is deactivated (deasserted) immediately when the reset input changes,
regardless of the clock state. This means the system can come out of reset at any time,
not necessarily aligned with a clock edge1.Synchronous Assertion after Two Clock Cycles: When the reset needs to be activated (asserted),
it waits for two complete clock cycles before actually asserting.
This ensures that the reset assertion is synchronized with the clock, reducing the risk of metastability
So, I I understand your requirements, whenever rst_n goes to 1, it must go low in 2 cycles.
assert property (@(posedge rst_n) 1’b1 ##0
@(posedge clk) rst_n [*2] ##1 rst_n==0);