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

[Luke Kenneth Casson Leighton]

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


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