Harshitha

SPR property fails when debug unit is enabled

2

SPR read and write requests are mutually exclusive. Both spr_read_access and spr_write_acess can’t be high at the same time. When the Debug unit is enabled, this property fails. **Assertion** (Check...

spr_ack is high when there is no mtspr/mfspr instructions

2

In the control module, signal `spr_access` is driven by the `spr_group` which is dependent on the address computed in the execution stage i.e., `ctrl_alu_result_i`. When we don’t have spr instructions...

Data bus Wishbone Interface Formal Check fails

2

**Properties that failed:** 1. The direction of the write enable shouldn't change within a series of strobe/requests. 2. Within any given bus cycle, the direction may *only* change when there...

onehot of SPR acknowledgments fail

2

**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...

Erroneous ICache hits impact performance counters

7

Icache updates the LRU access variable only if cache hits occur in the read state. There may be cache hits that occur in the state refill or invalidate. CPU gets...