[libre-riscv-dev] daily kan-ban update 14may2020

[libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

yesterday, i looked (again) at the address-acknowledgement of
LDSTCompUnit - i think i have a handle on it.  i also helped Michael
with the ALU pipelines, split out Logical operations.  also reviewed
the MarketNext article (which we are pushed for time to review).

today - more LDSTCompUnit, which is challenging - and probably
(because it's so much easier) keep reviewing and going over the ALU
code.

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Michael Nolan]

Yesterday I worked on connecting the rotator from microwatt up to the 
shift/rotate unit, fixing bugs in the rotator, and testing it. Today I 
might try working on comparisons, but I'm not sure whether they should 
be a part of the alu or a separate FU

--Michael


_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Thu, May 14, 2020 at 3:23 PM Michael Nolan <mtnolan2640@gmail.com> wrote:

> Yesterday I worked on connecting the rotator from microwatt up to the
> shift/rotate unit, fixing bugs in the rotator, and testing it.

i'm amazed it worked, and also how elegant the microwatt rotator code is.

> Today I might try working on comparisons, but I'm not sure whether they should
> be a part of the alu or a separate FU

i went through the list this morning, and left some TODOs.

cmpb is different from cmp: cmp is definitely based on add (actually,
subtract - but see the notes from execute1.vhdl):
https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L540

cmp is definitely arithmetic, however cmpb feels like it is a
logical-thing (and is in fixedlogical)
https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L657
https://github.com/antonblanchard/microwatt/blob/master/ppc_fx_insns.vhdl#L735
https://github.com/antonblanchard/microwatt/blob/master/helpers.vhdl#L117


btw, you'll like this: because we are doing a parallel processor,
different Function Units *can* actually cover multiple tasks :)  let's
not go into that right now, however if we convert power_enum Function
into an unary field (1<<0, 1<<1, 1<<2) then we can, in the CSV files,
set multiple bits.

a good example would be AND and OR and XOR: those are prime candidates
to put into *both* the Logical *and* Arithmetic pipelines.  recorded
it for now:
https://bugs.libre-soc.org/show_bug.cgi?id=310

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Tobias Platen]

Like Yesterday I am still working on the countzero.vhdl thing.

Tobias

On Thu, 14 May 2020 15:43:33 +0100
Luke Kenneth Casson Leighton <lkcl@lkcl.net> wrote:

> On Thu, May 14, 2020 at 3:23 PM Michael Nolan <mtnolan2640@gmail.com> wrote:
> 
> > Yesterday I worked on connecting the rotator from microwatt up to the
> > shift/rotate unit, fixing bugs in the rotator, and testing it.
> 
> i'm amazed it worked, and also how elegant the microwatt rotator code is.
> 
> > Today I might try working on comparisons, but I'm not sure whether they should
> > be a part of the alu or a separate FU
> 
> i went through the list this morning, and left some TODOs.
> 
> cmpb is different from cmp: cmp is definitely based on add (actually,
> subtract - but see the notes from execute1.vhdl):
> https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L540
> 
> cmp is definitely arithmetic, however cmpb feels like it is a
> logical-thing (and is in fixedlogical)
> https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L657
> https://github.com/antonblanchard/microwatt/blob/master/ppc_fx_insns.vhdl#L735
> https://github.com/antonblanchard/microwatt/blob/master/helpers.vhdl#L117
> 
> 
> btw, you'll like this: because we are doing a parallel processor,
> different Function Units *can* actually cover multiple tasks :)  let's
> not go into that right now, however if we convert power_enum Function
> into an unary field (1<<0, 1<<1, 1<<2) then we can, in the CSV files,
> set multiple bits.
> 
> a good example would be AND and OR and XOR: those are prime candidates
> to put into *both* the Logical *and* Arithmetic pipelines.  recorded
> it for now:
> https://bugs.libre-soc.org/show_bug.cgi?id=310
> 
> l.
> 
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev@lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev


-- 
Tobias Platen <libre-soc[at]platen-software[dot]de>

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Thu, May 14, 2020 at 4:49 PM Tobias Platen
<libre-soc@platen-software.de> wrote:

> Like Yesterday I am still working on the countzero.vhdl thing.

super.  btw i noticed that countzero.vhdl is two cycles.  feel free to
make the entire thing combinatorial (no use of sync).  we need the
algorithm, working, first.  making it faster by splitting across two
stages can be added later.

you'll see at line 98
https://github.com/antonblanchard/microwatt/blob/master/countzero.vhdl

