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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #20 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Michael Nolan from comment #18)

> ROFL, I got the idea of using Arrays from your conversations yesterday.

:)

> I'd be happy to help with formal proofs when you're ready.

really appreciated.  (In reply to Michael Nolan from comment #19)


> For writing unit tests, take a look at
> https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/
> test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937;
> hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place

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

so, Cole, note two things:

1) the establishment of the "DUT" - Device Under Test.  the "yield"
   statements to set the inputs, and the additional "yield" statement
   to obtain the output

2) the use of a **PYTHON** function - not a nmigen function - which
   computes the expected result.  this function - MASK() in this
   example by Michael - is given the EXACT SAME INPUT as was handed
   to the hardware.

thus you have an "expected" result (done in python) and a "hardware-simulated"
result.

if those two do not match, throw a python unittest assert.

simple.

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

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