[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 #40 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #39)



> 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.

Both proofs work on my machine on commit d635235. I'm using yosys 0.9-1706
(b9dfdbbf).

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