In reply to E_R_R:
I read the requirements differently. “signal should be treated as a STATIC input.” says that this is an input that is hardwired, possibly after the board is built with a jumper to provide options. If you want to include rst you can use the following code that can be used in formal:
/* signal should be treated as a STATIC input. If the value changes during operation, data corruption will occur.
It is also mentioned that signal is independent of the clocks and thus asynchronous.
From this specification I gathered that the signal is only able to legally change state
on an edge of the system reset. */
bit sig_support;
always_comb begin
if(rst) sig_support=sig;
am_sig: assert #0 (!rst && sig==sig_support || rst);
end
Ben