[Libre-soc-bugs] [Bug 418] SPR pipeline formal correctness proof needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)
> commit 769a8d5444f46cd093ff03645658198eaa8bd76d
> Author: Samuel A. Falvo II <kc5tja at arrl.net>
> Date:   Tue Jul 14 12:17:45 2020 -0700
> 
>     SPR: FV that should fail currently passes
>     
>     WIP.  Cannot figure out why this is not failing.  Code review requested.

commit ead389c3edc78ec2af354a3f713788ac8c0ce6a2 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl at lkcl.net>
Date:   Tue Jul 14 20:59:59 2020 +0100

    cookie-cut setup from alu proof_main_stage.py

Michael pre-established a pattern for verifying the input fields and in
particular for verifying that the ctx object fields are correctly
copied by the pipeline from input to output.

i've cookie-cut this code over.  this takes care of verifying this (one)
line of code at the end of fu/spr/main_stage.py:

        comb += self.o.ctx.eq(self.i.ctx)

actually.. it doesn't.  other ctx contents aren't verified.  it only
verifies ctx.op, oh well.  will raise a separate bugreport about that.



regarding unit tests:

    #don't worry about it - tests are run manually anyway.  fail is fine.
    #@skipUnless(getenv("FORMAL_SPR"), "Exercise SPR formal tests [WIP]")
    def test_formal(self):

commenting out / disabling unit tests "just because they fail or are
otherwise incomplete" is generally bad practice.  the python unittest
module is *specifically* designed to catch success/fail exceptions and
provide reporting.

disabling a test, there has to be a *really* good reason such as "the unit
test actively interferes with the completion or running of other tests",
such as failing to complete (at all), taking several days to complete,
or destroying or tampering with filesystems in ways that prevent other
tests from running.

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