[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 #6 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Jacob Lifshay from comment #5)
> (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),

yes, agreed, on an FPGA that makes sense.

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

the exercise here is to introduce the new team to nmigen-based formal
verification, warts and all.

plus, i have put some thought for several months into how to do that using the
existing PriorityPicker, and wouldn't know where to start with the i & -i one.

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