Many hyperlinks are disabled.
Use anonymous login
to enable hyperlinks.
1 check-in using file cores/roma/rtl/verilog/roma.v version c319f1224b
|
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 | |