[libre-riscv-dev] [Bug 151] introductory formal verification tutorial using the PriorityPicker

[bugzilla-daemon at libre-riscv.org]

http://bugs.libre-riscv.org/show_bug.cgi?id=151

--- Comment #5 from Jacob Lifshay <programmerjake at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #4)
> (In reply to Jacob Lifshay from comment #3)
> 
> > Related: priority picker where LSB has highest priority can be implemented
> > with:
> > 
> > i = Signal(32)
> > o = Signal(32)
> > 
> > m.d.comb += o.eq(i & -i)
> 
> nice!  that... hmmm, i wonder if that property can be exploited
> mathematically for the formal proof?
> 
> hardware-wise it would be nooowhere near as efficient as what Seymour Cray
> came up with (a O(N) cascade of NAND and NOT gates) so it's not something we
> want to deploy in production.  the proofs don't get put into actual silicon,
> though.

I'd actually argue that (i & -i) is likely to be more efficient (especially on
FPGAs), since synthesizers often have special handling for carry chains that
can avoid the need for 32-input gates or 32-gate latency (for 32-input priority
picker). It's also much easier to write/read/verify.

-- 
You are receiving this mail because:
You are on the CC list for the bug.