Bug 353 - formal proof of soc.regfile classes RegFile and RegFileArray needed
Summary: formal proof of soc.regfile classes RegFile and RegFileArray needed
Status: CONFIRMED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Cole Poirier
URL:
Depends on:
Blocks:
 
Reported: 2020-05-26 01:13 BST by Cole Poirier
Modified: 2020-06-02 13:27 BST (History)
4 users (show)

See Also:
NLnet milestone: NLNet.2019.10.Formal
total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Cole Poirier 2020-05-26 01:13:10 BST
A formal proof of the RegFile classes is needed

* Register           - DONE
* RegfileArray       - DONE
* Regfile            - todo
* VirtualRegFilePort - todo
Comment 1 Cole Poirier 2020-05-27 05:12:44 BST
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 :)
Comment 2 Luke Kenneth Casson Leighton 2020-05-27 12:14:46 BST
(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.
Comment 3 Cole Poirier 2020-05-27 17:45:13 BST
(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.
Comment 4 Luke Kenneth Casson Leighton 2020-05-27 18:26:36 BST
(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.
Comment 5 Cole Poirier 2020-05-27 18:42:40 BST
(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.
Comment 6 Luke Kenneth Casson Leighton 2020-05-27 19:08:15 BST
(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.
Comment 7 Cole Poirier 2020-05-27 19:40:38 BST
(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.
Comment 8 Luke Kenneth Casson Leighton 2020-05-27 19:48:12 BST
  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
Comment 9 Cole Poirier 2020-05-27 19:56:53 BST
(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.
Comment 10 Cole Poirier 2020-05-27 20:25:25 BST
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?
Comment 11 Luke Kenneth Casson Leighton 2020-05-27 20:43:34 BST
(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
Comment 12 Cole Poirier 2020-05-28 02:18:42 BST
(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?
Comment 13 Luke Kenneth Casson Leighton 2020-05-28 02:33:08 BST
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.
Comment 14 Cole Poirier 2020-05-28 02:50:21 BST
(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.
Comment 15 Cole Poirier 2020-05-28 03:59:21 BST
(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.
Comment 16 Luke Kenneth Casson Leighton 2020-05-28 11:18:30 BST
(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.
Comment 17 Michael Nolan 2020-05-28 15:18:37 BST
(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.
Comment 18 Cole Poirier 2020-05-28 20:50:04 BST
(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
```
Comment 19 Michael Nolan 2020-05-28 21:00:00 BST
(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.
Comment 20 Luke Kenneth Casson Leighton 2020-05-28 21:27:22 BST
(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.
Comment 21 Cole Poirier 2020-05-29 00:18:18 BST
(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?
Comment 22 Luke Kenneth Casson Leighton 2020-05-29 00:41:42 BST
(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.
Comment 23 Cole Poirier 2020-05-29 00:57:33 BST
(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?
Comment 24 Cole Poirier 2020-05-30 22:41:08 BST
(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?
Comment 25 Luke Kenneth Casson Leighton 2020-05-30 23:03:13 BST
(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.
Comment 26 Cole Poirier 2020-05-30 23:13:17 BST
(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?
Comment 27 Luke Kenneth Casson Leighton 2020-05-30 23:38:42 BST
(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.
Comment 28 Luke Kenneth Casson Leighton 2020-05-31 15:12:40 BST
https://zipcpu.com/blog/2018/03/10/induction-exercise.html

all i can say is: argh :)
Comment 29 Cesar Strauss 2020-05-31 19:20:13 BST
(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
Comment 30 Michael Nolan 2020-06-01 18:06:10 BST
(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?
Comment 31 Michael Nolan 2020-06-01 18:51:28 BST
(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.
Comment 32 Luke Kenneth Casson Leighton 2020-06-01 18:52:21 BST
(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)
Comment 33 Michael Nolan 2020-06-01 18:53:56 BST
(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.
Comment 34 Luke Kenneth Casson Leighton 2020-06-01 18:55:19 BST
(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.
Comment 35 Cole Poirier 2020-06-01 19:06:23 BST
(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 :)
Comment 36 Cole Poirier 2020-06-01 19:07:21 BST
(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
Comment 37 Michael Nolan 2020-06-01 19:35:38 BST
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)