[libre-riscv-dev] [Bug 165] New: Formally verify the FPCMP (FEQ, FLE, FLT) module

[Michael Nolan]

Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:

>
> wanna give it a shot?

So it does work, sort of. If I set the crossbar RHS to 1 and set the gt
inputs to 0, it gives the correct output for the active outputs, however
the outputs that should get set to a constant 0 get set to a constant 1
instead (which makes sense because that's part of what the crossbar is
for. I'd need to add a little extra logic (xor with (crossbar_rhs &
~gates[i])) to handle that

See https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part_cmp/experiments/formal/proof_gt.py;h=691d831707bf54d45451f76b34b0010547093ff7;hb=1750521d08baf5f8551bf3286647ed4777357500 and https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part_cmp/experiments/gt_combiner.py;h=7fd4da2a089b07a01c80b4a46a281eabeb016bc6;hb=1750521d08baf5f8551bf3286647ed4777357500

--Michael