[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 18:11:06 GMT 2020

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

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

actually a 3 2 CSA with one input set to zero, probably... yes.

it might be possible to eliminate the XORs by inverting pN as the input,
swapping the crossbar, or just heck outputting the carry bit into the next

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

oo i like it.

> > 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;
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev at lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

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

More information about the libre-riscv-dev mailing list