Hello,
I am trying to model an alert mechanism where the alert status can be observed by watching the payload on an interface. The payload is 32-bits wide where each bit represents a separate alert. I am currently trying to model the de-assertion of each alert as follows:
When a particular register is written to with the value 0x8000_0000, for example, then the 31st alert (corresponding to bit 31) is cleared and the payload on the alert interface will go from 0x8000_0000 to 0x0000_0000.
I have written a property as such:
property fcs_alert_deassert_p(reg_push, alert_reg_addr, alert_clear, alert_status_bit);
@(posedge clk) $fell(alert_status_bit) |-> $past(reg_push && alert_clear && alert_reg_addr == 32'h40000080, 3);
endproperty
What I now have to do is assert this property 32 times, once for each bit. I am wondering if there is a way instead to assert this property just one time and somehow modify this property to check the de-assertion for all 32 bits.
Thank you,
Sid