Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
22 check-ins that include changes to files matching 'cores/roma/*'
|
2018-10-22
| ||
| 02:09 | Import roma core from formal branch check-in: f6bd84d868 user: kc5tja tags: trunk | |
| 01:57 | Formal verification has proven itself as a viable development method. Merging into trunk. check-in: af53196bd7 user: kc5tja tags: trunk | |
|
2018-08-30
| ||
| 18:11 | Per ZipCPU's suggestion, I didn't need the initial block if I qualified some of my assertions more thoroughly. check-in: d5debe2752 user: kc5tja tags: formal | |
| 04:57 | ROMA: Formal verification of TileLink bus seems to be complete. check-in: b014c7b07f user: kc5tja tags: formal | |
|
2018-08-29
| ||
| 18:44 | WIP ROMA: Qualify A-channel transaction by comparing opcode. Verify that o_d_valid should be negated for as long as we lack a read result. Remove reg qualifier from all signals we "assign" to. Generate o_a_ready based on state of bits_so_far. Passes bmc; fails to prove inductively. Cause is o_d_valid && i_d_ready true while not engaged in an actual transaction. Cannot figure out how to tell prover that this is an impossible condition. check-in: 2f8acc4498 user: kc5tja tags: formal | |
| 06:57 | Enforce proper handling of o_a_ready check-in: 2da2614d5c user: kc5tja tags: formal | |
| 05:38 | First set of formal properties for ROMA core check-in: f1b71290ae user: kc5tja tags: formal | |
| 00:59 | Attempt to add ROMA verification properties on my own check-in: e19f2d7e5c user: kc5tja tags: trunk | |
|
2018-08-25
| ||
| 02:34 | ROMA: Fix data alignment bug. check-in: 1d81dbc235 user: kc5tja tags: trunk | |
|
2018-08-24
| ||
| 05:33 | WIP: FPGA programs OK; flash programs OK; DMAC seems to be working OK; ROMA seems to be working OK; however, data read back is always $FF on the LEDs. This suggests either the CPLD is interfering with my communications somehow, OR, I'm botching the SPI protocol somehow. Unsure which yet. More research is needed. check-in: ed4beeb135 user: kc5tja tags: trunk | |
| 00:59 | Refactor common definitions into shared headers check-in: 3444a010e1 user: kc5tja tags: trunk | |
|
2018-08-23
| ||
| 23:51 | ROMA: Support back-to-back transactions check-in: d3867aab51 user: kc5tja tags: trunk | |
| 23:29 | ROMA: Forgot to drive the CLK output check-in: f7064f5df0 user: kc5tja tags: trunk | |
| 23:25 | ROMA: I think it is finished. check-in: 2bccfe58ef user: kc5tja tags: trunk | |
| 23:10 | Confirm proper data output check-in: 85e9538b39 user: kc5tja tags: trunk | |
| 22:48 | ROMA: Proper D-channel handoff check-in: 1181e5b5d7 user: kc5tja tags: trunk | |
| 22:43 | Negate SPI Flash CS after 64 data bits read check-in: e4574d60c9 user: kc5tja tags: trunk | |
| 07:36 | ROMA: Send 21-bit dword-aligned address too check-in: a777854d78 user: kc5tja tags: trunk | |
| 07:20 | ROMA: Send command byte on read request check-in: cffa191f94 user: kc5tja tags: trunk | |
| 07:00 | ROMA: Recognize read request check-in: 0892ceaf82 user: kc5tja tags: trunk | |
| 06:02 | ROMA: Slave A-channel first commit check-in: 768fc08020 user: kc5tja tags: trunk | |
| 05:48 | First commit for ROMA core. check-in: e4318b055e user: kc5tja tags: trunk | |