that's a *synchronous* copy.  don't do that.  just make it a
combinatorial assignment.

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Jacob Lifshay]

I have been commenting on some of Rust's RFCs as well as on PyO3 issues:
link to my latest comment on forbidden values RFC:
https://github.com/rust-lang/rfcs/pull/2888#issuecomment-628789625

(some types in Rust aren't allowed to have certain values so rustc exploits
that fact to pack other information into those bytes to save space.
For example:
enum E {
    A,
    B,
    C(bool),
}

will probably only take one byte by using the byte values 2 and 3 for A and
B since bool can only be 0 or 1)

I'm planning on attending the OpenPower virtual coffee call later today,
and will try to make some progress on the load/store execution pipeline.

I may also work on a mul/div function unit, since Luke asked me to do that,
though I think integer mul should be part of the fp mul pipeline since they
can share multipliers, and integer div should be part of the
fdiv/idiv/irem/udiv/urem/fsqrt/frsqrt ALU pipeline that I wrote a lot of
previously.

Jacob
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Thu, May 14, 2020 at 7:28 PM Jacob Lifshay <programmerjake@gmail.com> wrote:
> (some types in Rust aren't allowed to have certain values so rustc exploits
> that fact to pack other information into those bytes to save space.

interesting!  and scary :)

> I'm planning on attending the OpenPower virtual coffee call later today,
> and will try to make some progress on the load/store execution pipeline.

cool.  my routine for a few days now:
bashing my head against the LD/ST FSM.... i do a little bit each morning,
scream loudly somewhere after lunch, and do a bit of ALU in the afternoon :)

> I may also work on a mul/div function unit, since Luke asked me to do that,

(btw i did popcount, if i can't stand the LD/ST FSM i'll try parity)

> though I think integer mul should be part of the fp mul pipeline since they
> can share multipliers, and integer div should be part of the
> fdiv/idiv/irem/udiv/urem/fsqrt/frsqrt ALU pipeline that I wrote a lot of
> previously.

yes.  so the DIV pipeline would need to be set up to take minimum 64-bit wide
ints, even though FP64 only takes... 53(?) for the mantissa.  likewise for MUL.

although a couple of things:

* i'd contemplated that there be some "hidden Function Units) and some
  rewriting of Function.OP_xxxx into "micro-ops"... this is complex so is
  off the "priority list"
* FP is also off the "critical priority" list for the 180nm test chip
* so is Partitioning

this drastically cuts down on complexity.

so although we can - and should - use the integer DIV ALU code that you wrote,
(and need to convert it to partitioning at some point) the partitioned
multiplier is
off the list.

this makes for a much simpler target and increases the chance of success for
our first test chip.

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Cole Poirier]

