[libre-riscv-dev] [Bug 316] bperm TODO
bugzilla-daemon at libre-soc.org
bugzilla-daemon at libre-soc.org
Sun May 17 00:26:37 BST 2020
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.
More information about the libre-riscv-dev
mailing list