[libre-riscv-dev] [Bug 353] New: formal proof of soc.regfile classes RegFile and RegFileArray needed

[libre-riscv-dev] [Bug 353] New: formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

            Bug ID: 353
           Summary: formal proof of soc.regfile classes RegFile and
                    RegFileArray needed
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: enhancement
          Priority: ---
         Component: Source Code
          Assignee: lkcl@lkcl.net
          Reporter: colepoirier@gmail.com
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Cole Poirier <colepoirier@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           Assignee|lkcl@lkcl.net               |colepoirier@gmail.com

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
           See Also|                            |https://bugs.libre-soc.org/
                   |                            |show_bug.cgi?id=351

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #1 from Cole Poirier <colepoirier@gmail.com> ---
Made some very minimal progress on this today. Since I'm still learning how to
write proofs it takes a long time to get the most basic assumptions of the most
basic class (Register) from regfile.py sorted enough that I can start to reason
about them. I think the foundation that I laid today will enable me to write
some code for this (instead of just written notes from working and reasoning
through the assumptions of the module) tomorrow. But, if this proof is needed
before then for the virtual_port tests, Luke please feel free to take it over
like you did with virtual_port today. I want to help, so I don't want my
learning while working slowly to be a blocker :)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #2 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #1)
> Made some very minimal progress on this today. Since I'm still learning how
> to write proofs it takes a long time to get the most basic assumptions of
> the most basic class (Register) from regfile.py sorted enough that I can
> start to reason about them. I think the foundation that I laid today will
> enable me to write some code for this (instead of just written notes from
> working and reasoning through the assumptions of the module) tomorrow. But,
> if this proof is needed before then for the virtual_port tests,

it's not.  i have a preliminary virtual_port test running, yesterday.

> Luke please
> feel free to take it over like you did with virtual_port today. I want to
> help, so I don't want my learning while working slowly to be a blocker :)

i don't totally get them either, so we work on it together, over time, ok?