Yesterday I worked on the script that automates the build and
installation of yosys and the various SYMByosys tools until when trying
to compile super_prove bitbucket had an internal error failed to load
for over half an hour. At that point I decided to try again the next
day. Today the bitbucket is working. I had to create two patches for the
abc-zz sub-dependency of super_prove, now super_prove compiles
successfully. Given that this prevents the successful compilation of an
entire yosys tool, should I make a PR with these small but significant
patches or should I just be satisfied that it now works for us and move
on? The abc-zz dependecy lives in a bitbucket repo
(https://bitbucket.org/niklaseen/abc-zz/src/default/) that is over five
years old and the super_prove bitbucket repo's
(https://bitbucket.org/sterin/super_prove_build/src/default/) most
recent commit is in 2017. Given this, what would you advise I do with
regard to a PR/moving on?

I'm hoping to finish the rest of the yosys tools in the script today,
and tomorrow finsish the rest of the HDL_workflow.

Cole

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Michael Nolan]

On 5/14/20 5:48 PM, Cole Poirier wrote:
> Yesterday I worked on the script that automates the build and
> installation of yosys and the various SYMByosys tools until when trying
> to compile super_prove bitbucket had an internal error failed to load
> for over half an hour. At that point I decided to try again the next
> day. Today the bitbucket is working. I had to create two patches for the
> abc-zz sub-dependency of super_prove, now super_prove compiles
> successfully. Given that this prevents the successful compilation of an
> entire yosys tool, should I make a PR with these small but significant
> patches or should I just be satisfied that it now works for us and move
> on? The abc-zz dependecy lives in a bitbucket repo
> (https://bitbucket.org/niklaseen/abc-zz/src/default/) that is over five
> years old and the super_prove bitbucket repo's
> (https://bitbucket.org/sterin/super_prove_build/src/default/) most
> recent commit is in 2017. Given this, what would you advise I do with
> regard to a PR/moving on?
>
I've never been able to/never bothered to install super_prove or aiger 
for use with SymbiYosys. For running the formal proofs Libre-Soc has 
done, I think you only need one of the SMTBMC solvers (my recommendation 
is yices2).

--Michael


_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Cole Poirier]

On May 14 2020, at 3:00 pm, Michael Nolan <mtnolan2640@gmail.com> wrote:
> I've never been able to/never bothered to install super_prove or aiger 
> for use with SymbiYosys. For running the formal proofs Libre-Soc has 
> done, I think you only need one of the SMTBMC solvers (my
> recommendation 
> is yices2).
> 
> --Michael

Thanks for the tip Michael! I'll definitely keep your reccomendation to
use yices2 in mind when setting the default engine in the script (if I
do end up needing to set one, I'm not done yet), and for myself when I
start trying to use nmigen.

In that regard, Luke, after I am done with the scripts and the
modifications to the docs on the wiki, is there some testing
infrastructure that needs to be worked on, or should I try to start
learning to make nmigen HDL contributions to the project? Essentially,
what do you reccomend I do next that would be most helpful to the project?

Here is my code for a working super_prove installation in case you are
interested in trying it out:
```
 hg clone https://bitbucket.org/sterin/super_prove_build
 cd super_prove_build
 patch -u abc-zz/MetaSat/MiniSat2/System.cc <(echo "diff -r bde167bca3cd MetaSat/MiniSat2/System.cc
--- a/MetaSat/MiniSat2/System.cc    Thu Sep 14 01:44:08 2017 -0700
+++ b/MetaSat/MiniSat2/System.cc    Thu May 14 20:10:24 2020 +0000
@@ -20,6 +20,7 @@

 #include <signal.h>
 #include <stdio.h>
+#include <stdlib.h>

 #include "System.hh"

@@ -27,7 +28,6 @@

 #if defined(__linux__)

-#include <stdlib.h>

 static inline int memReadStat(int field)
 {
")
patch -u abc-zz/Bip/Main_bip.cc <(echo "diff -r bde167bca3cd Bip/Main_bip.cc
--- a/Bip/Main_bip.cc   Thu Sep 14 01:44:08 2017 -0700
+++ b/Bip/Main_bip.cc   Thu May 14 20:08:52 2020 +0000
@@ -508,8 +508,8 @@
 void writeCex(Out& out, NetlistRef N, const Cex& cex, uint orig_num_pis)
 {
     Vec<Pair<int,GLit> > ffs, pis;
-    For_Gatetype(N, gate_Flop, w) ffs.push(tuple(attr_Flop(w).number, w));
-    For_Gatetype(N, gate_PI  , w) pis.push(tuple(attr_PI  (w).number, w));
+    For_Gatetype(N, gate_Flop, w
)ffs.push(ZZ::tuple(attr_Flop(w).number, w));
+    For_Gatetype(N, gate_PI  , w) pis.push(ZZ::tuple(attr_PI 
(w).number, w));
     sort(ffs);
     sort(pis);

")
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release -G Ninja ..
ninja
ninja package
SPBIN=`find . -maxdepth 1 -name "super_prove*-Release.tar.gz"`
tar xvf $SPBIN -C /usr/local/bin/
cat << "EOF" > /usr/local/bin/suprove
#!/bin/bash
tool=super_prove; if [ "$1" != "${1#+}" ]; then tool="${1#+}"; shift; fi
exec /usr/local/bin/super_prove/bin/${tool}.sh "$@"
EOF
chmod +x /usr/local/bin/suprove
suprove
```

Cole

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Thu, May 14, 2020 at 11:29 PM Cole Poirier <colepoirier@gmail.com> wrote:

> In that regard, Luke, after I am done with the scripts and the
> modifications to the docs on the wiki, is there some testing
> infrastructure that needs to be worked on, or should I try to start
> learning to make nmigen HDL contributions to the project?

that would be a really good challenge to try anyway.  apart from anything
you'd be able to read / recognise the code as it evolves.

> Essentially, what do you reccomend I do next that would be most helpful to the project?

i have nooo idea :)  oh wait - i have an idea.  could you raise a
bugreport "bperm TODO",
look at the 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]

and see if you can write that in nmigen?  this 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)

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Thu, May 14, 2020 at 10:48 PM Cole Poirier <colepoirier@gmail.com> wrote:
>
> Yesterday I worked on the script that automates the build and
> installation of yosys and the various SYMByosys tools until when trying
> to compile super_prove bitbucket had an internal error failed to load
> for over half an hour. At that point I decided to try again the next
> day. Today the bitbucket is working. I had to create two patches for the
> abc-zz sub-dependency of super_prove, now super_prove compiles
> successfully. Given that this prevents the successful compilation of an
> entire yosys tool, should I make a PR with these small but significant
> patches or should I just be satisfied that it now works for us and move
> on?

