[libre-riscv-dev] [Bug 173] dynamic partitioned "shift"

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=173

--- Comment #39 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #38)
> I'm guessing this will need to be pipelined at some point, would you like me
> to give that a try?

well, before that, we need to see if it's actually needed, by checking the
longest path (longest chain).

you rarely hear of processors breaking down a 64 bit shift into pipelines.
looking at RocketChip's ALU, that's gone to 1.5ghz in 45nm and they've
not done pipelining.  and, because of the breakdown into smaller sections
we might actually have *reduced* latency.

btw scalar formal proof is failing, here
python3 ieee754/part_shift/formal/proof_shift_scalar.py 
SBY 21:35:29 [proof_shift_scalar_shift] base: starting process "cd
proof_shift_scalar_shift/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 21:35:29 [proof_shift_scalar_shift] base: Warning: Driver-driver conflict
for $16 [15] between cell $17.Y and constant 1'0 in dut: Resolved using
constant.
SBY 21:35:29 [proof_shift_scalar_shift] base: Warning: Driver-driver conflict
for $16 [14] between cell $17.Y and constant 1'0 in dut: Resolved using
constant.
...
...
SBY 21:35:29 [proof_shift_scalar_shift] engine_0: ##   0:00:00  Value for
anyconst in top (ieee754/part_shift/formal/proof_shift_scalar.py:50): 0
SBY 21:35:29 [proof_shift_scalar_shift] engine_0: ##   0:00:00  Value for
anyconst in top (ieee754/part_shift/formal/proof_shift_scalar.py:51): 0
SBY 21:35:29 [proof_shift_scalar_shift] engine_0: ##   0:00:00  Value for
anyconst in top (ieee754/part_shift/formal/proof_shift_scalar.py:49): 32768
SBY 21:35:29 [proof_shift_scalar_shift] engine_0: ##   0:00:00  Assert failed
in top: ieee754/part_shift/formal/proof_shift_scalar.py:67

-- 
You are receiving this mail because:
You are on the CC list for the bug.