as you have probably noticed, i tend to write "proof-of-concept" unit
tests that at least give a basic level of confidence then move quickly
on.  this will allow rapid progress but will bite us in corner-cases.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #3 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #2)
> (In reply to Cole Poirier from comment #1)
> > if this proof is needed before then for the virtual_port tests,
> 
> it's not.  i have a preliminary virtual_port test running, yesterday.

Saw your 'proof-of-concept' test case yesterday, was helpful for understanding
the functionality of the module further. Unfortunately, I think this test is
now failing with the following error:

```
Traceback (most recent call last):
  File "virtual_port.py", line 203, in <module>
    test_regfile()
  File "virtual_port.py", line 200, in test_regfile
    vcd_name='test_regfile_array.vcd')
  File "/home/colepoirier/src/nmigen/nmigen/compat/sim/__init__.py", line 22,
in run_simulation
    fragment.domains += ClockDomain("sync")
AttributeError: 'VirtualRegPort' object has no attribute 'domains'
```

I suspect it's a simple fix, but the answer is not immediately apparent to me.


> > Luke please
> > feel free to take it over like you did with virtual_port today. I want to
> > help, so I don't want my learning while working slowly to be a blocker :)
> 
> i don't totally get them either, so we work on it together, over time, ok?
> 
> as you have probably noticed, i tend to write "proof-of-concept" unit
> tests that at least give a basic level of confidence then move quickly
> on.  this will allow rapid progress but will bite us in corner-cases.

Indeed, it seems to be a very productive strategy. Looking forward to working
with you on the proof today. Just reviewing my notes now, should have some code
for some of the basic assumptions committed in the next hour.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #3)
> (In reply to Luke Kenneth Casson Leighton from comment #2)
> > (In reply to Cole Poirier from comment #1)
> > > if this proof is needed before then for the virtual_port tests,
> > 
> > it's not.  i have a preliminary virtual_port test running, yesterday.
> 
> Saw your 'proof-of-concept' test case yesterday, was helpful for
> understanding the functionality of the module further. Unfortunately, I
> think this test is now failing with the following error:
> 
> ```
> Traceback (most recent call last):
>   File "virtual_port.py", line 203, in <module>
>     test_regfile()
>   File "virtual_port.py", line 200, in test_regfile
>     vcd_name='test_regfile_array.vcd')
>   File "/home/colepoirier/src/nmigen/nmigen/compat/sim/__init__.py", line
> 22, in run_simulation
>     fragment.domains += ClockDomain("sync")
> AttributeError: 'VirtualRegPort' object has no attribute 'domains'
> ```

then you know what to do there: inspect line 22 of that file, and check
it against the latest version of nmigen, online.  have a look:
https://github.com/nmigen/nmigen/blob/master/nmigen/compat/sim/__init__.py


    if not isinstance(generators, dict):
        generators = {"sync": generators}
        if "sync" not in fragment.domains:
            fragment.add_domains(ClockDomain("sync"))


does that match with what you have?

> Indeed, it seems to be a very productive strategy. Looking forward to
> working with you on the proof today. Just reviewing my notes now, should
> have some code for some of the basic assumptions committed in the next hour.

cool.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #5 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #4)
> then you know what to do there: inspect line 22 of that file, and check
> it against the latest version of nmigen, online.  have a look:
> https://github.com/nmigen/nmigen/blob/master/nmigen/compat/sim/__init__.py
> 
> 
>     if not isinstance(generators, dict):
>         generators = {"sync": generators}
>         if "sync" not in fragment.domains:
>             fragment.add_domains(ClockDomain("sync"))
> 
> 
> does that match with what you have?

Aha, my mistake, I forgot to checkout nmigen/nmigen master after I made a PR to
nmigen the other week... Oof silly me. fixed now, thanks.

> > Indeed, it seems to be a very productive strategy. Looking forward to
> > working with you on the proof today. Just reviewing my notes now, should
> > have some code for some of the basic assumptions committed in the next hour.
> 
> cool.

Are class attributes (self.x) declared within __init__ public and those
declared within elaborate() private? I though all python class attributes were
public, and in order to get 'private' variables in a class you have to do as
you did in virtual_port.py by simply declaring it a variable and not an
attribute of the class object. I ask because I'm having an issue where I'm
trying to access self.reg of class Register(), which is declared inside
elaborate(), and I get an error, but accessing any of the self.xyz attributes
like self.width declared in __init__ works fine.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #6 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #5)

> Are class attributes (self.x) declared within __init__ public and those
> declared within elaborate() private? 

in python the concept of public and private in classes does not exist, like it
does in c++

class instance atttributes are therefore *always* public.  there does exist
however a convention that if something starts with underscores it is *by
convention* considered "not for public use".

what you are getting confused about is "scope".

within a function, any local variables are entirely local.  however note that
stuff declared in a module is *also* accessible within the function.

therefore, only variables created *inside* the function are private scope to
that function.



> I though all python class attributes
> were public, and in order to get 'private' variables in a class you have to
> do as you did in virtual_port.py by simply declaring it a variable and not
> an attribute of the class object. I ask because I'm having an issue where
> I'm trying to access self.reg of class Register(), which is declared inside
> elaborate(),

no it is not declared (this is not c), it is created, and it is created only
when the function elaborate is called.

how can you expect Register.reg to be created when Register.elaborate has not
been called?

> and I get an error, but accessing any of the self.xyz
> attributes like self.width declared in __init__ works fine.

this is correct behaviour.  python is not a static language.

commit it let's have a look.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #7 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #6)
> (In reply to Cole Poirier from comment #5)
> 
> > Are class attributes (self.x) declared within __init__ public and those
> > declared within elaborate() private? 
> 
> in python the concept of public and private in classes does not exist, like
> it does in c++
> 
> class instance atttributes are therefore *always* public.  there does exist
> however a convention that if something starts with underscores it is *by
> convention* considered "not for public use".
> 
> what you are getting confused about is "scope".
> 
> within a function, any local variables are entirely local.  however note
> that stuff declared in a module is *also* accessible within the function.
> 
> therefore, only variables created *inside* the function are private scope to
> that function.

Thank you for clarifying this for me. My first language three years ago was
python (primarily pandas and numpy for data analysis), so I'm reasonably
comfortable with python scopes, the mistake I made was not thinking I had to
call elaborate first, which is about as silly. I also appreciate the review of
python vs c/c++, but I'm only proficient in python and rust, (and javascript if
I absolutely must**), so my OOP knowledge only comes from python, I don't know
how to write the other stuff like public/private classes, I can only sort of
read it because I've had to learn to understand when reading c/c++/java/go
code.

**I prefer doing UI in elm, which is a functional language that's designed
specifically for UI design that's transpiled to js. I bring this up because I
think you might find interesting to check out in a free moment because of your
work on pyjamas

> > I though all python class attributes
> > were public, and in order to get 'private' variables in a class you have to
> > do as you did in virtual_port.py by simply declaring it a variable and not
> > an attribute of the class object. I ask because I'm having an issue where
> > I'm trying to access self.reg of class Register(), which is declared inside
> > elaborate(),
> 
> no it is not declared (this is not c), it is created, and it is created only
> when the function elaborate is called.
> 
> how can you expect Register.reg to be created when Register.elaborate has
> not been called?
> 
> > and I get an error, but accessing any of the self.xyz
> > attributes like self.width declared in __init__ works fine.
> 
> this is correct behaviour.  python is not a static language.
> 
> commit it let's have a look.

With you... now. Pushed my commit.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #8 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
  18     def elaborate(self, platform):
  19         m = Module()
  20         comb = m.d.comb
  21         m.submodules.dut = dut = Register(32)

yep not going to work, trying to access domething that has not had elaborate
called.

derive Driver *from* Register, instead, and replace the above with

m = super().elaborate(platform)

then the Register.elaborate will have been called.

then self.reg will exist

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #9 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #8)
>   18     def elaborate(self, platform):
>   19         m = Module()
>   20         comb = m.d.comb
>   21         m.submodules.dut = dut = Register(32)
> 
> yep not going to work, trying to access domething that has not had elaborate
> called.
> 
> derive Driver *from* Register, instead, and replace the above with
> 
> m = super().elaborate(platform)
> 
> then the Register.elaborate will have been called.
> 
> then self.reg will exist

Thanks very much! Will work on getting the existing Asserts working, then push
another commit.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #10 from Cole Poirier <colepoirier@gmail.com> ---
Tests now actually run, so I pushed a new commit. In order to formally verify
class Register(), I think I've done most of it, but there's a part of the
class's elaborate function that uses sync instead of comb, and I'm not sure how
to do this in proof form.

```
def elaborate(self, platform):
     m = Module()
     self.reg = reg = Signal(self.width, name="reg")

[snip..] 
     # write ports, don't allow write to address 0 (ignore it)
     for wp in self._wrports:
         with m.If(wp.wen):
             m.d.sync += reg.eq(wp.data_i)

     return m
```

Does the above prevent write to address 0, and if so how? because it doesn't
seem to do any conditional checking. Further, how would I integrate this in
order to finish the proof or register?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #10)
> Tests now actually run, so I pushed a new commit. In order to formally
> verify class Register(), I think I've done most of it, but there's a part of
> the class's elaborate function that uses sync instead of comb, and I'm not
> sure how to do this in proof form.

one way is to use Past()

> 
> ```
> def elaborate(self, platform):
>      m = Module()
>      self.reg = reg = Signal(self.width, name="reg")
> 
> [snip..] 
>      # write ports, don't allow write to address 0 (ignore it)
>      for wp in self._wrports:
>          with m.If(wp.wen):
>              m.d.sync += reg.eq(wp.data_i)
> 
>      return m
> ```
> 
> Does the above prevent write to address 0, and if so how?

no.  do git pull

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #12 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #11)
> (In reply to Cole Poirier from comment #10)
> > Tests now actually run, so I pushed a new commit. In order to formally
> > verify class Register(), I think I've done most of it, but there's a part of
> > the class's elaborate function that uses sync instead of comb, and I'm not
> > sure how to do this in proof form.
> 
> one way is to use Past()

Sorry for the delay. I did a git pull and added an Assert using Past() but my
proof is still failing. I pushed my commit. Can you take a look when you can to
help me identify where I've erred?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #13 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
no idea.

first thing though: it is unsafe to mix python parameters that change the
entire behaviour of the module.

i suggest starting with two utterly different proofs, divided and isolated with
"if self.writethru".  yes NOT m.If because python parameters != nmigen AST.A

then, to do a 4 way (dual nested) set of m.If on ren and wen.

then, in EACH quadrant, do completely separate assertions.

but before making those assertions, write out in words the expected behaviour
when the 4 way truth table of wen and ren occurs.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #14 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #13)
> no idea.
> 
> first thing though: it is unsafe to mix python parameters that change the
> entire behaviour of the module.
> 
> i suggest starting with two utterly different proofs, divided and isolated
> with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> AST.A
> 
> then, to do a 4 way (dual nested) set of m.If on ren and wen.
> 
> then, in EACH quadrant, do completely separate assertions.
> 
> but before making those assertions, write out in words the expected
> behaviour when the 4 way truth table of wen and ren occurs.

Ah yes that makes sense. That is how the module I'm trying to verify is written
after all. Thanks for your guidance and helpful redirection on this. I'll work
through the 4 way truth table with expected behavior in words then report back.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #15 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Cole Poirier from comment #14)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > no idea.
> > 
> > first thing though: it is unsafe to mix python parameters that change the
> > entire behaviour of the module.
> > 
> > i suggest starting with two utterly different proofs, divided and isolated
> > with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> > AST.A
> > 
> > then, to do a 4 way (dual nested) set of m.If on ren and wen.
> > 
> > then, in EACH quadrant, do completely separate assertions.
> > 
> > but before making those assertions, write out in words the expected
> > behaviour when the 4 way truth table of wen and ren occurs.
> 
> Ah yes that makes sense. That is how the module I'm trying to verify is
> written after all. Thanks for your guidance and helpful redirection on this.
> I'll work through the 4 way truth table with expected behavior in words then
> report back.

Spent an hour trying to sense of this but I think my brain has given up for the
day. Will make a fresh effort tomorrow.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #16 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #15)

> Spent an hour trying to sense of this but I think my brain has given up for
> the day. Will make a fresh effort tomorrow.

did a bit of a reorg.  i think we need to look at how proof_fu.py works.
the use of "Initial()" may be crucial.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Michael Nolan <mtnolan2640@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |mtnolan2640@gmail.com

--- Comment #17 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #16)
> (In reply to Cole Poirier from comment #15)
> 
> > Spent an hour trying to sense of this but I think my brain has given up for
> > the day. Will make a fresh effort tomorrow.
> 
> did a bit of a reorg.  i think we need to look at how proof_fu.py works.
> the use of "Initial()" may be crucial.

It is. From my experience doing formal stuff in verilog, if you use $past()
without making sure the module is properly reset, the proof engine will make up
values for the signals before the proof even starts. Making sure you have a
reset for the first cycle of the proof, and not examining any Past() signals on
that cycle will avoid this.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Michael Nolan <mtnolan2640@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
          Component|Source Code                 |Formal Verification

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #18 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #13)
> i suggest starting with two utterly different proofs, divided and isolated
> with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> AST.A
> 
> then, to do a 4 way (dual nested) set of m.If on ren and wen.
> 
> then, in EACH quadrant, do completely separate assertions.
> 
> but before making those assertions, write out in words the expected
> behaviour when the 4 way truth table of wen and ren occurs.

I think I might not understand the functionality of the module enough to know
the expected behaviour. Is it the case that if not writethru nothing is
supposed to happen?

Further with regard to Michael's comments about needing to use Initial() and
ResetSignal() should I wrap the if writethru..else in a "with m.If(init)...with
m.Else()" similar to proof_fu.py? Is it the case that, if Initial() then do rd
operations, and else do wr operations?

Finally, with regard to the 4-way truth table, is this format close to correct?

```
rd.ren wr.wen rd.data_o reg
0      0      x         y
0      1      x         y
1      0      x         y
1      1      x         y
```

If not can you help me with a diagram or a link? I've looked for 4-way truth
tables via google and I just get basic boolean logic tutorials in the form of:

```
p q  p AND q
0 0  0
0 1  0
1 0  0
1 1  1
```

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #19 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Cole Poirier from comment #18)

> Further with regard to Michael's comments about needing to use Initial() and
> ResetSignal() should I wrap the if writethru..else in a "with
> m.If(init)...with m.Else()" similar to proof_fu.py? Is it the case that, if
> Initial() then do rd operations, and else do wr operations?

I don't know specifically for this module, but generally you want to make sure
that the module and control signals are initialized to a default state. 

For instance, you're going to be proving that a write to a register works sort
of like this:

with m.If(Past(rd_en)):
    comb += Assert(data_out == something)

However, on cycle 0, yosys may choose Past(rd_en) to be High, but no data will
be output because it didn't happen during the actual proof (basically, yosys
saves the past state of the signal to a register, which is then read whenever
you call Past(signal). But on cycle 0, that register has a random value)

If you wait one cycle (with m.If(~init)) before doing your assertion, you won't
have that issue because Past(signal) will return the actual value from the
cycle before.

However, if you decide to use the initial cycle to reset your register file,
you'll have other issues because you're resetting it at the same time you're
reading it, so once again your assertion will probably fail. To fix this, you'd
want to use an Assume to force rd_en (or whatever other signals you're using)
to be disabled during reset.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #20 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #18)
> (In reply to Luke Kenneth Casson Leighton from comment #13)
> > i suggest starting with two utterly different proofs, divided and isolated
> > with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> > AST.A
> > 
> > then, to do a 4 way (dual nested) set of m.If on ren and wen.
> > 
> > then, in EACH quadrant, do completely separate assertions.
> > 
> > but before making those assertions, write out in words the expected
> > behaviour when the 4 way truth table of wen and ren occurs.
> 
> I think I might not understand the functionality of the module enough to
> know the expected behaviour. Is it the case that if not writethru nothing is
> supposed to happen?
> 
> Further with regard to Michael's comments about needing to use Initial() and
> ResetSignal() should I wrap the if writethru..else in a "with
> m.If(init)...with m.Else()" similar to proof_fu.py?

yyep.

> Is it the case that, if
> Initial() then do rd operations, and else do wr operations?

nnope.  Initial() is just that: the initial conditions.


> Finally, with regard to the 4-way truth table, is this format close to
> correct?
> 
> ```
> rd.ren wr.wen rd.data_o reg
> 0      0      x         y
> 0      1      x         y
> 1      0      x         y
> 1      1      x         y
> ```

yep.  drop that into a comment in the code, so we can edit it before
implementing it.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #21 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #20)
> (In reply to Cole Poirier from comment #18)
> > (In reply to Luke Kenneth Casson Leighton from comment #13)
> > > i suggest starting with two utterly different proofs, divided and isolated
> > > with "if self.writethru".  yes NOT m.If because python parameters != nmigen
> > > AST.A
> > > 
> > > then, to do a 4 way (dual nested) set of m.If on ren and wen.
> > > 
> > > then, in EACH quadrant, do completely separate assertions.
> > > 
> > > but before making those assertions, write out in words the expected
> > > behaviour when the 4 way truth table of wen and ren occurs.
> > 
> > I think I might not understand the functionality of the module enough to
> > know the expected behaviour. Is it the case that if not writethru nothing is
> > supposed to happen?
> > 
> > Further with regard to Michael's comments about needing to use Initial() and
> > ResetSignal() should I wrap the if writethru..else in a "with
> > m.If(init)...with m.Else()" similar to proof_fu.py?
> 
> yyep.
> 
> > Is it the case that, if
> > Initial() then do rd operations, and else do wr operations?
> 
> nnope.  Initial() is just that: the initial conditions.
> 
>  
> > Finally, with regard to the 4-way truth table, is this format close to
> > correct?
> > 
> > ```
> > rd.ren wr.wen rd.data_o reg
> > 0      0      x         y
> > 0      1      x         y
> > 1      0      x         y
> > 1      1      x         y
> > ```
> 
> yep.  drop that into a comment in the code, so we can edit it before
> implementing it.

Ok. Pushed a commit with that. Can you take a look?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #22 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #21)

> Ok. Pushed a commit with that. Can you take a look?

done.  updated.  basically, this is... complicated.  there's time-dependent
interactions.  i actually managed to get one case to work: when wen is
not set, the reg should not change.  past value should equal the present value.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #23 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #22)

> done.  updated.  basically, this is... complicated.  there's time-dependent
> interactions.  i actually managed to get one case to work: when wen is
> not set, the reg should not change.  past value should equal the present
> value.

Ah it's time-dependent, that makes sense. Thanks, pulled and ran the test.
Cool. How would I go about better understanding how ren and wen are supposed to
interact? Studying the logic diagram? Or something else?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #24 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Cole Poirier from comment #23)
> (In reply to Luke Kenneth Casson Leighton from comment #22)
> 
> > done.  updated.  basically, this is... complicated.  there's time-dependent
> > interactions.  i actually managed to get one case to work: when wen is
> > not set, the reg should not change.  past value should equal the present
> > value.
> 
> Ah it's time-dependent, that makes sense. Thanks, pulled and ran the test.
> Cool. How would I go about better understanding how ren and wen are supposed
> to interact? Studying the logic diagram? Or something else?

Luke, is the use of Settle() warranted in the synchronous part of this proof?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #25 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #24)

> Luke, is the use of Settle() warranted in the synchronous part of this proof?

not at all.

l.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #26 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #25)
> (In reply to Cole Poirier from comment #24)
> 
> > Luke, is the use of Settle() warranted in the synchronous part of this proof?
> 
> not at all.
> 
> l.

Thanks, this helps clarify a little bit more for me the use and functionality
of Settle().

I think the proof as it stands may need a re-org... I tried filling in the
quadrants according the to 4-way truth table comment draft that I did, which I
saw you fixed. But nothing passes but the same Assert you added when you fixed
the truth table a few days ago (this is actually the else condition in the
code, but modified here to If for clarity):

```
with m.If(not Past(wp.wen)):
    # if wen not set, reg should not change
    comb += Assert(reg == Past(reg))
```

This leads me to believe that either the proof is wrong and needs to be
reorganized to conform to how Register is implemented in regfile/regfile.py, or
that Regfile itself doesn't properly implement what the proof says it should...
I'm thinking I should try re-organizing the proof first to see if that improves
things? What do you think?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #27 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cole Poirier from comment #26)

> This leads me to believe that either the proof is wrong and needs to be
> reorganized to conform to how Register is implemented in regfile/regfile.py,

the unit test for RegFileArray and RegFile leads me to believe that it is.
however it is worthwhile confirming this by writing a straight unit test,
exactly is done in regfile.py.

basically i have no idea what i am doing with Formal Proofs.  i can read
them, i can *maybe* spot omissions once they're written, and i can just about
manage combinatorial ones.  these sync/time-based ones: really no idea.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #28 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
https://zipcpu.com/blog/2018/03/10/induction-exercise.html

all i can say is: argh :)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Cesar Strauss <cestrauss@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |cestrauss@gmail.com

--- Comment #29 from Cesar Strauss <cestrauss@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #27)
> basically i have no idea what i am doing with Formal Proofs.  i can read
> them, i can *maybe* spot omissions once they're written, and i can just about
> manage combinatorial ones.  these sync/time-based ones: really no idea.

Hi Luke,

As I learned about formal verification, I found the initial slides of
http://www.clifford.at/papers/2017/smtbmc-sby/slides.pdf very enlightening for
basic concepts. See for instance slides 6 to 16.

(In reply to Luke Kenneth Casson Leighton from comment #28)
> https://zipcpu.com/blog/2018/03/10/induction-exercise.html
> 
> all i can say is: argh :)

This illustrates the difficulties in induction proofs.

It is apparent, from the circuit, that the two shift-registers will be equal
for all time, so the XOR output will be always zero.

However, bounded model check can only check for a finite number of cycles. To
prove it for all time, you prove it that, whenever the assertions hold for n
cycles, it will hold for the n+1 cycle.

The problem with induction, is that it does not start with the initial state
(see slide 11). So, the "initial" state can be in the unreachable state area
(see slide 9).

In the example, an initial state in which the shift register are different, is
unreachable. But the proof checker does not know that. So, it can choose an
initial state where the last bit is equal, passing the assertion, but the
next-to-last bit is different.

Then, it holds the shift enable de-asserted for n cycles and asserts it for the
n+1 cycle, finally shifting out the differing bits. So, it passes for n cycles,
but fails in n+1.

The easy way to solve this is to assert that the shift register contents are
always equal.

Another way is limiting the time in which the shift-enable can be kept
de-asserted. This is done with an assumption.

Without an assumption, the proof checker is free to toggle any unconnected
input signal, in the most perverse way possible, to make the proof fail. In
reality, the input signals must obey some protocol. For instance, you tell the
proof checker that it must keep (assume) issue_i low whenever busy_o is high.
Otherwise it would be free to assert issue_i in the middle of a busy_o cycle,
which it's a violation of the protocol.

Hope it helps,

Cesar

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #30 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Cole Poirier from comment #26)
> (In reply to Luke Kenneth Casson Leighton from comment #25)
> > (In reply to Cole Poirier from comment #24)
> > 
> > > Luke, is the use of Settle() warranted in the synchronous part of this proof?
> > 
> > not at all.
> > 
> > l.
> 
> Thanks, this helps clarify a little bit more for me the use and
> functionality of Settle().
> 
> I think the proof as it stands may need a re-org... I tried filling in the
> quadrants according the to 4-way truth table comment draft that I did, which
> I saw you fixed. But nothing passes but the same Assert you added when you
> fixed the truth table a few days ago (this is actually the else condition in
> the code, but modified here to If for clarity):
> 
> ```
> with m.If(not Past(wp.wen)):
>     # if wen not set, reg should not change
>     comb += Assert(reg == Past(reg))
> ```
> 
> This leads me to believe that either the proof is wrong and needs to be
> reorganized to conform to how Register is implemented in regfile/regfile.py,
> or that Regfile itself doesn't properly implement what the proof says it
> should... I'm thinking I should try re-organizing the proof first to see if
> that improves things? What do you think?

I'm taking a look at regfile.py as well as the proof. Part of the reason you
see everything failing is that the truth table in the proof isn't right; the
register file doesn't have a defined output when read enable is low. I have an
idea as to how to prove that register writes work, would you like me to write
it or leave it up to you?

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #31 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Michael Nolan from comment #30)

> I'm taking a look at regfile.py as well as the proof. Part of the reason you
> see everything failing is that the truth table in the proof isn't right; the
> register file doesn't have a defined output when read enable is low. I have
> an idea as to how to prove that register writes work, would you like me to
> write it or leave it up to you?

Actually, it turned out that the register file wasn't generating read and write
ports.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #32 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Michael Nolan from comment #30)

> I'm taking a look at regfile.py as well as the proof. Part of the reason you
> see everything failing is that the truth table in the proof isn't right; the
> register file doesn't have a defined output when read enable is low.

the default - because it is combinatorial - will be that the output is
zero when read-enable is low.  we rely on this when it comes to multiple
registers (later) because those zeros are OR-cascaded together (using
ortreereduce) to create the output.

> I have
> an idea as to how to prove that register writes work, would you like me to
> write it?

yes please.  we really need to move on, fast.  RegFileArray *should* be
a lot easier to write (if using the Register as the base)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #33 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #32)

> the default - because it is combinatorial - will be that the output is
> zero when read-enable is low.  we rely on this when it comes to multiple
> registers (later) because those zeros are OR-cascaded together (using
> ortreereduce) to create the output.

This has been fixed

> 
> yes please.  we really need to move on, fast.  RegFileArray *should* be
> a lot easier to write (if using the Register as the base)

Done.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #34 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Michael Nolan from comment #31)

> Actually, it turned out that the register file wasn't generating read and
> write ports.

thank you for sorting that.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #35 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #34)
> (In reply to Michael Nolan from comment #31)
> 
> > Actually, it turned out that the register file wasn't generating read and
> > write ports.
> 
> thank you for sorting that.

Thanks so much Michael, more material for me to learn from :)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #36 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Cesar Strauss from comment #29)
> (In reply to Luke Kenneth Casson Leighton from comment #27)
> > basically i have no idea what i am doing with Formal Proofs.  i can read
> > them, i can *maybe* spot omissions once they're written, and i can just about
> > manage combinatorial ones.  these sync/time-based ones: really no idea.
> 
> Hi Luke,
> 
> As I learned about formal verification, I found the initial slides of
> http://www.clifford.at/papers/2017/smtbmc-sby/slides.pdf very enlightening
> for basic concepts. See for instance slides 6 to 16.
> 
> (In reply to Luke Kenneth Casson Leighton from comment #28)
> > https://zipcpu.com/blog/2018/03/10/induction-exercise.html
> > 
> > all i can say is: argh :)
> 
> This illustrates the difficulties in induction proofs.
> 
> It is apparent, from the circuit, that the two shift-registers will be equal
> for all time, so the XOR output will be always zero.
> 
> However, bounded model check can only check for a finite number of cycles.
> To prove it for all time, you prove it that, whenever the assertions hold
> for n cycles, it will hold for the n+1 cycle.
> 
> The problem with induction, is that it does not start with the initial state
> (see slide 11). So, the "initial" state can be in the unreachable state area
> (see slide 9).
> 
> In the example, an initial state in which the shift register are different,
> is unreachable. But the proof checker does not know that. So, it can choose
> an initial state where the last bit is equal, passing the assertion, but the
> next-to-last bit is different.
>  
> Then, it holds the shift enable de-asserted for n cycles and asserts it for
> the n+1 cycle, finally shifting out the differing bits. So, it passes for n
> cycles, but fails in n+1.
> 
> The easy way to solve this is to assert that the shift register contents are
> always equal.
> 
> Another way is limiting the time in which the shift-enable can be kept
> de-asserted. This is done with an assumption.
> 
> Without an assumption, the proof checker is free to toggle any unconnected
> input signal, in the most perverse way possible, to make the proof fail. In
> reality, the input signals must obey some protocol. For instance, you tell
> the proof checker that it must keep (assume) issue_i low whenever busy_o is
> high. Otherwise it would be free to assert issue_i in the middle of a busy_o
> cycle, which it's a violation of the protocol.
> 
> Hope it helps,
> 
> Cesar

Thank you very much for sharing this to help me Cesar, it's super helpful, and
I'm incredibly grateful for your help.

Cole

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

--- Comment #37 from Michael Nolan <mtnolan2640@gmail.com> ---
Aha, I knew something was fishy. The inputs should have been AnySeq not
AnyConst. Because it's a sequential circuit, they should be able to change on
any cycle (to be able to read or write and such)

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon]

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

Luke Kenneth Casson Leighton <lkcl@lkcl.net> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
    NLnet milestone|---                         |NLNet.2019.10.Formal

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev