A formal proof of the RegFile classes is needed * Register - DONE * RegfileArray - DONE * Regfile - todo * VirtualRegFilePort - todo
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 :)
(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.
(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.
(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.
(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.
(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.
(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.
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
(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.
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?
(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
(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?
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.
(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.
(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.
(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.
(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.
(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 ```
(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.
(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.
(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?
(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.
(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?
(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?
(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.
(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?
(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.
https://zipcpu.com/blog/2018/03/10/induction-exercise.html all i can say is: argh :)
(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
(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?
(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.
(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)
(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.
(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.
(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 :)
(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
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)