[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=316

--- Comment #24 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #23)
> (In reply to Luke Kenneth Casson Leighton from comment #20)
> 
> > Cole that's a really good template to start from.
> > 
> > (*sotto voice to michael*: i tend to just set mb = dut.mb as a temp
> >  python variable, and do "yield dut.o" rather than spend the time
> >  setting up copies of things that you can get at directly anyway).
> 
> I think I did this because when I was first starting nmigen there was a bug
> where the vcd dump didn't show the top level signals unless you did this.

ah HA!  i half-expected that might be why.

> I haven't seen it happen in a while so maybe it's fixed...?

it's not.  if you can see if there's a bugreport raised for nmigen, and
cross-reference the discussion here, that would be really handy.

> > this is why we want to do Formal Proofs, because one Formal unit test,
> > if written correctly, covers *everything*.
> 
> I haven't closely examined bpermd, but for maskgen I didn't bother writing a
> proof because it was easy and quick enough to exhaustively test the input
> space. I suspect you won't be able to do that for bpermd though.

yehyeh.  Cole: maskgen is... 8-bit wide? so running 2x for-loops @ 256 x 256
cycles, for such a small amount of code that's perfectly feasible.
however if it was say 64-bit wide? (as is the case for bpermd) - that's
flat-out
impractical.  we can't possibly run 2^64 times 2^64 clock cycles to cover
all permutations for inputs.

hence: formal proofs

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