report them, put the patch into the git repo with the scripts, put the
link to the patch
on the wiki, and move on.

i only use i think z3solver, yices2 and one other - i didn't bother
with any of the
others.

l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Yehowshua]

More Create-X stuff. Working on the pinout tonight with Luke’s Python code - will try to have it ready by tomorrow afternoon.

Yehowshua
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Friday, May 15, 2020, Yehowshua <yimmanuel3@gatech.edu> wrote:

> More Create-X stuff. Working on the pinout tonight with Luke’s Python code
> - will try to have it ready by tomorrow afternoon.


good.  then we can review.  Rudi cannot start until we have a clear
specification.

l.



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Tobias Platen]

I've now done the conversion of countzero.vhdl and most of the testbench.

Tobias

On Fri, 15 May 2020 09:28:09 +0100
Luke Kenneth Casson Leighton <lkcl@lkcl.net> wrote:

> On Friday, May 15, 2020, Yehowshua <yimmanuel3@gatech.edu> wrote:
> 
> > More Create-X stuff. Working on the pinout tonight with Luke’s Python code
> > - will try to have it ready by tomorrow afternoon.
> 
> 
> good.  then we can review.  Rudi cannot start until we have a clear
> specification.
> 
> l.
> 
> 
> 
> -- 
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
> _______________________________________________
> libre-riscv-dev mailing list
> libre-riscv-dev@lists.libre-riscv.org
> http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev


-- 
Tobias Platen <libre-soc[at]platen-software[dot]de>

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

On Friday, May 15, 2020, Tobias Platen <libre-soc@platen-software.de> wrote:

> I've now done the conversion of countzero.vhdl and most of the testbench.


fantastic.  next step, to put it into the Logical pipeline and write a
formal correctness proof (that's the bit that can receive donations!)



-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=HEAD

remember tobias, i said do not use sync, replace that with comb on the
intermediate result.

apart from anything this will make the unit test a great deal simpler to
write.


l.


On Friday, May 15, 2020, Luke Kenneth Casson Leighton <lkcl@lkcl.net> wrote:

>
>
> On Friday, May 15, 2020, Tobias Platen <libre-soc@platen-software.de>
> wrote:
>
>> I've now done the conversion of countzero.vhdl and most of the testbench.
>
>
> fantastic.  next step, to put it into the Logical pipeline and write a
> formal correctness proof (that's the bit that can receive donations!)
>
>
>
> --
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
>
>

-- 
---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

tobias, take note:

commit 4bca5df68e130da5d816cf0ab10182c4c1d27380 (HEAD -> master, origin/master)
Author: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date:   Fri May 15 11:54:35 2020 +0100

    make module combinatorial


---
crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68

On Fri, May 15, 2020 at 10:13 AM Luke Kenneth Casson Leighton
<lkcl@lkcl.net> wrote:
>
> https://git.libre-soc.org/?p=soc.git;a=commitdiff;h=HEAD
>
> remember tobias, i said do not use sync, replace that with comb on the intermediate result.
>
> apart from anything this will make the unit test a great deal simpler to write.
>
>
> l.
>
>
> On Friday, May 15, 2020, Luke Kenneth Casson Leighton <lkcl@lkcl.net> wrote:
>>
>>
>>
>> On Friday, May 15, 2020, Tobias Platen <libre-soc@platen-software.de> wrote:
>>>
>>> I've now done the conversion of countzero.vhdl and most of the testbench.
>>
>>
>> fantastic.  next step, to put it into the Logical pipeline and write a formal correctness proof (that's the bit that can receive donations!)
>>
>>
>>
>> --
>> ---
>> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
>>
>
>
> --
> ---
> crowd-funded eco-conscious hardware: https://www.crowdsupply.com/eoma68
>

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev

Re: [libre-riscv-dev] daily kan-ban update 14may2020

[Luke Kenneth Casson Leighton]

hey tobias, totally cool, the countzero unit test works! :)
l.

_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev