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

https://i.imgur.com/azx2hpQ.jpg

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

--Michae;