Assertion to check signal will go high for one clk cycle after 1us of FSM state change. lets say FSM state value is 3.
Signal cannot go high within 1us of the state change. It can come anytime after that.
Assertion to check one clk cycle is like
$rose(a) => $fell (a);
But how to model 1us delay and trigger above property after that (report error if comes early), as time delay is not allowed in assertions.
Please advise. Thanks in advance.