Revert "dcache: Allow writing during write_pending"

[stffrdhrn]

This reverts commit 040a89fa0f7e0c2fdbc09ee6a343e6f05c65204e.

I bisected to this commit causing linux instability.

After reverting linux is stable again, however our or1k-mmu regression test now fails again.

Issue: #146

[stffrdhrn]

This fixes linux stability but formal verifaction now fails.

If fails because spr_ack_o can now be asserted after reset (invalidate_ack is always high in IDLE state) and we have a formal rule saying that we should never have more acks then requests.

SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: starting process "cd mor1kx_dcache_prv; yosys-smtbmc --presat --unroll --noprogress -t 25  --appen
ogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: starting process "cd mor1kx_dcache_prv; yosys-smtbmc --presat --unroll -i --noprogress -t 25  --a
d --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Solver: yices
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Solver: yices
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Trying induction in step 25..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Trying induction in step 24..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Trying induction in step 23..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assumptions in step 2..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Checking assertions in step 2..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Trying induction in step 22..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  BMC failed!
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.way_memories[0].way_data_ram.f_addr (mor1kx_simple_
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.way_memories[1].way_data_ram.f_addr (mor1kx_simple_
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.f_write_data (mor1kx_dcache.v:0.0-0.0): 2147483648
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.f_write_addr (mor1kx_dcache.v:0.0-0.0): 0
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.f_refill_addr (mor1kx_dcache.v:0.0-0.0): 0
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Value for anyconst mor1kx_dcache.f_refill_data (mor1kx_dcache.v:0.0-0.0): 0
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Assert failed in mor1kx_dcache.u_f_icache_slave: fspr_slave.v:58.24-59.37
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: ##   0:00:00  Trying induction in step 21..
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: ##   0:00:00  Status: failed
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.basecase: finished (returncode=1)
SBY 12:51:17 [mor1kx_dcache_prv] engine_0: Status returned by engine for basecase: FAIL
SBY 12:51:17 [mor1kx_dcache_prv] engine_0.induction: terminating process

Trace:

[stffrdhrn]

Hello, This is a pretty big change to fix the dcache issue. Most of this is documentation and fixing formal to be able to detect the issue before I actually fixed it. IN the LSU I removed some of the AUTOINST directive stuff used by emacs verilog as I dont use it. I hope that is OK.

The actual fix is in cebcd66b09c32ab10f1378b23cb304cc2ed58502

[stffrdhrn]

Thanks @bandvig , I will just merge it as it does seem to fix this issue. The main thing I think people would have concern with was the size of the change and me re-arranging some of the instantiation blocks. But, as not objections I will merge.