mor1kx
mor1kx copied to clipboard
openrisc
mor1kx - an OpenRISC 1000 processor IP core
This can be tested by setting the cache with in `mor1k_dcache.sby` and running `make -C bench/formal mor1kx_dcache`. It seems the generator logic does not work with smaller cache widths.
The `mor1kx_lsu_cappuccino` write ack logic depends on writes to the store buffer to be acked. If we disable the store buffer acks are not returned and the system does not...
When fixing #146 I rewrote formal properties to do a better job of simulating real Load/Store and Dcache transactions. I was able to track down the bug and fix it....
If I set the DBUS_WB_TYPE parameter to "B3_READ_BURSTING", then the CPU locks up when attempting the first data access. It seems that the dbwm_we_o output gets asserted, and a valid...
The OpenRISC specification requires that the EEAR register be accessible from the supervisor mode but the mor1kx implementation does not have the option to write to EEAR with the mtspr...
The OpenRISC specification requires that the EPCR register be accessible only from supervisor mode. Bug location: rtl/verilog/mor1kx_ctrl_cappuccino.v Triggering input: #include int main() { // enter user mode : asm volatile...
The carry flag value is not as expected for some cases. For instance, with the following trigger input, since r1 > r3, carry flag should be reset, but it is...
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...
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...
**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...