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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #22 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #20)
> (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*.

Ah, thank you very much for these additional details Luke. Everything the both
of you (and Yehowshua) have said is proving critical to my ability to quickly
(or slowly...) get going with the various required aspects of our HDL_workflow.
Once I have finished this first small 'project'/assignment, I'd like to pause
for a few hours and update the documentation of the HDL_workflow with the
things I learned while scripting it, as well as all that I've learned in this
assignment. Some of this exists elsewhere on the wiki, however, most of the
getting started with nmigen stuff I've learned in the past two days does not
(as far as I am aware) and I believe this will be valuable to new members. But
right now I have a prior engagement I must attend to, so I'll attempt an
initial unit test tomorrow :)

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