Fixes for debug asserts for 40x
Created by: silabs-robin
After a lot of progress on the design side of 40x, a few assertions were in need of updating.
Added "wb_valid" qualification to both "is_trigger_match" and "is_ebreak". Took heed of the fact that exceptions can now count as single stepping (e.g. in "debug_cause_pri"). Split "a_debug_mode_pc" in three[0]. Some signals were renamed more logically. NMI was taken into acount in the assertions that already exclude interrupts. "mcause_q" was widened to support new exception codes. NMI was also taken into acount for setting "pc_at_dbg_req". Added two assertions for "dm_halt_addr_i".
The assertions pass in formal[0] and ci_check. Confered with @silabs-oysteink
on CEXes along the way. (@silabs-oysteink
could you please review this PR?)
[0] Note, "a_debug_mode_pc_dpc" really struggles to converge in formal. The helper logic faning into it might need to be rewritten if it is possible? Should we accept a bounded proof? Must it be fixed as part of this PR?