[libre-riscv-dev] [Bug 316] New: bperm TODO

[libre-riscv-dev] [Bug 316] New: bperm TODO

[bugzilla-daemon]

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

            Bug ID: 316
           Summary: bperm TODO
           Product: Libre-SOC's first SoC
           Version: unspecified
          Hardware: PC
                OS: Linux
            Status: CONFIRMED
          Severity: normal
          Priority: ---
         Component: Source Code
          Assignee: lkcl@lkcl.net
          Reporter: colepoirier@gmail.com
                CC: libre-riscv-dev@lists.libre-riscv.org
   NLnet milestone: ---

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)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #1 from Cole Poirier <colepoirier@gmail.com> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

Cole Poirier <colepoirier@gmail.com> changed:

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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

Yehowshua <yimmanuel3@gatech.edu> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |yimmanuel3@gatech.edu

--- Comment #2 from Yehowshua <yimmanuel3@gatech.edu> ---
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)
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #3 from Cole Poirier <colepoirier@gmail.com> ---
(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)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |lkcl@lkcl.net

--- Comment #4 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #5 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #6 from Cole Poirier <colepoirier@gmail.com> ---
(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])
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #7 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #8 from Cole Poirier <colepoirier@gmail.com> ---
(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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #9 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #10 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #11 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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 are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #12 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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]

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #13 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #14 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
     for i in range(0, 8):

just

     for i in range(8):

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #15 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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...
:)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #16 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #17 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

Michael Nolan <mtnolan2640@gmail.com> changed:

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

--- Comment #18 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #19 from Michael Nolan <mtnolan2640@gmail.com> ---
(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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #20 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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*.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #21 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #22 from Cole Poirier <colepoirier@gmail.com> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #23 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #24 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #25 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
        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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #26 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #27 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #28 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #29 from Cole Poirier <colepoirier@gmail.com> ---
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)
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #30 from Michael Nolan <mtnolan2640@gmail.com> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #31 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
try running a different formal test that is known to already work.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #32 from Cole Poirier <colepoirier@gmail.com> ---
(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)
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #33 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #34 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #35 from Cole Poirier <colepoirier@gmail.com> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #36 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #37 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #38 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
cole i moved the soc.logical.bperm code into soc.fu.logical.bperm
can i leave it with you to update the imports?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #39 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #40 from Cole Poirier <colepoirier@gmail.com> ---
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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #41 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #42 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #43 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #44 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #45 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #46 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #47 from Cole Poirier <colepoirier@gmail.com> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #48 from Michael Nolan <mtnolan2640@gmail.com> ---
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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #49 from Cole Poirier <colepoirier@gmail.com> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #50 from Michael Nolan <mtnolan2640@gmail.com> ---
(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).

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #51 from Cole Poirier <colepoirier@gmail.com> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #52 from Cole Poirier <colepoirier@gmail.com> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #53 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #54 from Cole Poirier <colepoirier@gmail.com> ---
(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'?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

Jacob Lifshay <programmerjake@gmail.com> changed:

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

--- Comment #55 from Jacob Lifshay <programmerjake@gmail.com> ---
(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`.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #56 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #57 from Cole Poirier <colepoirier@gmail.com> ---
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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #58 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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... :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #59 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #60 from Cole Poirier <colepoirier@gmail.com> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #61 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #62 from Jacob Lifshay <programmerjake@gmail.com> ---
(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).

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #63 from Cole Poirier <colepoirier@gmail.com> ---
(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'
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #64 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #65 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #66 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #67 from Cole Poirier <colepoirier@gmail.com> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #68 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #69 from Cole Poirier <colepoirier@gmail.com> ---
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()?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #70 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #71 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #72 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #73 from Cole Poirier <colepoirier@gmail.com> ---
(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 :)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #74 from Cole Poirier <colepoirier@gmail.com> ---
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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #75 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #76 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #77 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #78 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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...

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #79 from Cole Poirier <colepoirier@gmail.com> ---
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'
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #80 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #81 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #82 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #83 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #84 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
ok cole try again, michael just updated the CSV files

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #85 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #86 from Cole Poirier <colepoirier@gmail.com> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #87 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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)

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #88 from Cole Poirier <colepoirier@gmail.com> ---
(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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #89 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #90 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #91 from Cole Poirier <colepoirier@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #92 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #93 from Cole Poirier <colepoirier@gmail.com> ---
(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
```

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #94 from Cole Poirier <colepoirier@gmail.com> ---
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!

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #95 from Michael Nolan <mtnolan2640@gmail.com> ---
(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

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #96 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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():

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #97 from Michael Nolan <mtnolan2640@gmail.com> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #98 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #99 from Cole Poirier <colepoirier@gmail.com> ---
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?

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

[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon]

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

--- Comment #100 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(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.

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