a simple introduction to nmigen formal verification is needed. the PriorityPicker is to be used to do that.
this is the code that needs a formal proof added: https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/nmutil/picker.py
example code which is extremely good and has comprehensively well-written formal mathematical proofs: http://chiselapp.com/user/kc5tja/repository/kestrel-3/dir?ci=f84f6c3126376ab2&name=cores/cpu here is a sophisticated one involving "things that occur in the past": http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/217f2862441726f5 see UpCounterCSRFormal. this one uses "Past" to check (assert) that data which comes "into" the hardware comes *out* of the hardware at the required number of "ticks" (clock cycles) in the future. actually, by comparing "right now" to "Past()".
(In reply to Luke Kenneth Casson Leighton from comment #1) > this is the code that needs a formal proof added: > https://git.libre-riscv.org/?p=ieee754fpu.git;a=blob;f=src/nmutil/picker.py 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) See: https://stackoverflow.com/a/12250963
(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. here's the installation process: https://symbiyosys.readthedocs.io/en/latest/ you'll each need to go through that, and also install nmigen. i *strongly* recommend using debian - or last resort ubuntu. if you try windows or macosx, you will get into a world of pain. the critical solvers to have are yices3 and z3. if you really really want to you could add super_prove, amy and boolector. the tutorial there ("a simple BMC example") is a good idea to try out as a by-rote test of symbiyosis. once you've each confirmed that working we can move to nmigen.
(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.
(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.
actually, you know what? i really like the idea of *also* doing a priority picker with that i & -i in it, and comparing the two. i think it would be a good idea to leave it to bartok, maciej and juliusz to write, though :)
hmmm, actually... by writing both, it may be possible to write a formal proof that shows equivalence between the two. something like: p1.i.eq(p2.i) Assert(p2.o == p1.o) where p2.i is the input to the module. basically the solver would know, because p2.i is the input, to generate a test of all possible values for p2.i and confirm that the outputs for both p2 and p1 are identical *for* all those inputs. exactly how the SAT solvers do that is beyond my knowledge, i haven't investigated: i am treating them as a "black box" at the moment.
https://libre-riscv.org/HDL_workflow/ contains various useful links and instructions on getting set up