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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #23 from Michael Nolan <mtnolan2640 at gmail.com> ---
(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. I
haven't seen it happen in a while so maybe it's fixed...?

> except, it is necessary to write a *lot* of these, catching and testing
> different aspects of the hardware.
> 
> 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.

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