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

Luke Kenneth Casson Leighton lkcl at lkcl.net
Mon Feb 3 14:58:53 GMT 2020

On Monday, February 3, 2020, Michael Nolan <mtnolan2640 at gmail.com> wrote:

> Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:
> >
> > michael if you want something a bit challenging to do, could you see if
> you
> > can optimise the part_cmp eq.py code?
> In the truth table for partitioned EQ here
> https://libre-riscv.org/3d_gpu/architecture/dynamic_simd/eq/, whenever
> the partition gates are open, there are 0s in the table for some of the
> outputs. Do those actually need to be 0, or can they be X's?

i thought about this and the answer is i don't know.

on one hand they should definitely be 0s

on the other they should be the same as the LSB result at the start of each

X i do not feel is a good idea.

the answer will come naturally when implementing  Partitioned Mux, which is
where these eq tests etc all get used.

actually that is an important one to add to the TODO list.


crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68

More information about the libre-riscv-dev mailing list