Assigned to me by Luke as a first nmigen excercise. pseudo-code here: perm <- [0] * 8 for i = 0 to 7 index <- (RS)[8*i:8*i+7] if index < 64 then perm[i] <- (RB)[index] else perm[i] <- 0 RA <- [0]*56 || perm[0:7] I am to see if I can write the above in nmigen. Below is the simulation version (translated from the above pseudo-code), it may be easier to understand: @inject() def op_bpermd(self, RS, RB): perm = concat(0, repeat=8) for i in range(0, 7 + 1): index = RS[8 * i:8 * i + 7 + 1] if lt(index, 64): perm[i] = RB[index] else: perm[i] = 0 RA = concat(concat(0, repeat=56), perm[0:8]) notes: * repeat=8 you use Repl * concat you use Cat * index you will have to actually store that in a temporary Signal (8 bits in length)
The code below is what I have so far in my first attempt at solving this problem: from nmigen import Elaboratable, Signal, Module, Repl, Cat from nmigen.cli import main class Bpermd(Elaboratable): def __init__(self, width): self.perm = Signal(width) self.rs = Signal(width) self.ra = Signal(width) self.rb = Signal(width) def elaborate(self, platform): m = Module() m.d.comb += self.perm.eq(Cat(0, Repl(8))) index = Signal(8) for i in range(0, 7 + 1): index = rs[8 * i:8 * i + 7 + 1] with m.If(index.lt(64)): m.d.comb += self.perm[i].eq(rb[index]) with m.Else(): m.d.comb += self.perm[i].eq(0) m.d.comb += ra.eq(Cat(Cat(0, Repl(56)),prem[0:8])) return m if __name__ == "__main__": bperm = Bpermd(width=8) main(bperm, ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) ``` When I try running a command (python3 bperm.py simulate -c 20 -v bperm.vcd) taken from this (http://blog.lambdaconcept.com/doku.php?id=nmigen:nmigen_hello_world) tutorial I get the following error: ``` Traceback (most recent call last): File "bperm.py", line 26, in <module> main(bperm, ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) File "/home/colepoirier/src/nmigen/nmigen/cli.py", line 74, in main main_runner(parser, parser.parse_args(), *args, **kwargs) File "/home/colepoirier/src/nmigen/nmigen/cli.py", line 65, in main_runner fragment = Fragment.get(design, platform) File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 39, in get obj = obj.elaborate(platform) File "bperm.py", line 13, in elaborate m.d.comb += self.perm.eq(Cat(0, Repl(8))) TypeError: __init__() missing 1 required positional argument: 'count' ``` I don't understand why I am getting the error that I'm missing a positional argument count in my __init__() function, since it only takes the parameters self and width. I'm sure this error is just due to my not understanding nmigen properly yet, so any help will be very much appreciated.
Change line 13 to ``m.d.comb += self.perm.eq(0)`` You don't need to use ``Cat`` and or ``Repo``. nMigen knows how to 0 pad and sign extend. Now you'll get another issue - namely, that rs isn't define... What is Bpermd supposed to do? You should put a Python class comment as shown below to help readers understand. ``` class Bpermd(Elaboratable): """This class does X,Y, and Z""" def __init__(self, width): self.perm = Signal(width) ```
(In reply to Yehowshua from comment #2) > Change line 13 to > ``m.d.comb += self.perm.eq(0)`` > > You don't need to use ``Cat`` and or ``Repo``. nMigen knows how to 0 pad and > sign extend. > > Now you'll get another issue - namely, that rs isn't define... > > What is Bpermd supposed to do? > You should put a Python class comment as shown below to help readers > understand. > > ``` > class Bpermd(Elaboratable): > """This class does X,Y, and Z""" > def __init__(self, width): > self.perm = Signal(width) > ``` Thanks so much for your help Yehowshua! I've done as you reccomended and added a doc string, as well as changing line 13, and referring to ra and rb with the self prefix. Now I am getting a different error, perhaps you could advise me as to how to proceed? 1 bperm.py X from nmigen import Elaboratable, Signal, Module, Repl, Cat from nmigen.cli import main class Bpermd(Elaboratable): """This class does a Bit Permute on a Doubleword X-form bpermd RA,RS,RB] [snip] """ def __init__(self, width): self.perm = Signal(width) self.rs = Signal(width) self.ra = Signal(width) self.rb = Signal(width) def elaborate(self, platform): m = Module() m.d.comb += self.perm.eq(0) index = Signal(8) for i in range(0, 7 + 1): index = self.rs[8 * i:8 * i + 7 + 1] with m.If(index < 64): m.d.comb += self.perm[i].eq(self.rb[index]) with m.Else(): m.d.comb += self.perm[i].eq(0) m.d.comb += self.ra.eq(Cat(Cat(0,Repl(56)), self.perm[0:8])) return m if __name__ == "__main__": bperm = Bpermd(width=64) main(bperm,ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) ``` Traceback (most recent call last): File "bperm.py", line 50, in <module> main(bperm,ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) File "/home/colepoirier/src/nmigen/nmigen/cli.py", line 74, in main main_runner(parser, parser.parse_args(), *args, **kwargs) File "/home/colepoirier/src/nmigen/nmigen/cli.py", line 65, in main_runner fragment = Fragment.get(design, platform) File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 39, in get obj = obj.elaborate(platform) File "bperm.py", line 42, in elaborate m.d.comb += self.perm[i].eq(self.rb[index]) File "/home/colepoirier/src/nmigen/nmigen/hdl/ast.py", line 253, in __getitem__ raise TypeError("Cannot index value with {}".format(repr(key))) TypeError: Cannot index value with (slice (sig rs) 0:8)
(In reply to Cole Poirier from comment #1) > The code below is what I have so far in my first attempt at solving this > problem: good for you! throw it into... mmm... let's see... soc/src/soc/logical/bperm.py something like that. > from nmigen import Elaboratable, Signal, Module, Repl, Cat > from nmigen.cli import main > > class Bpermd(Elaboratable): > def __init__(self, width): > self.perm = Signal(width) > self.rs = Signal(width) > self.ra = Signal(width) > self.rb = Signal(width) > > def elaborate(self, platform): > m = Module() > m.d.comb += self.perm.eq(Cat(0, Repl(8))) > index = Signal(8) > for i in range(0, 7 + 1): > index = rs[8 * i:8 * i + 7 + 1] > with m.If(index.lt(64)): > m.d.comb += self.perm[i].eq(rb[index]) > with m.Else(): > m.d.comb += self.perm[i].eq(0) > m.d.comb += ra.eq(Cat(Cat(0, Repl(56)),prem[0:8])) > return m > > if __name__ == "__main__": > bperm = Bpermd(width=8) > main(bperm, ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) > ``` > m.d.comb += self.perm.eq(Cat(0, Repl(8))) ok this needed to be: m.d.comb += self.perm.eq(Repl(Const(0, 1), 8))) or better just: m.d.comb += self.perm.eq(Const(0, 8)) but to be honest you do not need to set it at all. if not set, the default will be zero. > TypeError: __init__() missing 1 required positional argument: 'count' > ``` > > I don't understand why I am getting the error that I'm missing a positional > argument count in my __init__() function, since it only takes the parameters > self and width. Repl takes 2 arguments: the thing to replicate, and the number of times to replicate it. you passed only one argument. > I'm sure this error is just due to my not understanding > nmigen properly yet, so any help will be very much appreciated. change this with m.If(index.lt(64)): to this with m.If(index < 64): and this m.d.comb += ra.eq(Cat(Cat(0, Repl(56)),prem[0:8])) to just this: m.d.comb += ra[0:8].eq(perm) because you want the answer in the 1st 8 bits, and perm you know is 8 bits. actually you could just do ra.eq(perm) but nmigen might try to bit-extend perm out to 64 bits, and that's a waste, because, again, if not set, the bits will default to being set to zero. he said. they better be :)
(In reply to Cole Poirier from comment #3) > m.d.comb += self.perm[i].eq(self.rb[index]) > File "/home/colepoirier/src/nmigen/nmigen/hdl/ast.py", line 253, in > __getitem__ > raise TypeError("Cannot index value with {}".format(repr(key))) > TypeError: Cannot index value with (slice (sig rs) 0:8) err... err.... ah :) rrrright, you need to use nmigen.Array. basically: * create a list of 64 signals, each 1-bit wide, for-loop, append them each to the list * assign 1 bit of rb into each of those 64 (signal_1_bit.eq(rb[i]) * create the array: rb8 = Array(my_list_of_64_signals) *then* you can index them. however... be aware that this is an absolutely truly dreadful way to do it :) it will at least be functional and we can work on an improved design in a second iteration. basically it is absolutely awful because we are creating a *SIXTY FOUR* way crossbar... actually 8 such 64-way crossbars! this is pretty massive. however... before completely freaking out, it is worthwhile seeing what yosys actually generates (synth command). it *might* actually generate an efficient design. we have to see. if it really doesn't, then we can look around for alternatives. there might be something in clifford wolf's excellent bitmanip code. but - go through with this as it is, then write a unit test. you will then have "something to test an alternative design against", later.
(In reply to Luke Kenneth Casson Leighton from comment #4) > (In reply to Cole Poirier from comment #1) > good for you! throw it into... mmm... let's see... > soc/src/soc/logical/bperm.py Thank you so much Luke, am positively giddy at having written my first bit of nmigen HDL!!! (In reply to Luke Kenneth Casson Leighton from comment #5) > (In reply to Cole Poirier from comment #3) > err... err.... ah :) rrrright, you need to use nmigen.Array. > > basically: > > * create a list of 64 signals, each 1-bit wide, for-loop, append them each > to the > list > * assign 1 bit of rb into each of those 64 (signal_1_bit.eq(rb[i]) > * create the array: rb8 = Array(my_list_of_64_signals) > > *then* you can index them. > > however... be aware that this is an absolutely truly dreadful way to do it :) > it will at least be functional and we can work on an improved design in a > second iteration. > > basically it is absolutely awful because we are creating a *SIXTY FOUR* way > crossbar... actually 8 such 64-way crossbars! > > this is pretty massive. > > however... before completely freaking out, it is worthwhile seeing what > yosys actually generates (synth command). it *might* actually generate > an efficient design. we have to see. > > if it really doesn't, then we can look around for alternatives. there might > be something in clifford wolf's excellent bitmanip code. I looked up 'clifford wolf bitmanip' and found this https://github.com/riscv/riscv-bitmanip/blob/master/verilog/rvb_bextdep/rvb_bextdep.v which seems to implement the rvb equivalent of bperm, shfl (and unshfl). Wolf, who I believe from the copyright on this file now goes by Claire, wrote the riscv bitmanip extention proposal, which is also available in the linked repo in pre-built or self-built pdf form. Is this the bitmanip code you are referring to? > but - go through with this as it is, then write a unit test. you will then > have "something to test an alternative design against", later. I believe I have implemented the fixes you have suggested, but I'm really struggling with how to write an appropriate unit test, which prevents me from committing my code to your suggested location in the soc repo, if I'm recalling the HDL_Workflow development rules correctly. Can you point me to a resource or explain the basic principles or rules of writing hardware unit tests? I'm feeling at a total loss of where to start here. Additionally, pardon my ignorance, but are the unit tests supposed to be written inline or put in the tests directory of the working directory? (It wasn't obvious to me after examining the alu and experiment directories) Here is my attempt at the array code because I believe I can't yet commit it to the repo: ``` from nmigen import Elaboratable, Signal, Module, Repl, Cat, Const, Array from nmigen.cli import main class Bpermd(Elaboratable): def __init__(self, width): self.perm = Signal(width) self.rs = Signal(width) self.ra = Signal(width) self.rb = Signal(width) def elaborate(self, platform): m = Module() m.d.comb += self.perm.eq(Const(0,8)) index = Signal(8) signals = [ Signal(1) for i in range(0,64) ] for i,n in enumerate(signals): n.eq(self.rb[i]) rb8 = Array(signals) for i in range(0, 7 + 1): index = self.rs[8 * i:8 * i + 7 + 1] with m.If(index < 64): m.d.comb += self.perm[i].eq(rb8[index]) with m.Else(): m.d.comb += self.perm[i].eq(0) m.d.comb += self.ra[0:8].eq(self.perm) return m if __name__ == "__main__": bperm = Bpermd(width=64) main(bperm,ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) ```
(In reply to Cole Poirier from comment #6) > I looked up 'clifford wolf bitmanip' and found this > https://github.com/riscv/riscv-bitmanip/blob/master/verilog/rvb_bextdep/ > rvb_bextdep.v which seems to implement the rvb equivalent of bperm, shfl > (and unshfl). Wolf, who I believe from the copyright on this file now goes > by Claire, wrote the riscv bitmanip extention proposal, which is also > available in the linked repo in pre-built or self-built pdf form. Is this > the bitmanip code you are referring to? yes. > > but - go through with this as it is, then write a unit test. you will then > > have "something to test an alternative design against", later. > > I believe I have implemented the fixes you have suggested, but I'm really > struggling with how to write an appropriate unit test, which prevents me > from committing my code to your suggested location in the soc repo, if I'm > recalling the HDL_Workflow development rules correctly. you're not. if the code is unused by anyone (which in this case it is), you cannot cause anyone else "damage" or "inconvenience"... therefore commit it. right now. > Can you point me to > a resource or explain the basic principles or rules of writing hardware unit > tests? I'm feeling at a total loss of where to start here. Additionally, > pardon my ignorance, but are the unit tests supposed to be written inline or > put in the tests directory of the working directory? tests directory of the working directory. in this case, soc/src/logical/test as "test_bperm.py" or something. > Here is my attempt at the array code because I believe I can't yet commit it > to the repo: the very fact that you've cut/paste at least 3 variations into a *bugtracker* should tell you everything that you need to know. and that if your hard drive were to become corrupted, the only way for you to recover the work would be.... to extract the code... *from these comments*. that's s***, isn't it? :) therefore, clearly, you must have misunderstood. > ``` > from nmigen import Elaboratable, Signal, Module, Repl, Cat, Const, Array > from nmigen.cli import main > > class Bpermd(Elaboratable): > def __init__(self, width): > self.perm = Signal(width) > self.rs = Signal(width) > self.ra = Signal(width) > self.rb = Signal(width) > > def elaborate(self, platform): > m = Module() > m.d.comb += self.perm.eq(Const(0,8)) no need to set perm to 0. i said already. > index = Signal(8) > signals = [ Signal(1) for i in range(0,64) ] just range(64). no need to specify the default of 0 > for i,n in enumerate(signals): > n.eq(self.rb[i]) > rb8 = Array(signals) call it rb64 > for i in range(0, 7 + 1): you _can_ do this as "8", which is 7+1 :) > index = self.rs[8 * i:8 * i + 7 + 1] likewise here... > with m.If(index < 64): > m.d.comb += self.perm[i].eq(rb8[index]) > with m.Else(): > m.d.comb += self.perm[i].eq(0) again, no need to set something to zero when, if it is not set, it will default *to* zero. this btw only holds true for *combinatorial* logic. sync logic you *must* do zero-setting (etc) where needed. > m.d.comb += self.ra[0:8].eq(self.perm) looks good. > return m > > if __name__ == "__main__": > bperm = Bpermd(width=64) > main(bperm,ports=[bperm.perm, bperm.rs, bperm.ra, bperm.rb]) > ``` run python3 bperm.py generate -t il > bperm.il then use yosys to examine the graph (read_ilang bperm.il; show top) it will be fascinating to see.
(In reply to Luke Kenneth Casson Leighton from comment #7) > (In reply to Cole Poirier from comment #6) > you're not. if the code is unused by anyone (which in this case it is), > you cannot cause anyone else "damage" or "inconvenience"... therefore commit > it. right now. Indeed I did misunderstand, thank you for correcting me. Unfortunately, I just made the correction you suggested, and tried to push but I do not have push access rights to the soc repo, only the dev-env-setup repo. > > Additionally, pardon my ignorance, but are the unit tests supposed to > > be written inline or put in the tests directory of the working directory? > > tests directory of the working directory. in this case, soc/src/logical/test > as "test_bperm.py" or something. > > the very fact that you've cut/paste at least 3 variations into a *bugtracker* > should tell you everything that you need to know. > > and that if your hard drive were to become corrupted, the only way for you to > recover the work would be.... to extract the code... *from these comments*. > > that's s***, isn't it? :) > > therefore, clearly, you must have misunderstood. Very much so, I agree with your above logic, but due to my misunderstanding I was very afraid to commit something because I mistakenly thought it could have negative consequences. > again, no need to set something to zero when, if it is not set, it will > default *to* zero. > > this btw only holds true for *combinatorial* logic. sync logic you *must* > do zero-setting (etc) where needed. Thanks, I'll keep this in mind as I continue forwards, a very helpful tip! > run python3 bperm.py generate -t il > bperm.il then use yosys to examine the > graph (read_ilang bperm.il; show top) > > it will be fascinating to see. Ohhhboy... It worked! Very cool, however it is indeed a monster of a design
(In reply to Cole Poirier from comment #8) > (In reply to Luke Kenneth Casson Leighton from comment #7) > > (In reply to Cole Poirier from comment #6) > > you're not. if the code is unused by anyone (which in this case it is), > > you cannot cause anyone else "damage" or "inconvenience"... therefore commit > > it. right now. > > Indeed I did misunderstand, thank you for correcting me. Unfortunately, I > just made the correction you suggested, and tried to push but I do not have > push access rights to the soc repo, only the dev-env-setup repo. added you. > Very much so, I agree with your above logic, but due to my misunderstanding > I was very afraid to commit something because I mistakenly thought it could > have negative consequences. think in terms of multi-way collaboration: you need to do work, other people need to do work, the code under development needs to work. the guidelines (based on 20+ years of experience of working with software libre) balance all those three things. > > run python3 bperm.py generate -t il > bperm.il then use yosys to examine the > > graph (read_ilang bperm.il; show top) > > > > it will be fascinating to see. > > Ohhhboy... It worked! Very cool, however it is indeed a monster of a design yyep. to be expected. clifford's bperm code is equally massive. you might want to try running these: * proc * opt * show top and if you *really* want to put your computer into meltdown, run "synth" followed by "show top". just from a few lines of python, eh? shows how careful you have to be when working in H(igh) D(efinition) L(anguage)s.
(In reply to Luke Kenneth Casson Leighton from comment #9) > (In reply to Cole Poirier from comment #8) > added you. Awesome! It worked :) > think in terms of multi-way collaboration: you need to do work, other people > need to do work, the code under development needs to work. > > the guidelines (based on 20+ years of experience of working with software > libre) balance all those three things. I'm with you fully Luke. I try to follow your guidelines as best as I can. > > Ohhhboy... It worked! Very cool, however it is indeed a monster of a design > > yyep. to be expected. clifford's bperm code is equally massive. > > you might want to try running these: > > * proc > * opt > * show top > > and if you *really* want to put your computer into meltdown, run "synth" > followed by "show top". I just might try it. > just from a few lines of python, eh? shows how careful you have to be > when working in H(igh) D(efinition) L(anguage)s. It really is incredible. Looking forward to improving the level of care I am capable of taking with regard to HDL.
(In reply to Cole Poirier from comment #10) > (In reply to Luke Kenneth Casson Leighton from comment #9) > > (In reply to Cole Poirier from comment #8) > > added you. > > Awesome! It worked :) exxxcellent. muhahaha. > > > think in terms of multi-way collaboration: you need to do work, other people > > need to do work, the code under development needs to work. > > > > the guidelines (based on 20+ years of experience of working with software > > libre) balance all those three things. > > I'm with you fully Luke. I try to follow your guidelines as best as I can. i am inviting you to think for yourself, to derive them from first principles and thus be able, if there are any... unusual circumstances, to not be either frozen solid or disruptive. > > and if you *really* want to put your computer into meltdown, run "synth" > > followed by "show top". > > I just might try it. be prepared to have to run "killall xdot". > > > just from a few lines of python, eh? shows how careful you have to be > > when working in H(igh) D(efinition) L(anguage)s. > > It really is incredible. Looking forward to improving the level of care I am > capable of taking with regard to HDL. if you at least run "show top" and also inspect submodules visually ("show presstabkey presstabkey") and if you can relate what you see back to the actual code and still follow the graph, the design is "clean". if however you cannot see the graph even at fullscreen because boxes are too small even on a 1920x1080 screen, then something is wrong, you need to break it down into smaller submodules. if possible. or in this particular case, redesign it. but not right now. write unit test first. research examples on how to do that ok?
you forgot this. do a git pull in a moment... diff --git a/src/soc/logical/bperm.py b/src/soc/logical/bperm.py index 1dcb36d..05321e5 100644 --- a/src/soc/logical/bperm.py +++ b/src/soc/logical/bperm.py @@ -37,7 +37,7 @@ class Bpermd(Elaboratable): index = Signal(8) signals = [ Signal(1) for i in range(64) ] for i,n in enumerate(signals): - n.eq(self.rb[i]) + m.d.comb += n.eq(self.rb[i]) rb64 = Array(signals) for i in range(0, 8): index = self.rs[8 * i:8 * i + 8]
ok. right. re-run the generate -t ilang, and yosys show top. then trace "rs", note how there are *two* copies of 8-bit chunks of rs? one that goes into the "lt" (less-than) comparison, and a *second* copy that goes into the the big "group" (this is a massive multiplexer btw) that's 2x copies of 8 8-bit chunks. so let's trace it back. what thing or things - related to rs - have an 8-bit width? well, that will be index, won't it? index = self.rs[8 * i:8 * i + 8] now, look where index is used. first time: with m.If(index < 64): that's where the lt (less-than) comes in (times 8) second time: (rb64[index]) this is really important to note the difference between a *python* variable and a nmigen Abstract Syntax Tree code-fragment. you have created - with the "index = self.rs[blah blah]" a *python* variable assignment from a *nmigen AST*. therefore, whereever you use that python variable it INSERTS A COPY OF THAT NMIGEN AST... into more nmigen AST. now, in this particular case, that's fine (it's not a pretty graph) but in cases where you did something like this: index = Cat(rs[blah], 5) * i + rb[i] * 3, rs[i] & rb[i]) or anything hugely and massively complex, that would ALSO GET INSERTED TWICE and you would end up with a huge duplication of gate logic as a result, which yosys would be very unlikely to spot and optimise away. the solution - therefore - the best practice - is never to assign anything other than the most basic of nmigen objects - Signals, Consts, Records etc. - to a python variable OR to actually create a Signal into which that nmigen AST fragment is assigned... *and then use that signal*. in this case that would be: index = ... idx = Signal(8, name="idx%d" % i, reset_less=True) m.d.comb += idx.eq(index) and then m.If(idx < 64) and also rb64[idx] see what difference that makes to the graphviz, ok?
for i in range(0, 8): just for i in range(8):
i've put a stack of TODO comments in for you. always remember to "git pull" before doing any editing. keep people informed what you are doing, "i am going to edit this file, now" for example, because this will help you to avoid edit-conflicts (because the other person knows to coordinate with you). for example, if you had fixed the thing in the previous comment *without* a "git pull", committed it, *then* tried "git pull" you would now have a conflict to resolve, because you edited the exact same line that i had also edited. we will soon see if you are checking the bugtracker and reading all comments... :)
(In reply to Luke Kenneth Casson Leighton from comment #15) > i've put a stack of TODO comments in for you. always remember to "git pull" > before doing any editing. keep people informed what you are doing, > "i am going to edit this file, now" for example, because this will help you > to avoid edit-conflicts (because the other person knows to coordinate with > you). > > for example, if you had fixed the thing in the previous comment *without* > a "git pull", committed it, *then* tried "git pull" you would now have > a conflict to resolve, because you edited the exact same line that i had > also edited. > > we will soon see if you are checking the bugtracker and reading all > comments... :) Thank you for the very helpful TODOs Luke. I think I've made the necessary changes, and the graph looked quite different as a made each change. Especially the first one, as prior to that as you had noted I had neglected to 'connect' a key component. ``` for i,n in enumerate(signals): - n.eq(self.rb[i]) + m.d.comb += n.eq(self.rb[i]) ``` I have committed the changes. Now I am going to go over Robert Baruch's nmigen tutorials and search out resources on writing unit tests, and formal proofs for hardware. Then I will attempt to write an appropriate unit test for this class.
(In reply to Cole Poirier from comment #16) > I have committed the changes. fantastic: feel free to do another "git pull" because i just made some PEP8-like changes. btw notice in cr/main_stage.py, michael also does the same "indexing" trick :) in particular notice what he does with the name argument: cr_out_arr = Array([Signal(name=f"cr_out_{i}") for i in range(32)]) if you try that out you will end up with actual properly-named Signals rather than "stuff that's randomly named $1, $2, $3.... $64". > Now I am going to go over Robert Baruch's > nmigen tutorials and search out resources on writing unit tests, and formal > proofs for hardware. Then I will attempt to write an appropriate unit test > for this class. great. formal proofs are... odd. i can barely get my head round them.
(In reply to Luke Kenneth Casson Leighton from comment #17) > (In reply to Cole Poirier from comment #16) > > btw notice in cr/main_stage.py, michael also does the same "indexing" trick > :) > in particular notice what he does with the name argument: > > cr_out_arr = Array([Signal(name=f"cr_out_{i}") for i in range(32)]) > > if you try that out you will end up with actual properly-named Signals rather > than "stuff that's randomly named $1, $2, $3.... $64". ROFL, I got the idea of using Arrays from your conversations yesterday. > > > > Now I am going to go over Robert Baruch's > > nmigen tutorials and search out resources on writing unit tests, and formal > > proofs for hardware. Then I will attempt to write an appropriate unit test > > for this class. > > great. formal proofs are... odd. i can barely get my head round them. I'd be happy to help with formal proofs when you're ready.
(In reply to Cole Poirier from comment #16) > > I have committed the changes. Now I am going to go over Robert Baruch's > nmigen tutorials and search out resources on writing unit tests, and formal > proofs for hardware. Then I will attempt to write an appropriate unit test > for this class. For writing unit tests, take a look at https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937;hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place
(In reply to Michael Nolan from comment #18) > ROFL, I got the idea of using Arrays from your conversations yesterday. :) > I'd be happy to help with formal proofs when you're ready. really appreciated. (In reply to Michael Nolan from comment #19) > For writing unit tests, take a look at > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/ > test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937; > hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place Cole that's a really good template to start from. (*sotto voice to michael*: i tend to just set mb = dut.mb as a temp python variable, and do "yield dut.o" rather than spend the time setting up copies of things that you can get at directly anyway). so, Cole, note two things: 1) the establishment of the "DUT" - Device Under Test. the "yield" statements to set the inputs, and the additional "yield" statement to obtain the output 2) the use of a **PYTHON** function - not a nmigen function - which computes the expected result. this function - MASK() in this example by Michael - is given the EXACT SAME INPUT as was handed to the hardware. thus you have an "expected" result (done in python) and a "hardware-simulated" result. if those two do not match, throw a python unittest assert. simple. except, it is necessary to write a *lot* of these, catching and testing different aspects of the hardware. this is why we want to do Formal Proofs, because one Formal unit test, if written correctly, covers *everything*.
(In reply to Michael Nolan from comment #19) > (In reply to Cole Poirier from comment #16) > > > > I have committed the changes. Now I am going to go over Robert Baruch's > > nmigen tutorials and search out resources on writing unit tests, and formal > > proofs for hardware. Then I will attempt to write an appropriate unit test > > for this class. > > For writing unit tests, take a look at > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/ > test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937; > hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place Thanks Michael! This looks like it will be really helpful. (In reply to Michael Nolan from comment #18) > (In reply to Luke Kenneth Casson Leighton from comment #17) > > (In reply to Cole Poirier from comment #16) > > > > > btw notice in cr/main_stage.py, michael also does the same "indexing" trick > > :) > > in particular notice what he does with the name argument: > > > > cr_out_arr = Array([Signal(name=f"cr_out_{i}") for i in range(32)]) > > > > if you try that out you will end up with actual properly-named Signals rather > > than "stuff that's randomly named $1, $2, $3.... $64". > > ROFL, I got the idea of using Arrays from your conversations yesterday. I just pushed I commit where I have tried to copy this, although I'm unsure if I did it correctly, because rb_{n} shows up correctly in the graph, but I see no idx_{n}'s. I took a second look at my code after using yosys to examine it, and I'm not able to discern why idx would not show up... I just took a third look and realized it was because I had neglected to delete my temporary assignment of an 8-bit wide Signal from my first iteration to the variable index, which I was actually using within the body of the for loop that makes up the bulk of the function. Now both labels show up correctly. I have pushed this new commit. > > great. formal proofs are... odd. i can barely get my head round them. Yeah.. I have the feeling that I'm wading into quite strange waters here :) > I'd be happy to help with formal proofs when you're ready. Thanks again Michael, I'm looking forward to working with you and learning from your knowledge and experience. I have a prior obligation, so I'll have to push writing the unit test until tomorrow. But, for my own understanding, once I have the unit test is working, would it be wiser to search for optimization opportunities, for example from Claire Wolf's bitmanip code, or to write the formal proof? I'm guessing that the formal proof is specific to the function's implementation and thus I should wait to write the formal proof until the function is optimized but I am not sure. (In reply to Luke Kenneth Casson Leighton from comment #17) > (In reply to Cole Poirier from comment #16) > > > I have committed the changes. > > fantastic: feel free to do another "git pull" because i just made some > PEP8-like > changes. Thanks Luke, and apologies for not perfectly conforming to PEP8 yet, I'm working on getting my autopep8 working but have run into a problem, I should have it sorted tomorrow.
(In reply to Luke Kenneth Casson Leighton from comment #20) > (In reply to Michael Nolan from comment #18) > > > ROFL, I got the idea of using Arrays from your conversations yesterday. > > :) > > > I'd be happy to help with formal proofs when you're ready. > > really appreciated. (In reply to Michael Nolan from comment #19) > > > > For writing unit tests, take a look at > > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/shift_rot/test/ > > test_maskgen.py;h=1a4d34e676154b250f95ef120932a9b88fcaf937; > > hb=3c65f5ff7893bb34696c476abacfe34ad739bf18 for decent starting place > > Cole that's a really good template to start from. > > (*sotto voice to michael*: i tend to just set mb = dut.mb as a temp > python variable, and do "yield dut.o" rather than spend the time > setting up copies of things that you can get at directly anyway). > > so, Cole, note two things: > > 1) the establishment of the "DUT" - Device Under Test. the "yield" > statements to set the inputs, and the additional "yield" statement > to obtain the output > > 2) the use of a **PYTHON** function - not a nmigen function - which > computes the expected result. this function - MASK() in this > example by Michael - is given the EXACT SAME INPUT as was handed > to the hardware. > > thus you have an "expected" result (done in python) and a > "hardware-simulated" > result. > > if those two do not match, throw a python unittest assert. > > simple. > > except, it is necessary to write a *lot* of these, catching and testing > different aspects of the hardware. > > this is why we want to do Formal Proofs, because one Formal unit test, > if written correctly, covers *everything*. Ah, thank you very much for these additional details Luke. Everything the both of you (and Yehowshua) have said is proving critical to my ability to quickly (or slowly...) get going with the various required aspects of our HDL_workflow. Once I have finished this first small 'project'/assignment, I'd like to pause for a few hours and update the documentation of the HDL_workflow with the things I learned while scripting it, as well as all that I've learned in this assignment. Some of this exists elsewhere on the wiki, however, most of the getting started with nmigen stuff I've learned in the past two days does not (as far as I am aware) and I believe this will be valuable to new members. But right now I have a prior engagement I must attend to, so I'll attempt an initial unit test tomorrow :)
(In reply to Luke Kenneth Casson Leighton from comment #20) > Cole that's a really good template to start from. > > (*sotto voice to michael*: i tend to just set mb = dut.mb as a temp > python variable, and do "yield dut.o" rather than spend the time > setting up copies of things that you can get at directly anyway). I think I did this because when I was first starting nmigen there was a bug where the vcd dump didn't show the top level signals unless you did this. I haven't seen it happen in a while so maybe it's fixed...? > except, it is necessary to write a *lot* of these, catching and testing > different aspects of the hardware. > > this is why we want to do Formal Proofs, because one Formal unit test, > if written correctly, covers *everything*. I haven't closely examined bpermd, but for maskgen I didn't bother writing a proof because it was easy and quick enough to exhaustively test the input space. I suspect you won't be able to do that for bpermd though.
(In reply to Michael Nolan from comment #23) > (In reply to Luke Kenneth Casson Leighton from comment #20) > > > Cole that's a really good template to start from. > > > > (*sotto voice to michael*: i tend to just set mb = dut.mb as a temp > > python variable, and do "yield dut.o" rather than spend the time > > setting up copies of things that you can get at directly anyway). > > I think I did this because when I was first starting nmigen there was a bug > where the vcd dump didn't show the top level signals unless you did this. ah HA! i half-expected that might be why. > I haven't seen it happen in a while so maybe it's fixed...? it's not. if you can see if there's a bugreport raised for nmigen, and cross-reference the discussion here, that would be really handy. > > this is why we want to do Formal Proofs, because one Formal unit test, > > if written correctly, covers *everything*. > > I haven't closely examined bpermd, but for maskgen I didn't bother writing a > proof because it was easy and quick enough to exhaustively test the input > space. I suspect you won't be able to do that for bpermd though. yehyeh. Cole: maskgen is... 8-bit wide? so running 2x for-loops @ 256 x 256 cycles, for such a small amount of code that's perfectly feasible. however if it was say 64-bit wide? (as is the case for bpermd) - that's flat-out impractical. we can't possibly run 2^64 times 2^64 clock cycles to cover all permutations for inputs. hence: formal proofs
rb64 = Array([Signal(1, reset_less=True, name=f"rb64_{i}") for i in range(64)]) Cole, this is over the 80-char limit. this is why i recommended split it into two: setting up a list, followed by assigning the list to an array. also, *because* it is assigned to an Array, this code: for i in range(64): m.d.comb += rb64[i].eq(self.rb[i]) might actually try to generate an Array-assigning method of setting the 64 elements. you'll have to check the graphviz the *possibility* of that occurring is why i recommended it to be done as: rb64 = [Signal.... for i in range(64)] for i in range(64): m.d.comb += rb64[i].eq(self.rb[i]) rb64 = Array(rb64) see the difference? this one is assigning to signals that, oh look, they happen to be in a python list. the one that you did, the signals are assigned *via the nmigen Array*. and the code is violating PEP8 by being over 80 chars in length.
(In reply to Cole Poirier from comment #21) > Yeah.. I have the feeling that I'm wading into quite strange waters here :) > > > I'd be happy to help with formal proofs when you're ready. > > Thanks again Michael, I'm looking forward to working with you and learning > from your knowledge and experience. I have a prior obligation, so I'll have > to push writing the unit test until tomorrow. But, for my own understanding, > once I have the unit test is working, would it be wiser to search for > optimization opportunities, for example from Claire Wolf's bitmanip code, or > to write the formal proof? I'm guessing that the formal proof is specific to > the function's implementation and thus I should wait to write the formal > proof until the function is optimized but I am not sure. > Cole, I added a skeleton proof module for bperm.py here https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/logical/formal/proof_bperm.py;h=da198940f75b3868ca864f1d75c6e99c55b1f073;hb=HEAD with a bunch of comments on how to finish the formal proof. Take a look when you get around to it, and let me know if you have problems.
(In reply to Luke Kenneth Casson Leighton from comment #25) > rb64 = Array([Signal(1, reset_less=True, name=f"rb64_{i}") for i in > range(64)]) > > Cole, this is over the 80-char limit. > > this is why i recommended split it into two: setting up a list, > followed by assigning the list to an array. > > also, *because* it is assigned to an Array, this code: > > for i in range(64): > m.d.comb += rb64[i].eq(self.rb[i]) > > might actually try to generate an Array-assigning method of setting > the 64 elements. you'll have to check the graphviz > > the *possibility* of that occurring is why i recommended it to be done as: > > rb64 = [Signal.... for i in range(64)] > for i in range(64): > m.d.comb += rb64[i].eq(self.rb[i]) > rb64 = Array(rb64) > > see the difference? this one is assigning to signals that, oh look, > they happen to be in a python list. > > the one that you did, the signals are assigned *via the nmigen Array*. > > and the code is violating PEP8 by being over 80 chars in length. Thanks for catching this error Luke. I have made the modification you recommended, and run autopep8 on the file to ensure proper conformance to formatting rules. I'm still learning how to read yosys dot diagrams, but it does appear that this modification changes the graph, so it is possible that array-assigning methods were being generated.
(In reply to Michael Nolan from comment #26) > (In reply to Cole Poirier from comment #21) > > Yeah.. I have the feeling that I'm wading into quite strange waters here :) > > > > > I'd be happy to help with formal proofs when you're ready. > > > > Thanks again Michael, I'm looking forward to working with you and learning > > from your knowledge and experience. I have a prior obligation, so I'll have > > to push writing the unit test until tomorrow. But, for my own understanding, > > once I have the unit test is working, would it be wiser to search for > > optimization opportunities, for example from Claire Wolf's bitmanip code, or > > to write the formal proof? I'm guessing that the formal proof is specific to > > the function's implementation and thus I should wait to write the formal > > proof until the function is optimized but I am not sure. > > > > Cole, I added a skeleton proof module for bperm.py here > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/logical/formal/ > proof_bperm.py;h=da198940f75b3868ca864f1d75c6e99c55b1f073;hb=HEAD with a > bunch of comments on how to finish the formal proof. Take a look when you > get around to it, and let me know if you have problems. Thank you! Thank you! Thank you! This is honestly unbelievable Michael, I am so grateful for your very generous help. I'm going over the proof skeleton now, about to start working on the second proof assertion that you've given me a very good starting point for. I'll be sure to let you know once I have something... or if I have a significant problem.
Hi Michael, is there an argument that needs to be passed in order to run the formal proof, or a config.sby file? I'm currently trying 'python3 proof_bperm.py' which gives me an error about a missing file... I'm pulling my hair out trying to figure out which file it's looking for. ``` E. ====================================================================== ERROR: test_formal (__main__.TestCase) ---------------------------------------------------------------------- Traceback (most recent call last): File "proof_bperm.py", line 112, in test_formal self.assertFormal(module, mode="bmc", depth=2) File "/home/colepoirier/src/nmigen/nmigen/test/utils.py", line 100, in assertFormal stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc: File "/usr/lib/python3.7/subprocess.py", line 775, in __init__ restore_signals, start_new_session) File "/usr/lib/python3.7/subprocess.py", line 1522, in _execute_child raise child_exception_type(errno_num, err_msg, err_filename) FileNotFoundError: [Errno 2] No such file or directory: '': '' ---------------------------------------------------------------------- Ran 2 tests in 0.479s FAILED (errors=1) ```
(In reply to Cole Poirier from comment #29) > Hi Michael, is there an argument that needs to be passed in order to run the > formal proof, or a config.sby file? I'm currently trying 'python3 > proof_bperm.py' which gives me an error about a missing file... I'm pulling > my hair out trying to figure out which file it's looking for. > > ``` > E. > ====================================================================== > ERROR: test_formal (__main__.TestCase) > ---------------------------------------------------------------------- > Traceback (most recent call last): > File "proof_bperm.py", line 112, in test_formal > self.assertFormal(module, mode="bmc", depth=2) > File "/home/colepoirier/src/nmigen/nmigen/test/utils.py", line 100, in > assertFormal > stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc: > File "/usr/lib/python3.7/subprocess.py", line 775, in __init__ > restore_signals, start_new_session) > File "/usr/lib/python3.7/subprocess.py", line 1522, in _execute_child > raise child_exception_type(errno_num, err_msg, err_filename) > FileNotFoundError: [Errno 2] No such file or directory: '': '' > > ---------------------------------------------------------------------- > Ran 2 tests in 0.479s > > FAILED (errors=1) > ``` Nope, no arguments needed. I ran into this error a while ago, it's something to do with symbiyosys not finding a file. I'm not sure how it got fixed though, as it seemed to resolve itself. Are you using the latest nmigen, installed from the git repo?
try running a different formal test that is known to already work.
(In reply to Luke Kenneth Casson Leighton from comment #31) > try running a different formal test that is known to already work. Unfortunately, after several hours and multiple re-installations of nmigen, nmutil, ieee754fpu, soc, yosys, symbiyosys, and dist-packages cleanings, when trying to run known working proof '~/src/soc/src/soc/decoder/formal$ python3.7 proof_decoder.py' I get the same error with the following output: ``` mask 0x1f E ====================================================================== ERROR: test_decoder (__main__.DecoderTestCase) ---------------------------------------------------------------------- Traceback (most recent call last): File "proof_decoder.py", line 125, in test_decoder self.assertFormal(module, mode="bmc", depth=4) File "/home/colepoirier/src/nmigen/nmigen/test/utils.py", line 100, in assertFormal stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc: File "/usr/lib/python3.7/subprocess.py", line 775, in __init__ restore_signals, start_new_session) File "/usr/lib/python3.7/subprocess.py", line 1522, in _execute_child raise child_exception_type(errno_num, err_msg, err_filename) FileNotFoundError: [Errno 2] No such file or directory: '': '' ---------------------------------------------------------------------- Ran 1 test in 3.459s FAILED (errors=1) ```
Cole, one critically important thing that you need to learn as a "first reaction" is to go through every single file, at every single line, on a stack trace, actually seeing what that line (and nearby) actually does. here is the relevant line of nmigen.test.utils: with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name], cwd=spec_dir, universal_newlines=True, stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc: stdout, stderr = proc.communicate(config) also, that it is perfectly find to insert debug print statements into that code in order to find out what is going on. for example, do this: sbytool = require_tool("sby") print ("sby tool blah blah", sbytool, spec_name, spec_dir) with subprocess.Popen([sbytool, "-f", "-d", spec_name], .... then, if that is not obvious what is going on, drill down into require_tool, which can be found in nmigen/_toolchain.py and there, start dropping in a ton of print debug statements that tell you what is going on. print ("env_var", env_var) print path print shutil.which(path) print os.environ.keys() etc blah blah blah further up the assertFormal function, start dropping in print statements there. basically, when you've done all that, try this: lkcl@fizzy:~/src/libresoc/soc/src/soc/logical/formal$ python3 proof_bperm.py and: lkcl@fizzy:~/src/libresoc/soc/src/soc/logical/formal$ cd .. lkcl@fizzy:~/src/libresoc/soc/src/soc/logical$ python3 logical/proof_bperm.py and tell me what happens in each case.
(In reply to Luke Kenneth Casson Leighton from comment #33) > Cole, one critically important thing that you need to learn as a "first > reaction" > is to go through every single file, at every single line, on a stack trace, > actually seeing what that line (and nearby) actually does. > > here is the relevant line of nmigen.test.utils: > > with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name], > cwd=spec_dir, > universal_newlines=True, > stdin=subprocess.PIPE, stdout=subprocess.PIPE) > as proc: > stdout, stderr = proc.communicate(config) > > also, that it is perfectly find to insert debug print statements into that > code in order to find out what is going on. > > for example, do this: > > sbytool = require_tool("sby") > print ("sby tool blah blah", sbytool, spec_name, spec_dir) > with subprocess.Popen([sbytool, "-f", "-d", spec_name], .... > > > then, if that is not obvious what is going on, drill down into require_tool, > which can be found in nmigen/_toolchain.py > > and there, start dropping in a ton of print debug statements that tell you > what is going on. > > print ("env_var", env_var) > print path > print shutil.which(path) > print os.environ.keys() > > etc blah blah blah > > further up the assertFormal function, start dropping in print statements > there. > > basically, when you've done all that, try this: > > lkcl@fizzy:~/src/libresoc/soc/src/soc/logical/formal$ python3 proof_bperm.py > > and: > > lkcl@fizzy:~/src/libresoc/soc/src/soc/logical/formal$ cd .. > lkcl@fizzy:~/src/libresoc/soc/src/soc/logical$ python3 logical/proof_bperm.py > > and tell me what happens in each case. Ah yes, classic python debugging print over here, print over there, print everywhere! I thought I was doing something trivially wrong. Will deep dive now. Thank you for the guidance. Will report back shortly.
Thank you for the guidance to do standard python debugging, found the bug and fixed it in minutes. The key turned out to be adding os.realpath() at the top of the assertFormal() function: ``` def assertFormal(self, spec, mode="bmc", depth=1): caller, *_ = traceback.extract_stack(limit=2) spec_root, _ = os.path.splitext(caller.filename) - spec_dir = os.path.dirname(spec_root) + spec_dir = os.path.dirname(os.path.realpath(spec_root)) spec_name = "{}_{}".format( os.path.basename(spec_root).replace("test_", "spec_"), caller.name.replace("test_", "") ) [snip..] ``` Should I make a PR to nmigen with this fix? I'm stopping work for today. Will pick this up and make my 'real' first proof attempt in the morning.
(In reply to Cole Poirier from comment #35) > Thank you for the guidance to do standard python debugging, found the bug > and fixed it in minutes. ta-daaa :) > Should I make a PR to nmigen with this fix? of course! and next time, don't ask, just do it :) > I'm stopping work for today. Will pick this up and make my 'real' first > proof attempt in the morning. great. it's kinda cool, isn't it?
(In reply to Luke Kenneth Casson Leighton from comment #36) > (In reply to Cole Poirier from comment #35) > > Thank you for the guidance to do standard python debugging, found the bug > > and fixed it in minutes. > > ta-daaa :) > > > > Should I make a PR to nmigen with this fix? > > of course! and next time, don't ask, just do it :) Just did, and will do in the future, still getting my... cirucuit-legs so to speak :) > > I'm stopping work for today. Will pick this up and make my 'real' first > > proof attempt in the morning. > > great. it's kinda cool, isn't it? It's fantastically cool! I can't wait to work on this tomorrow, would keep working now, but I must give my brain some rest.
cole i moved the soc.logical.bperm code into soc.fu.logical.bperm can i leave it with you to update the imports?
(In reply to Luke Kenneth Casson Leighton from comment #38) > cole i moved the soc.logical.bperm code into soc.fu.logical.bperm > can i leave it with you to update the imports? Just went to do this, but it appears you or someone else has already done this. Thank you. Going to start working on the formal proof now.
Hi Michael, I have finally run the formal proof 'proof_bperm.py' and gotten a failure with the following in its output: ``` SBY 15:20:39 [proof_bperm_formal] engine_0: ## 0:00:00 BMC failed! SBY 15:20:39 [proof_bperm_formal] engine_0: ## 0:00:00 Value for anyconst in top (proof_bperm.py:56): 15481123719086080 SBY 15:20:39 [proof_bperm_formal] engine_0: ## 0:00:00 Value for anyconst in top (proof_bperm.py:57): 36028797018963968 SBY 15:20:39 [proof_bperm_formal] engine_0: ## 0:00:00 Assert failed in top: proof_bperm.py:93 ``` I feel like I have misunderstood your directions for proving property #2, am I extracting the indices incorrectly? Or am I making a different fundamental mistake? 84 # Now we need to prove property #2. I'm going to leave this to 85 # you Cole. I'd start by writing a for loop and extracting the 86 # 8 indices into signals. Then I'd write an if statement 87 # checking if the index is >= 64 (it's hardware, so use an 88 # m.If()). Finally, I'd add an assert that checks whether 89 # ra[i] is equal to 0 90 for i in range(8): 91 index = rb[i*8:i*8+8] 92 with m.If(index >= 64): 93 comb += Assert(ra[i] == 0) 94 95 96 return m
(In reply to Cole Poirier from comment #40) > > I feel like I have misunderstood your directions for proving property #2, am > I extracting the indices incorrectly? Or am I making a different fundamental > mistake? > > 84 # Now we need to prove property #2. I'm going to leave this to > 85 # you Cole. I'd start by writing a for loop and extracting the > 86 # 8 indices into signals. Then I'd write an if statement > 87 # checking if the index is >= 64 (it's hardware, so use an > 88 # m.If()). Finally, I'd add an assert that checks whether > 89 # ra[i] is equal to 0 > 90 for i in range(8): > 91 index = rb[i*8:i*8+8] > 92 with m.If(index >= 64): > 93 comb += Assert(ra[i] == 0) > 94 > 95 > 96 return m No, that is about what I would have written. What I would suggest to you is to open the trace yosys generated (should be in proof_bperm_formal/engine_0/trace.vcd) and see why it's not working. Looking at it on my machine... double check that you're generating the `index` correctly in the proof.
(In reply to Michael Nolan from comment #41) > No, that is about what I would have written. What I would suggest to you is > to open the trace yosys generated (should be in > proof_bperm_formal/engine_0/trace.vcd) and see why it's not working. > > > Looking at it on my machine... double check that you're generating the > `index` correctly in the proof. When I look at trace.vcd by running 'gtkwave proof_bperm_formal/engine_0/trace.vcd' and clicking to expose the bperm module under top, then selecting and adding all the wires, all I see is, what I presume out of ignorance is the initial state of the wires, and I can advance to the next edge where the wires are in their 'final' state, and that's it... I'm assuming since this is a combinatorial single cycle proof that's what I'm supposed to see? How should I be reading the gtkwave diagram in order to diagnose that index is not being set correctly in the proof? Above, you said that doing 'index = rb[i*8:i*8+8]' within a for loop where i counts from 0 to 7 was what you would have done... is this shown by the vcd output to now be incorrect? How would I go about discerning that I'm generating the `index` correctly in the proof? I'm sorry that these are stupid questions that likely have obvious answers, but I'm struggling to determine them on my own reading through the gtkwave manual.
(In reply to Cole Poirier from comment #42) > (In reply to Michael Nolan from comment #41) > > No, that is about what I would have written. What I would suggest to you is > > to open the trace yosys generated (should be in > > proof_bperm_formal/engine_0/trace.vcd) and see why it's not working. > > > > > > Looking at it on my machine... double check that you're generating the > > `index` correctly in the proof. > > When I look at trace.vcd by running 'gtkwave > proof_bperm_formal/engine_0/trace.vcd' and clicking to expose the bperm > module under top, then selecting and adding all the wires, all I see is, > what I presume out of ignorance is the initial state of the wires, and I can > advance to the next edge where the wires are in their 'final' state, and > that's it... I'm assuming since this is a combinatorial single cycle proof > that's what I'm supposed to see? How should I be reading the gtkwave diagram > in order to diagnose that index is not being set correctly in the proof? For a combinatorial circuit like this one, the inputs (rs and rb) are set to their initial values, and the outputs (ra) are set to whatever the circuit calculates from the inputs. > > Above, you said that doing 'index = rb[i*8:i*8+8]' within a for loop where i > counts from 0 to 7 was what you would have done... is this shown by the vcd > output to now be incorrect? How would I go about discerning that I'm > generating the `index` correctly in the proof? I'm sorry that these are > stupid questions that likely have obvious answers, but I'm struggling to > determine them on my own reading through the gtkwave manual. In the proof, you're generating the index from rb, but in the actual module and the Power spec, it's generated from rs. That's why the proof fails. If you look at the index variables (for me it's index 6), you'll notice that one is less than 64 - that's how I figured it out.
(In reply to Michael Nolan from comment #43) > (In reply to Cole Poirier from comment #42) > For a combinatorial circuit like this one, the inputs (rs and rb) are set to > their initial values, and the outputs (ra) are set to whatever the circuit > calculates from the inputs. Thank you for this clarification, I think I am missing some of the basic background knowledge of registers/assembly, should I just do some background reading on wikipedia, or is there a better resource you or luke can point me to, or should I simply study OPF ISA Spec v3.1? > In the proof, you're generating the index from rb, but in the actual module > and the Power spec, it's generated from rs. That's why the proof fails. If > you look at the index variables (for me it's index 6), you'll notice that > one is less than 64 - that's how I figured it out. That makes sense. I didn't catch this because all other idx_n's were 00, and idx_6 was 37. 37 is less than 64, but is 00 not also less than 64 correct? I'm confused by this so your clarification would be very helpful. I'd like to clarify one other thing so I don't repeat this same mistake. In the skeleton you provided the below pseudo code and assertion properties. # The pseudocode in the Power ISA manual (v3.1) is as follows: 61 # do i = 0 to 7 62 # index <- RS[8*i:8*i+8] 63 # if index < 64: 64 # perm[i] <- RB[index] 65 # else: 66 # perm[i] <- 0 67 # RA <- 56'b0 || perm[0:8] # big endian though 68 69 # Looking at this, I can identify 3 properties that the bperm 70 # module should keep: 71 # 1. RA[8:64] should always equal 0 72 # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 73 # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] For 2 and 3 should RB[i*8:i*8+8] actually be RS[i*8:i*8+8]? Or am I failing to properly read/interpret the 'formalism'? In other words, I'm very confused and looking for a way to better understand what I am doing, and what I am supposed to be doing.
err *cough* really-bad-hack mumble *cough* index 453e419..0f879e3 100644 --- a/src/soc/fu/logical/formal/proof_bperm.py +++ b/src/soc/fu/logical/formal/proof_bperm.py @@ -88,9 +88,15 @@ class Driver(Elaboratable): # m.If()). Finally, I'd add an assert that checks whether # ra[i] is equal to 0 for i in range(8): - index = rb[i*8:i*8+8] + index = rs[i*8:i*8+8] with m.If(index >= 64): comb += Assert(ra[i] == 0) + with m.Else(): + # to avoid having to create an Array of rb, + # cycle through from 0-63 on the index *whistle nonchalantly* + for j in range(64): + with m.If(index == j): + comb += Assert(ra[i] == rb[j]) return m
(In reply to Cole Poirier from comment #44) > 71 # 1. RA[8:64] should always equal 0 > 72 # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 > 73 # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] > > For 2 and 3 should RB[i*8:i*8+8] actually be RS[i*8:i*8+8]? yes. > Or am I failing > to properly read/interpret the 'formalism'? In other words, I'm very > confused and looking for a way to better understand what I am doing, and > what I am supposed to be doing. you are expressing the expectations about the inputs and outputs of the module. these you express as assertions that must be true. (sby then checks those for you under *all* possible values of input and output). therefore you not only need to get the code right, you actually need to properly understand what it does... and express that in the assertions. example. from this line of code, is it *ever* possible that bits 8 and above will be *anything* other than zero? m.d.comb += self.ra[0:8].eq(perm) answer: no it is not. *therefore make an assertion about that*: comb += Assert(self.ra[8:] == 0) now let us move on to when any given "index" (in rs, not rb) is greater than 64. is it *ever* possible that perm[i] - which remember is the same as ra[i] - that when "index" is >= 64, that perm[i] (aka ra[i]) will be anything other than zero? with m.If(idx < 64): m.d.comb += perm[i].eq(rb64[idx]) answer: no, it cannot, because when index >= 64, perm[i] is never set, and therefore will *always* be zero. *therefore make an assertion about that*: with m.If(index >= 64): comb += Assert(ra[i] == 0) and that just leaves the last one, which is annoyingly a little more complicated, and best done probably by setting up that array rb64 again, which will allow you to get at rb[index] i "cheated" by doing a ridiculously-CPU-intensive cycling through j=0..64 looking for a match against j == index.
(In reply to Luke Kenneth Casson Leighton from comment #46) > (In reply to Cole Poirier from comment #44) > > > 71 # 1. RA[8:64] should always equal 0 > > 72 # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 > > 73 # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] > > > > For 2 and 3 should RB[i*8:i*8+8] actually be RS[i*8:i*8+8]? > > yes. > > > Or am I failing > > to properly read/interpret the 'formalism'? In other words, I'm very > > confused and looking for a way to better understand what I am doing, and > > what I am supposed to be doing. > > you are expressing the expectations about the inputs and outputs of > the module. > > these you express as assertions that must be true. > > (sby then checks those for you under *all* possible values of input and > output). > > therefore you not only need to get the code right, you actually need to > properly understand what it does... and express that in the assertions. > > example. > > from this line of code, is it *ever* possible that bits 8 and above > will be *anything* other than zero? > > m.d.comb += self.ra[0:8].eq(perm) > > answer: no it is not. > > *therefore make an assertion about that*: > > comb += Assert(self.ra[8:] == 0) > > now let us move on to when any given "index" (in rs, not rb) is > greater than 64. > > is it *ever* possible that perm[i] - which remember is the same > as ra[i] - that when "index" is >= 64, that perm[i] > (aka ra[i]) will be anything other than zero? > > with m.If(idx < 64): > m.d.comb += perm[i].eq(rb64[idx]) > > answer: no, it cannot, because when index >= 64, perm[i] is never > set, and therefore will *always* be zero. > > *therefore make an assertion about that*: > > with m.If(index >= 64): > comb += Assert(ra[i] == 0) > > and that just leaves the last one, which is annoyingly a little more > complicated, and best done probably by setting up that array rb64 again, > which will allow you to get at rb[index] > > i "cheated" by doing a ridiculously-CPU-intensive cycling through > j=0..64 looking for a match against j == index. Thank Luke, this is tremendously helpful. I think Michael explained it well, but I was having a hard time fully comprehending because I'm still learning how to read and write the 'language' of the cpu/rtl/circuit domain. Going to re-read this a few times, then review nmigen tutorial by Robert Baruch, Claire Wolf's 'Yosys Application Note 011: Interactive Design Investigation', so I can better understand those 'languages'. Tomorrow should I move on to trying to understand Wolf's verilog code for the rvb equivalent of this operation? With regard to copyright, what should I do? Am I supposed to write to her to ask for permission to use her code? Is that even a possibility? I don't know how to proceed, what do you advise?
Cole, since your module passes your formal proof, I think it might be a good idea to try hooking it up to the logical pipeline, and adding a test for it. To hook it up, you're going to want to open up logical/main_stage.py and take a look at what's there for OP_CNTZ. You're going to want to do something similar to that for OP_BPERM using your Bpermd module. To add a test for bperm, you'll want to open up logical/test/test_pipe_caller.py and duplicate the function `test_cmpb`. You'd then want to modify this copy to have a different name, execute the bpermd instruction instead of cmpb, and possibly have different data for registers 1 and 2. Again, happy to help if you get stuck
(In reply to Michael Nolan from comment #48) > Cole, since your module passes your formal proof, I think it might be a good > idea to try hooking it up to the logical pipeline, and adding a test for it. > > To hook it up, you're going to want to open up logical/main_stage.py and > take a look at what's there for OP_CNTZ. You're going to want to do > something similar to that for OP_BPERM using your Bpermd module. > > To add a test for bperm, you'll want to open up > logical/test/test_pipe_caller.py and duplicate the function `test_cmpb`. > You'd then want to modify this copy to have a different name, execute the > bpermd instruction instead of cmpb, and possibly have different data for > registers 1 and 2. Again, happy to help if you get stuck Sure that sounds like a good plan. I was planning on taking the proof luke provided yesterday, and trying to speed it up by using an Array() as he suggested instead of nested [i][j] for loops. Should I try connecting the module or making the proof modification first? And thank you again for your extreme generosity in offering to help, and in all the help you've given me so far :)
(In reply to Cole Poirier from comment #49) > I was planning on taking the proof luke > provided yesterday, and trying to speed it up by using an Array() as he > suggested instead of nested [i][j] for loops. Should I try connecting the > module or making the proof modification first? And thank you again for your > extreme generosity in offering to help, and in all the help you've given me > so far :) I'm not sure I would. To me, a proof should be as simple as possible to understand, because you need to be able to check the proof against the specification. The existing proof is clear enough to allow it to be checked against the pseudocode, and doesn't take an inordinate amount of time, so I think it's fine to leave it as is. So yeah, I'd say try hooking it up to main_stage and adding a test for it would be better than trying to "optimize" the proof. Especially since there's a bug in the module that the proof hasn't revealed (hint: it has to do with power's numbering of bits).
(In reply to Michael Nolan from comment #50) > I'm not sure I would. To me, a proof should be as simple as possible to > understand, because you need to be able to check the proof against the > specification. The existing proof is clear enough to allow it to be checked > against the pseudocode, and doesn't take an inordinate amount of time, so I > think it's fine to leave it as is. Makes sense to me! > So yeah, I'd say try hooking it up to main_stage and adding a test for it > would be better than trying to "optimize" the proof. Especially since > there's a bug in the module that the proof hasn't revealed (hint: it has to > do with power's numbering of bits). Is this the big-endian comment you left in the pseudo-code? Is that documented in the spec? Looking at POWERISA v3.1 doesn't look like it notes this, unless there is some esoteric notation that denotes this? Or POWERISA is just always big-endian?
Michael, or Luke, In order to add Bpermd to LogicalMainStage, it appears that I first have to add it to soc.decoder.power_enums.InternalOp, because that is the type of the cases for the switch statement. The switch-case statment 'matches' on 'op.isn_type' which is an InternalOp. Is it possible to user Bpermd inside of a with m.Case statement, given that all the other m.Case statements wrap InternalOp.isn's and the bpermd TODO comment template expects InternalOp.OP_BPERM? If I need to add OP_BPERM to soc.decoder.power_enums.InternalOp, are there any special instructions or restrictions for doing so? As this will be my first time touching code that is used by other people I want to make sure I don't interfere with or break anything.
(In reply to Cole Poirier from comment #52) > Michael, or Luke, > > In order to add Bpermd to LogicalMainStage, it appears that I first have to > add it to soc.decoder.power_enums.InternalOp, line 102, it is already there. remember use grep or in-editor search i also use ctags (aptget install exuberant-ctags) https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/decoder/power_enums.py;h=690bf129381cb9ede1d0d92e3564440597fd9e3e;hb=HEAD so with it already being there, the Case statement can be uncommented and code added. try just doing something small and innocuous to confirm that. regarding code commits, if you make sure there are no syntax errors and second that no other tests fail you're in the clear. it is perfectly fine to commit a test that fails although decorating it as such is generally better. @unittest.skip("broken") or something if memory serves correctly.
(In reply to Luke Kenneth Casson Leighton from comment #53) > (In reply to Cole Poirier from comment #52) > > Michael, or Luke, > > > > In order to add Bpermd to LogicalMainStage, it appears that I first have to > > add it to soc.decoder.power_enums.InternalOp, > > line 102, it is already there. > remember use grep or in-editor search > > i also use ctags (aptget install exuberant-ctags) > > https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/decoder/power_enums.py; > h=690bf129381cb9ede1d0d92e3564440597fd9e3e;hb=HEAD > > so with it already being there, the Case statement can be uncommented and > code added. try just doing something small and innocuous to confirm that. > > > regarding code commits, if you make sure there are no syntax errors and > second that no other tests fail you're in the clear. > > it is perfectly fine to commit a test that fails although decorating it as > such is generally better. > > @unittest.skip("broken") or something if memory serves correctly. Ah yes, appreciated, I will grep first in the future. For clarification, the way to run the tests is by cd'ing to the soc/decoder directory then running 'python3 test/{test_file.py}' for each of the files in the tests directory? Or do I cd to the top level soc directory, and run 'sudo python3 setup.py test'?
(In reply to Cole Poirier from comment #54) > Ah yes, appreciated, I will grep first in the future. For clarification, the > way to run the tests is by cd'ing to the soc/decoder directory then running > 'python3 test/{test_file.py}' for each of the files in the tests directory? > Or do I cd to the top level soc directory, and run 'sudo python3 setup.py > test'? Definitely don't use `sudo`. I cd to the top level and run either `python3 setup.py test` or `nosetests`.
(In reply to Jacob Lifshay from comment #55) > (In reply to Cole Poirier from comment #54) > > Ah yes, appreciated, I will grep first in the future. For clarification, the > > way to run the tests is by cd'ing to the soc/decoder directory then running > > 'python3 test/{test_file.py}' for each of the files in the tests directory? > > Or do I cd to the top level soc directory, and run 'sudo python3 setup.py > > test'? > > Definitely don't use `sudo`. I cd to the top level and run either `python3 > setup.py test` or `nosetests`. I tried doing that but it seems like because the egg_info or wheel is installed (per the HDL_Workflow instructions) within sudo bash I can't run it as a normal user: ``` cole@computer:~/src/soc$ python3 setup.py test running test running egg_info error: [Errno 13] Permission denied ``` If there is something I have to do our could due to fix this please let me know. In the process of running 'sudo (i know it's bad) python3 setup.py test' I noticed some tests are failing due to import errors after the recent 'fu' directory structure change, so I'm going through and fixing the import paths.
Upon further investigation the import errors appear to be non-trivial to fix so I am leaving them alone and moving on to adding Bpermd to fu/logical
(In reply to Jacob Lifshay from comment #55) > (In reply to Cole Poirier from comment #54) > > Ah yes, appreciated, I will grep first in the future. For clarification, the > > way to run the tests is by cd'ing to the soc/decoder directory then running > > 'python3 test/{test_file.py}' for each of the files in the tests directory? because i run ctags in one directory (usually the top level or close to it) and stay there. i generally run e.g. python3 fu/alu/test/test_pipe_caller.py or something. constantly doing "cd" i find very annoying. to find previously-run commands is a matter of running "history" followed by !inserthistorynumber this saves typing the command out repeatedly - also very annoying. lots of annoyingness... :) > > Or do I cd to the top level soc directory, and run 'sudo python3 setup.py > > test'? > > Definitely don't use `sudo`. yep. it will result in test output that, on return as the ordinary user, you will not be able to overwrite. to "fix" that, do this: soc/src$ sudo bash soc/src# chown -R colepoirier . soc/src# exit soc/src$ that will ensure that all files are owned by you (not root) in the entire soc locally checked out repository. a "dumb" way to achieve the same effect is to completely destroy the entire checkout. this is wasteful of both time and bandwidth. > I cd to the top level and run either `python3 setup.py test` or `nosetests`. this runs every single test, which consumes a lot of time however is a good idea. to get a "faster development cycle" i tend to run only the test that is needed. delays in that cycle - by running tests that have nothing to do with the task at hand - i also find annoying. however *after* that fast-iterative cycle (explicitly running only the relevant test), it is kinda important to run more (nosetests3, python3 setup.py test) just to make absolutely sure you didn't break anything unrelated. don't tell no-one i tend not to do that very often... :)
(In reply to Cole Poirier from comment #57) > Upon further investigation the import errors appear to be non-trivial to fix > so I am leaving them alone que? que? give me a hint, i can take a look. > and moving on to adding Bpermd to fu/logical ok.
(In reply to Luke Kenneth Casson Leighton from comment #58) > (In reply to Jacob Lifshay from comment #55) > > (In reply to Cole Poirier from comment #54) > > > Ah yes, appreciated, I will grep first in the future. For clarification, the > > > way to run the tests is by cd'ing to the soc/decoder directory then running > > > 'python3 test/{test_file.py}' for each of the files in the tests directory? > > because i run ctags in one directory (usually the top level or close to it) > and stay there. > > i generally run e.g. python3 fu/alu/test/test_pipe_caller.py or something. > constantly doing "cd" i find very annoying. > > to find previously-run commands is a matter of running "history" followed by > !inserthistorynumber > > this saves typing the command out repeatedly - also very annoying. > > lots of annoyingness... :) Ah that sounds radically better than my 'dumb' bog-standard online/corporate unix training method of cd .. cd cd cd cd ..... ahhhh!!! I'll have to do a quick read of what ctags is and how to use it as you've specified tomorrow. And go back and reference your email to me from march that outlined how I could set up my computer as you have yours set up. > > > Or do I cd to the top level soc directory, and run 'sudo python3 setup.py > > > test'? > > > > Definitely don't use `sudo`. > > yep. it will result in test output that, on return as the ordinary user, > you will not be able to overwrite. to "fix" that, do this: > > soc/src$ sudo bash > soc/src# chown -R colepoirier . > soc/src# exit > soc/src$ > > that will ensure that all files are owned by you (not root) in the entire soc > locally checked out repository. > > a "dumb" way to achieve the same effect is to completely destroy the entire > checkout. this is wasteful of both time and bandwidth. Perfect. Worked. > > I cd to the top level and run either `python3 setup.py test` or `nosetests`. > > this runs every single test, which consumes a lot of time however is a good > idea. > > to get a "faster development cycle" i tend to run only the test that is > needed. > delays in that cycle - by running tests that have nothing to do with the > task at > hand - i also find annoying. > > however *after* that fast-iterative cycle (explicitly running only the > relevant > test), it is kinda important to run more (nosetests3, python3 setup.py test) > just > to make absolutely sure you didn't break anything unrelated. don't tell > no-one > i tend not to do that very often... :) Hmm will try to do as you preach not as you practice then :)
(In reply to Luke Kenneth Casson Leighton from comment #59) > (In reply to Cole Poirier from comment #57) > > Upon further investigation the import errors appear to be non-trivial to fix > > so I am leaving them alone > > que? que? give me a hint, i can take a look. found them. sorted several.
(In reply to Luke Kenneth Casson Leighton from comment #58) > (In reply to Jacob Lifshay from comment #55) > > (In reply to Cole Poirier from comment #54) > > > Ah yes, appreciated, I will grep first in the future. For clarification, the > > > way to run the tests is by cd'ing to the soc/decoder directory then running > > > 'python3 test/{test_file.py}' for each of the files in the tests directory? > > because i run ctags in one directory (usually the top level or close to it) > and stay there. > > i generally run e.g. python3 fu/alu/test/test_pipe_caller.py or something. > constantly doing "cd" i find very annoying. > > to find previously-run commands is a matter of running "history" followed by > !inserthistorynumber > > this saves typing the command out repeatedly - also very annoying. > > lots of annoyingness... :) At the bash prompt, type Ctrl-R then some portion of the previous command, it's the readline shortcut for search through history from most to least recent. You can also keep pressing Ctrl-R to go to the previous occurrence. > > however *after* that fast-iterative cycle (explicitly running only the > relevant > test), it is kinda important to run more (nosetests3, python3 setup.py test) > just > to make absolutely sure you didn't break anything unrelated. don't tell > no-one > i tend not to do that very often... :) should do it more often, since otherwise stuff never gets fixed. Part of why I went to lots of effort to get CI setup and working (which still needs someone to finish setting up the CI mailing list and the sendmail script for use with gitlab-ci-archiver).
(In reply to Luke Kenneth Casson Leighton from comment #59) > (In reply to Cole Poirier from comment #57) > > Upon further investigation the import errors appear to be non-trivial to fix > > so I am leaving them alone > > que? que? give me a hint, i can take a look. I must stop for today. I don't have confidence that I can write the necessary code with the level of care necessary at this point at the end of my day, so I will refrain from doing so and continue tomorrow with integrating Bpermd into fu/logical. Below is the failed test info that I got when trying to fix import errors in two of the tests. Tried to fix the following two tests (stack traces provided for debuggability): ``` Failed test1: File "/home/colepoirier/src/soc/src/soc/scoreboard/test_mem2_fu_matrix.py", line 20, in <module> from ..experiment.score6600 import IssueToScoreboard, RegSim, instr_q, wait_for_busy_clear, wait_for_issue, CompUnitALUs, CompUnitBR, CompUnitsBase File "/home/colepoirier/src/soc/src/soc/experiment/score6600.py", line 17, in <module> from soc.experiment.compalu import ComputationUnitNoDelay File "/home/colepoirier/src/soc/src/soc/experiment/compalu.py", line 9, in <module> from soc.experiment.alu_hier import CompALUOpSubset File "/home/colepoirier/src/soc/src/soc/experiment/alu_hier.py", line 20, in <module> from soc.alu.alu_input_record import CompALUOpSubset ModuleNotFoundError: No module named 'soc.alu' Failed test 2: File "/home/colepoirier/src/soc/src/soc/scoreboard/test_mem_fu_matrix.py", line 24, in <module> from ..experiment.score6600 import IssueToScoreboard, RegSim, instr_q, wait_for_busy_clear, wait_for_issue, CompUnitALUs, CompUnitBR File "/home/colepoirier/src/soc/src/soc/experiment/score6600.py", line 17, in <module> from soc.experiment.compalu import ComputationUnitNoDelay File "/home/colepoirier/src/soc/src/soc/experiment/compalu.py", line 9, in <module> from soc.experiment.alu_hier import CompALUOpSubset File "/home/colepoirier/src/soc/src/soc/experiment/alu_hier.py", line 20, in <module> from soc.alu.alu_input_record import CompALUOpSubset ModuleNotFoundError: No module named 'soc.alu' ``` Fixing the path of soc.alu to be soc.fu.alu results in the tests still failing but with a different error: ``` Failed test 1: ERROR: soc.scoreboard.test_mem2_fu_matrix.test_mem_fus ---------------------------------------------------------------------- Traceback (most recent call last): File "/usr/lib/python3/dist-packages/nose/case.py", line 197, in runTest self.test(*self.arg) File "/home/colepoirier/src/soc/src/soc/scoreboard/test_mem2_fu_matrix.py", line 585, in test_mem_fus vcd_name='test_mem_fus.vcd') File "/home/colepoirier/src/nmigen/nmigen/compat/sim/__init__.py", line 22, in run_simulation fragment.domains += ClockDomain("sync") AttributeError: 'MemFunctionUnits' object has no attribute 'domains' Failed test2: ERROR: soc.scoreboard.test_mem_fu_matrix.test_mem_fus ---------------------------------------------------------------------- Traceback (most recent call last): File "/usr/lib/python3/dist-packages/nose/case.py", line 197, in runTest self.test(*self.arg) File "/home/colepoirier/src/soc/src/soc/scoreboard/test_mem_fu_matrix.py", line 679, in test_mem_fus vcd_name='test_mem_fus.vcd') File "/home/colepoirier/src/nmigen/nmigen/compat/sim/__init__.py", line 22, in run_simulation fragment.domains += ClockDomain("sync") AttributeError: 'MemFunctionUnits' object has no attribute 'domains' ```
(In reply to Cole Poirier from comment #60) > Ah that sounds radically better than my 'dumb' bog-standard online/corporate > unix training method of cd .. cd cd cd cd ..... you'll be hilariously amused that when presented with a DOS prompt that's exactly what i end up doing... > ahhhh!!! I'll have to do a > quick read of what ctags is and how to use it as you've specified tomorrow. > And go back and reference your email to me from march that outlined how I > could set up my computer as you have yours set up. be prepared to have your brain melted > > yep. it will result in test output that, on return as the ordinary user, > > you will not be able to overwrite. to "fix" that, do this: > > > > soc/src$ sudo bash > > soc/src# chown -R colepoirier . > Perfect. Worked. goood. > > to make absolutely sure you didn't break anything unrelated. don't tell > > no-one > > i tend not to do that very often... :) > > Hmm will try to do as you preach not as you practice then :) and what happened? i made some commits, changing stuff - e.g. renamed Logical ALUInputData to LogicalInputData and the unit tests broke. yaaay
(In reply to Cole Poirier from comment #63) > (In reply to Luke Kenneth Casson Leighton from comment #59) > > (In reply to Cole Poirier from comment #57) > > > Upon further investigation the import errors appear to be non-trivial to fix > > > so I am leaving them alone > > > > que? que? give me a hint, i can take a look. > > I must stop for today. I don't have confidence that I can write the > necessary code with the level of care necessary at this point at the end of > my day, yep. focus. not your problem. my responsibility. i broke em, therefore i fix em. > so I will refrain from doing so and continue tomorrow with > integrating Bpermd into fu/logical. yep. this one is your responsibility. > File "/home/colepoirier/src/soc/src/soc/experiment/alu_hier.py", line 20, > in <module> > from soc.alu.alu_input_record import CompALUOpSubset > ModuleNotFoundError: No module named 'soc.alu' sorted that one 5 mins ago > File "/home/colepoirier/src/soc/src/soc/experiment/alu_hier.py", line 20, > in <module> > from soc.alu.alu_input_record import CompALUOpSubset > ModuleNotFoundError: No module named 'soc.alu' > ``` and that one. do a git pull > Failed test2: > ERROR: soc.scoreboard.test_mem_fu_matrix.test_mem_fus interesting. ignore it. not your problem. do raise a separate bugreport about it though.
(In reply to Jacob Lifshay from comment #62) > At the bash prompt, type Ctrl-R then some portion of the previous command, > it's the readline shortcut for search through history from most to least > recent. You can also keep pressing Ctrl-R to go to the previous occurrence. Appreciate the tip Jacob. > > however *after* that fast-iterative cycle (explicitly running only the > > relevant > > test), it is kinda important to run more (nosetests3, python3 setup.py test) > > just > > to make absolutely sure you didn't break anything unrelated. don't tell > > no-one > > i tend not to do that very often... :) > > should do it more often, since otherwise stuff never gets fixed. Part of why > I went to lots of effort to get CI setup and working (which still needs > someone to finish setting up the CI mailing list and the sendmail script for > use with gitlab-ci-archiver). Was that task assigned to Jock? I remember I helped with the initial setup but I thought I remembered Jock taking over once the CI mailing list task was introduced. Jacob, is there any testing stuff that I was supposed to do that you've noticed I forgot or failed to do? I don't think there is, but honestly I forget, as I moved on to focusing on the coriolis chroot setup script immediately after that.
(In reply to Luke Kenneth Casson Leighton from comment #65) > > Failed test2: > > ERROR: soc.scoreboard.test_mem_fu_matrix.test_mem_fus > > interesting. ignore it. not your problem. do raise a separate bugreport > about it though. Did a git pull, and now the test fails with the second error state instead of the first. I'm not sure how I would file a bug report for this failed test, and since this is your domain, and I have no more energy today I'll leave it to you, ok?
(In reply to Cole Poirier from comment #67) > Did a git pull, and now the test fails with the second error state instead > of the first. joy. > I'm not sure how I would file a bug report for this failed > test, and since this is your domain, and I have no more energy today I'll > leave it to you, ok? ok :) 2:30am here so definitely time to stop. l.
I have made the small code additions necessary to connect the Bperm module to the fu/logical pipeline, and added the test for this to test_pipe_caller.py. Important question, has soc.decoder.isa.all.ISA() been moved to soc.decoder.pseudo.pagereader.ISA()?
(In reply to Cole Poirier from comment #69) > I have made the small code additions necessary to connect the Bperm module > to the fu/logical pipeline, and added the test for this to > test_pipe_caller.py. great. if it passes, commit it, git pull, then push it. let's take a look. > Important question, important _non-sequitur_ question. > has soc.decoder.isa.all.ISA() been > moved to soc.decoder.pseudo.pagereader.ISA()? pagereader.ISA is for reading the ISA markdown files. that is its job. it creates a data structure that conveniently allows access in python to the contents of those markdown files. decoder.isa.all.ISA() is an auto-generated representation *of* the pseudo-code - converted to python - for use by the simulator. there is absolutely no relation whatsoever between the two tasks that these two completely different modules perform, other than that, by coincidence, pagereader.ISA happens to read the pseudocode that is auto-oonverted to python and contained in decoder.isa.all.ISA() hence why i am left puzzled and wondering - out of fascinated curiosity - why there would be any reason why you imagine that one would be moved to the other. same name, perhaps? was that it?
(In reply to Luke Kenneth Casson Leighton from comment #70) > (In reply to Cole Poirier from comment #69) > > I have made the small code additions necessary to connect the Bperm module > > to the fu/logical pipeline, and added the test for this to > > test_pipe_caller.py. > > great. if it passes, commit it, git pull, then push it. let's take a look. I can't run the test, see below. > > Important question, > > important _non-sequitur_ question. > > > has soc.decoder.isa.all.ISA() been > > moved to soc.decoder.pseudo.pagereader.ISA()? > > pagereader.ISA is for reading the ISA markdown files. that is its job. > it creates a data structure that conveniently allows access in python > to the contents of those markdown files. > > decoder.isa.all.ISA() is an auto-generated representation *of* the > pseudo-code - converted to python - for use by the simulator. > > there is absolutely no relation whatsoever between the two tasks that > these two completely different modules perform, other than that, by > coincidence, pagereader.ISA happens to read the pseudocode that is > auto-oonverted to python and contained in decoder.isa.all.ISA() > > hence why i am left puzzled and wondering - out of fascinated curiosity - > why there would be any reason why you imagine that one would be moved > to the other. > > same name, perhaps? was that it? Yes, has caused an hour of headache. decoder/all.py is needed in order to run the tests. all.py is auto-generated, so is not present in the directory. How am I supposed to auto-generate it? Is it supposed to be autogenerated by the test itself? This would be odd as the fu/logical/tests/test_pipe_caller.py file imports this at the top of the file. Essentially, help I am quite stuck after trying to solve this for an hour.
(In reply to Cole Poirier from comment #71) > (In reply to Luke Kenneth Casson Leighton from comment #70) > > (In reply to Cole Poirier from comment #69) > > > I have made the small code additions necessary to connect the Bperm module > > > to the fu/logical pipeline, and added the test for this to > > > test_pipe_caller.py. > > > > great. if it passes, commit it, git pull, then push it. let's take a look. > > I can't run the test, see below. > > > > Important question, > > > > important _non-sequitur_ question. > > > > > has soc.decoder.isa.all.ISA() been > > > moved to soc.decoder.pseudo.pagereader.ISA()? > > > > pagereader.ISA is for reading the ISA markdown files. that is its job. > > it creates a data structure that conveniently allows access in python > > to the contents of those markdown files. > > > > decoder.isa.all.ISA() is an auto-generated representation *of* the > > pseudo-code - converted to python - for use by the simulator. > > > > there is absolutely no relation whatsoever between the two tasks that > > these two completely different modules perform, other than that, by > > coincidence, pagereader.ISA happens to read the pseudocode that is > > auto-oonverted to python and contained in decoder.isa.all.ISA() > > > > hence why i am left puzzled and wondering - out of fascinated curiosity - > > why there would be any reason why you imagine that one would be moved > > to the other. > > > > same name, perhaps? was that it? > > Yes, has caused an hour of headache. decoder/all.py is needed in order to > run the tests. all.py is auto-generated, so is not present in the directory. > How am I supposed to auto-generate it? ah - you should have asked earlier :) look in the Makefile: python3 src/soc/decoder/pseudo/pywriter.py > Is it supposed to be autogenerated by > the test itself? no because it takes a good couple of minutes to go over the 300+ pseudo-code code-fragments. > This would be odd as the > fu/logical/tests/test_pipe_caller.py file imports this at the top of the > file. Essentially, help I am quite stuck after trying to solve this for an > hour. should have asked earlier :)
(In reply to Luke Kenneth Casson Leighton from comment #72) > > Yes, has caused an hour of headache. decoder/all.py is needed in order to > > run the tests. all.py is auto-generated, so is not present in the directory. > > How am I supposed to auto-generate it? > > ah - you should have asked earlier :) look in the Makefile: > python3 src/soc/decoder/pseudo/pywriter.py Aha! I completely forgot about the Makefile. > > Is it supposed to be autogenerated by > > the test itself? > > no because it takes a good couple of minutes to go over the 300+ pseudo-code > code-fragments. > > > This would be odd as the > > fu/logical/tests/test_pipe_caller.py file imports this at the top of the > > file. Essentially, help I am quite stuck after trying to solve this for an > > hour. > > should have asked earlier :) Indeed, I'm trying to balance doing things without help at every step, with trying to communicate in the manner necessary for collaborative work. Getting one step closer to the right balance with each mistake! At least this bug report will be helpful to new members, as it's an utter novice (me) discovering all (well, most) of the possible difficulties/misunderstandings :)
Test passes, and code has been commit-pushed. Moving on to your suggestion on today's kanban update of integrating the formal proof of bpermd: ``` Luke in reply to Cole: >Today I plan on integrating the Bpermd module into the >logical pipeline, with tests. fooocuuuus :) adding the module to Logical main_stage.py should be around... maximum 10 lines of code. really. not. difficult. link the inputs. link the outputs. err... that's it. btw as a third (incremental) step, after integrating it and putting in the unit test into soc.fu.logical.test/test_pipe_caller.py, you should actually be able to integrate the formal proof into the Logical pipeline as well. ``` How should I go about integrating the formal proof of bpermd into the logical pipeline? I've thought about it, and I am unsure as to how to proceed. Is there a model I can follow as before? I also want to follow up on a comment of Michael's from yesterday: ``` From comment #50 of this bug Michael Nolan 2020-05-19 20:24:19 BST I'd say try hooking it up to main_stage and adding a test for it would be better than trying to "optimize" the proof. Especially since there's a bug in the module that the proof hasn't revealed (hint: it has to do with power's numbering of bits). ``` Is my proof of bpermd in fact not a proper proof, and incorrect because it's making an mistake with endian-ness?
(In reply to Cole Poirier from comment #74) > Test passes, and code has been commit-pushed. Moving on to your suggestion > on today's kanban update of integrating the formal proof of bpermd: > Cool. I've modified test_bpermd a bit so it exercises the module a bit better. Previously, you only had it do one iteration with two constants, and those constants made bpermd evaluate to 0. This isn't *really* sufficient to establish much confidence in the module, so I modified it to do ~20 iterations of something that would evaluate to something other than 0. > How should I go about integrating the formal proof of bpermd into the > logical pipeline? I've thought about it, and I am unsure as to how to > proceed. Is there a model I can follow as before? > > I also want to follow up on a comment of Michael's from yesterday: > > ``` > From comment #50 of this bug > > Michael Nolan 2020-05-19 20:24:19 BST > I'd say try hooking it up to main_stage and adding a test for it would be > better than trying to "optimize" the proof. Especially since there's a bug > in the module that the proof hasn't revealed (hint: it has to do with > power's numbering of bits). > ``` > > Is my proof of bpermd in fact not a proper proof, and incorrect because it's > making an mistake with endian-ness? Well kinda. Your proof is written to match the Power ISA spec, and from a glance it looks like it does that. However, Power bit indices go from left to right, which is opposite what python and nmigen do. So although your proof looks like it matches the spec, it doesn't give correct results when it's actually tested. That's why I suggested you hook it up to the testbench , because the testbench compares it to some python pseudocode that *does* index bits correctly. So what I think you should do now is pull and run the testbench again, and see if you can't figure out how to get it to pass those tests. Then modify the proof correspondingly.
(In reply to Michael Nolan from comment #75) > (In reply to Cole Poirier from comment #74) > > Test passes, and code has been commit-pushed. Moving on to your suggestion > > on today's kanban update of integrating the formal proof of bpermd: > > > Cool. I've modified test_bpermd a bit so it exercises the module a bit > better. Previously, you only had it do one iteration with two constants, and > those constants made bpermd evaluate to 0. This isn't *really* sufficient to > establish much confidence in the module, so I modified it to do ~20 > iterations of something that would evaluate to something other than 0. > > > > > > How should I go about integrating the formal proof of bpermd into the > > logical pipeline? I've thought about it, and I am unsure as to how to > > proceed. Is there a model I can follow as before? > > > > I also want to follow up on a comment of Michael's from yesterday: > > > > ``` > > From comment #50 of this bug > > > > Michael Nolan 2020-05-19 20:24:19 BST > > I'd say try hooking it up to main_stage and adding a test for it would be > > better than trying to "optimize" the proof. Especially since there's a bug > > in the module that the proof hasn't revealed (hint: it has to do with > > power's numbering of bits). > > ``` > > > > Is my proof of bpermd in fact not a proper proof, and incorrect because it's > > making an mistake with endian-ness? > > Well kinda. Your proof is written to match the Power ISA spec, and from a > glance it looks like it does that. However, Power bit indices go from left > to right, which is opposite what python and nmigen do. So although your > proof looks like it matches the spec, it doesn't give correct results when > it's actually tested. That's why I suggested you hook it up to the testbench > , because the testbench compares it to some python pseudocode that *does* > index bits correctly. > > So what I think you should do now is pull and run the testbench again, and > see if you can't figure out how to get it to pass those tests. Then modify > the proof correspondingly. Thanks Michael, your help is yet again very helpful :) Unfortunately I won't be able to do this until tomorrow morning because an exterminator appointment is forcing me to be away from my computer. Looking forward to tackling this.
so, cole, here's an example: RS=0x4000000, RB=0xdeadcownonsense the hardware produces the answer 0xf7, the *actual* expected answer is supposed to be 0xff. so you can now write a unit test which puts those exact values in (oh look, fu/logical/test/test_bpermd.py is empty....) and play with the code until you *do* get the answer "0xff". bpermd 3, 1, 2 ['RS', 'RB'] reading reg 1 reading reg 2 [SelectableInt(value=0x4000000, bits=64), SelectableInt(value=0xdeadbeefcafec0de, bits=64)] concat 8 SelectableInt(value=0x0, bits=8) concat 56 SelectableInt(value=0x0, bits=56) concat 1 SelectableInt(value=0xff, bits=64) (SelectableInt(value=0xff, bits=64),) writing reg 3 SelectableInt(value=0xff, bits=64) expected ff, actual: f7 File "fu/logical/test/test_pipe_caller.py", line 260, in process self.assertEqual(expected, alu_out, code) AssertionError: 255 != 247 : bpermd 3, 1, 2
https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/cr/formal/proof_main_stage.py;h=d109f81f599c335986ef8a847246796cfa40e996 hey cole, psst, see line 61...
Unfortunately I think I have reached a blocker. When attempting to run the tests, I get to testing the test_rand_imm_logical(): ``` ['ori 3, 1, 18936'] ['xori 3, 1, 18465'] ``` Then I get this error which I don't think I am able to fix. ``` ['xori 3, 1, 18465'] . ---------------------------------------------------------------------- Ran 9 tests in 3.111s OK ControlBase <soc.fu.logical.pipeline.LogicalBasePipe object at 0x7fbf8d70ea20> None None False DynamicPipe init <super: <class 'DynamicPipe'>, <LogicalStages object>> (<soc.fu.logical.pipe_data.LogicalPipeSpec object at 0x7fbf8d70e908>,) redir <abc.LogicalStages object at 0x7fbf8d70e6a0> (<soc.fu.logical.pipe_data.LogicalPipeSpec object at 0x7fbf8d70e908>,) ControlBase <abc.LogicalStages object at 0x7fbf8d70e6a0> <abc.LogicalStages object at 0x7fbf8d70e6a0> None False E ====================================================================== ERROR: run_all (__main__.TestRunner) ---------------------------------------------------------------------- Traceback (most recent call last): File "test_pipe_caller.py", line 201, in run_all sim = Simulator(m) File "/home/colepoirier/src/nmigen/nmigen/back/pysim.py", line 933, in __init__ self._fragment = Fragment.get(fragment, platform=None).prepare() File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 39, in get obj = obj.elaborate(platform) File "/home/colepoirier/src/nmigen/nmigen/hdl/dsl.py", line 537, in elaborate fragment.add_subfragment(Fragment.get(self._named_submodules[name], platform), name) File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 39, in get obj = obj.elaborate(platform) File "/home/colepoirier/src/nmigen/nmigen/hdl/dsl.py", line 537, in elaborate fragment.add_subfragment(Fragment.get(self._named_submodules[name], platform), name) File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 39, in get obj = obj.elaborate(platform) File "/home/colepoirier/src/soc/src/soc/decoder/power_decoder.py", line 328, in elaborate m = PowerDecoder.elaborate(self, platform) File "/home/colepoirier/src/soc/src/soc/decoder/power_decoder.py", line 275, in elaborate comb += self.op._eq(row) File "/home/colepoirier/src/soc/src/soc/decoder/power_decoder.py", line 152, in _eq self.cr_out.eq(CROutSel[row['CR out']]), File "/usr/lib/python3.7/enum.py", line 352, in __getitem__ return cls._member_map_[name] KeyError: '0' ```
(In reply to Cole Poirier from comment #79) > Unfortunately I think I have reached a blocker. When attempting to run the > tests, I get to testing the test_rand_imm_logical(): make sure to re-run pywriter.py michael just updated the csv files and that means that the format of the auto-generated ISA files changes.
(In reply to Luke Kenneth Casson Leighton from comment #80) > (In reply to Cole Poirier from comment #79) > > Unfortunately I think I have reached a blocker. When attempting to run the > > tests, I get to testing the test_rand_imm_logical(): > > make sure to re-run pywriter.py > > michael just updated the csv files and that means that the format of the > auto-generated ISA files changes. Aha! Thank you. I did git submodule update --init --recursive and git pull but forgot this other part... I'm going to write a small script that does all three in sequence.
just checked it here - doesn't work. need michael to investigate. running pywriter.py every time will significantly slow your workflow down. suggest doing it when needed.
(In reply to Luke Kenneth Casson Leighton from comment #82) > just checked it here - doesn't work. need michael to investigate. > > running pywriter.py every time will significantly slow your workflow down. > suggest doing it when needed. Thanks. I'm planning on just running the script at the start of my day, hopefully will leave a little reminder in my brain to run pywriter.py if I get decoder/op-code errors.
ok cole try again, michael just updated the CSV files
(In reply to Luke Kenneth Casson Leighton from comment #84) > ok cole try again, michael just updated the CSV files Awesome, my test now fails as expected. Going to get to work on making the test pass.
Is there a way to access the values of the Signals instead of just their type and name? It would be really useful if I could print the values of signals while trying to get the test to pass.
(In reply to Cole Poirier from comment #86) > Is there a way to access the values of the Signals instead of just their > type and name? It would be really useful if I could print the values of > signals while trying to get the test to pass. x = yield val then print (x)
(In reply to Luke Kenneth Casson Leighton from comment #87) > (In reply to Cole Poirier from comment #86) > > Is there a way to access the values of the Signals instead of just their > > type and name? It would be really useful if I could print the values of > > signals while trying to get the test to pass. > > x = yield val > > then print (x) I have tried doing the following: ``` def elaborate(self, platform): m = Module() width = yield self.width rs = yield self.rs ra = yield self.ra rb = yield self.rb print("width: ", width, "rs: ", rs, "rb: ", rb, "ra: ", ra) ``` Which unfortunately does not print the values, but gives me the following error: ``` File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 50, in get raise AttributeError("Object {!r} cannot be elaborated".format(obj)) AttributeError: Object <generator object Bpermd.elaborate at 0x7f1f4ca00750> cannot be elaborated ``` What am I doing wrong?
(In reply to Cole Poirier from comment #88) > (In reply to Luke Kenneth Casson Leighton from comment #87) > > (In reply to Cole Poirier from comment #86) > > > Is there a way to access the values of the Signals instead of just their > > > type and name? It would be really useful if I could print the values of > > > signals while trying to get the test to pass. > > > > x = yield val > > > > then print (x) > > I have tried doing the following: > ``` > def elaborate(self, platform): > m = Module() > width = yield self.width > rs = yield self.rs > ra = yield self.ra > rb = yield self.rb > print("width: ", width, "rs: ", rs, "rb: ", rb, "ra: ", ra) > ``` > > Which unfortunately does not print the values, but gives me the following > error: > ``` > File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 50, in get > raise AttributeError("Object {!r} cannot be elaborated".format(obj)) > AttributeError: Object <generator object Bpermd.elaborate at 0x7f1f4ca00750> > cannot be elaborated > ``` > > What am I doing wrong? Sorry, the x = yield sig only works inside the simulator. There's not a way to print the value of a signal from inside the module itself This should make sense, the module is *building* a circuit, it has no idea what the values of any of the parts of the circuit are while it's being built.
(In reply to Michael Nolan from comment #89) > (In reply to Cole Poirier from comment #88) > > (In reply to Luke Kenneth Casson Leighton from comment #87) > > > (In reply to Cole Poirier from comment #86) > > > > Is there a way to access the values of the Signals instead of just their > > > > type and name? It would be really useful if I could print the values of > > > > signals while trying to get the test to pass. > > > > > > x = yield val > > > > > > then print (x) > > > > I have tried doing the following: > > ``` > > def elaborate(self, platform): > > m = Module() > > width = yield self.width > > rs = yield self.rs > > ra = yield self.ra > > rb = yield self.rb > > print("width: ", width, "rs: ", rs, "rb: ", rb, "ra: ", ra) > > ``` > > > > Which unfortunately does not print the values, but gives me the following > > error: > > ``` > > File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 50, in get > > raise AttributeError("Object {!r} cannot be elaborated".format(obj)) > > AttributeError: Object <generator object Bpermd.elaborate at 0x7f1f4ca00750> > > cannot be elaborated > > ``` > > > > What am I doing wrong? > > Sorry, the x = yield sig only works inside the simulator. There's not a way > to print the value of a signal from inside the module itself > > This should make sense, the module is *building* a circuit, it has no idea > what the values of any of the parts of the circuit are while it's being > built. I see. Thank you, that does indeed make sense. I've been working on this for a few hours and am struggling. I'm going to try writing this in regular python code so I can debug print the values, and properly understand how endian-ness affects the code.
(In reply to Cole Poirier from comment #90) > (In reply to Michael Nolan from comment #89) > > (In reply to Cole Poirier from comment #88) > > > (In reply to Luke Kenneth Casson Leighton from comment #87) > > > > (In reply to Cole Poirier from comment #86) > > > > > Is there a way to access the values of the Signals instead of just their > > > > > type and name? It would be really useful if I could print the values of > > > > > signals while trying to get the test to pass. > > > > > > > > x = yield val > > > > > > > > then print (x) > > > > > > I have tried doing the following: > > > ``` > > > def elaborate(self, platform): > > > m = Module() > > > width = yield self.width > > > rs = yield self.rs > > > ra = yield self.ra > > > rb = yield self.rb > > > print("width: ", width, "rs: ", rs, "rb: ", rb, "ra: ", ra) > > > ``` > > > > > > Which unfortunately does not print the values, but gives me the following > > > error: > > > ``` > > > File "/home/colepoirier/src/nmigen/nmigen/hdl/ir.py", line 50, in get > > > raise AttributeError("Object {!r} cannot be elaborated".format(obj)) > > > AttributeError: Object <generator object Bpermd.elaborate at 0x7f1f4ca00750> > > > cannot be elaborated > > > ``` > > > > > > What am I doing wrong? > > > > Sorry, the x = yield sig only works inside the simulator. There's not a way > > to print the value of a signal from inside the module itself > > > > This should make sense, the module is *building* a circuit, it has no idea > > what the values of any of the parts of the circuit are while it's being > > built. > > I see. Thank you, that does indeed make sense. I've been working on this for > a few hours and am struggling. I'm going to try writing this in regular > python code so I can debug print the values, and properly understand how > endian-ness affects the code. At this point my head is going in circles over and over with respect to the endianness of python and the inputs to the function, and I keep flipping from one understanding to another, essentially leaving me with no understanding... I'd describe it as unpleasant and unhelpful self recursion. So this seems like a good point to stop today, and try my luck with understanding endianness again tomorrow.
Big endianess: LSB starts at top numbered wire, MSB is in wire 0. little: LSB is in wire 0. to access 64 bit in BE you do this x[63-index] not x[index] to access 32 bit in BE you do this: x[31-index] so somewhere, that is what is needed.
(In reply to Luke Kenneth Casson Leighton from comment #92) > Big endianess: LSB starts at top numbered wire, MSB is in wire 0. > > little: LSB is in wire 0. > > to access 64 bit in BE you do this > x[63-index] > not > x[index] > > to access 32 bit in BE you do this: > x[31-index] > > so somewhere, that is what is needed. I think I've tried every possible combination at this point and I am still unable to make progress. This is the current state of my bpermd.py module, that at least doesn't just output 0 every time. I think I have tried all possible permutations of 63-index and 7-index, but still cannot get it to produce correct results. Can you please give me some guidance? ``` def elaborate(self, platform): m = Module() perm = Signal(self.width, reset_less=True) rb64 = [Signal(1, reset_less=True, name=f"rb64_{i}") for i in range(64)] for i in range(64): m.d.comb += rb64[i].eq(self.rb[63-i]) rb64 = Array(rb64) for i in range(8): index = self.rs[8*(7-i)+8:8*(7-i):-1] idx = Signal(8, name=f"idx_{i}", reset_less=True) m.d.comb += idx.eq(index) with m.If(idx < 64): m.d.comb += perm[7-i].eq(rb64[63-idx]) m.d.comb += self.ra[0:8].eq(perm) return m ```
Michael, the unit tests for fu/logical/test/test_pipe_caller.py has been fixed by luke, and now produces a failed test for my module bpermd. Thanks for your help!
(In reply to Cole Poirier from comment #94) > Michael, the unit tests for fu/logical/test/test_pipe_caller.py has been > fixed by luke, and now produces a failed test for my module bpermd. Thanks > for your help! Bpermd is now working
(In reply to Michael Nolan from comment #95) > (In reply to Cole Poirier from comment #94) > > Michael, the unit tests for fu/logical/test/test_pipe_caller.py has been > > fixed by luke, and now produces a failed test for my module bpermd. Thanks > > for your help! > > Bpermd is now working *smacks-forehead* - the commit you made, to use self.i.b, made no sense, until i spotted in the popcount for-loop that b had been overwritten. that's why it ended up with the value "7". and the horrible thing is, the simulation would only have failed after running popcnt before bpermd. --- a/src/soc/fu/logical/main_stage.py +++ b/src/soc/fu/logical/main_stage.py @@ -45,7 +45,6 @@ class LogicalMainStage(PipeModBase): comb += o.ok.eq(1) # overridden if no op activates - m.submodules.bpermd = bpermd = Bpermd(64) ########################## @@ -76,13 +75,13 @@ class LogicalMainStage(PipeModBase): pc = [a] # QTY32 2-bit (to take 2x 1-bit sums) etc. work = [(32, 2), (16, 3), (8, 4), (4, 5), (2, 6), (1, 7)] - for l, b in work: - pc.append(array_of(l, b)) + for l, bw in work: + pc.append(array_of(l, bw)) pc8 = pc[3] # array of 8 8-bit counts (popcntb) pc32 = pc[5] # array of 2 32-bit counts (popcntw) popcnt = pc[-1] # array of 1 64-bit count (popcntd) # cascade-tree of adds - for idx, (l, b) in enumerate(work): + for idx, (l, bw) in enumerate(work): for i in range(l): stt, end = i*2, i*2+1 src, dst = pc[idx], pc[idx+1] @@ -136,7 +135,7 @@ class LogicalMainStage(PipeModBase): ###### bpermd ####### with m.Case(InternalOp.OP_BPERM): comb += bpermd.rs.eq(a) - comb += bpermd.rb.eq(self.i.b) + comb += bpermd.rb.eq(b) comb += o.data.eq(bpermd.ra) with m.Default():
(In reply to Luke Kenneth Casson Leighton from comment #96) > (In reply to Michael Nolan from comment #95) > > (In reply to Cole Poirier from comment #94) > > > Michael, the unit tests for fu/logical/test/test_pipe_caller.py has been > > > fixed by luke, and now produces a failed test for my module bpermd. Thanks > > > for your help! > > > > Bpermd is now working > > *smacks-forehead* - the commit you made, to use self.i.b, made no sense, > until > i spotted in the popcount for-loop that b had been overwritten. that's why > it ended up with the value "7". > > and the horrible thing is, the simulation would only have failed after > running popcnt before bpermd. Oh is *THAT* why? That confused the heck out of me.
(In reply to Michael Nolan from comment #97) > (In reply to Luke Kenneth Casson Leighton from comment #96) > > *smacks-forehead* - the commit you made, to use self.i.b, made no sense, > > until > > i spotted in the popcount for-loop that b had been overwritten. that's why > > it ended up with the value "7". > Oh is *THAT* why? That confused the heck out of me. ngggggh my penchant for short variable names has downsides.
Awesome, thank you both for your help, I clearly wasn't going to figure this out. What should I do now? Should I try reading and understanding Claire Wolf's optimized bit manip code, then try optimizing the bpermd module? Or is there something more helpful I should do?
(In reply to Cole Poirier from comment #99) > Awesome, thank you both for your help, I clearly wasn't going to figure this > out. What should I do now? Should I try reading and understanding Claire > Wolf's optimized bit manip code, then try optimizing the bpermd module? we have a working module so leave optimisation for later. leave thus bugreport open, come back to that later > Or > is there something more helpful I should do? see mailing list.
Luke should we close this bug and open a new bug "bpermd optimization" when it's appropriate after the oct 2020 tapeout?
(In reply to Cole Poirier from comment #101) > Luke should we close this bug and open a new bug "bpermd optimization" yes good idea. > when > it's appropriate after the oct 2020 tapeout? link it to depend on #383 for now and add "see also" this one.