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

Michael Nolan mtnolan2640 at gmail.com
Mon Feb 3 17:49:25 GMT 2020

Luke Kenneth Casson Leighton <lkcl at lkcl.net> writes:
>  muxes right, not adders.  ok.  errr not muxes, you're describing a
> crossbar.

Ah, I suspected there was a better name for that.

> ok so there are 3 inputs, the crossbar switcher and the outputs (2 in
> crossbars are around 20 to 30 gates iirc, quite a lot, surprising)

Oof, that's more than I thought. Though I think these would be somewhat
less since one input is hardwired to 0. I think two and gates and an
inverter would work here instead.

>> I don't have anything for gt/lt yet

My idea for partitioned gt looks pretty similar, with an AND gate and OR
gate cascaded instead of the single OR (or AND for the noninverted
circuit) in the partitioned eq circuit.


> i prefer in ikiwiki will upload later
(Happy to upload these to ikwiki, do I just add them to the wiki's git


More information about the libre-riscv-dev mailing list