onehot of SPR acknowledgments fail

[Harshitha172000]

Property: No two spr groups can acknowledge at the same time.

Assertion:

https://github.com/openrisc/mor1kx/blob/master/bench/formal/fspr_master.v#L66#L70

always @(posedge clk)
      if (f_past_valid)
         assert ($onehot0({spr_bus_ack_dc_i, spr_bus_ack_ic_i,
                 spr_bus_ack_dmmu_i, spr_bus_ack_immu_i}));

Back-to-back spr requests may delay the fall of spr acknowledgment. Meanwhile, a new spr request would have been acknowledged. Here, we can see spr_bus_ack_ic_i and spr_bus_ack_dc_i signals are high at the same time.

Trace:

[stffrdhrn]

can you put a link to the code, or mention the module where this is happening?

[Harshitha172000]

It's tested in the spr master interface, referring to mor1kx_cpu_cappuccino.v module.