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

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

[Luke Kenneth Casson Leighton]

yesterday:

* reviewed Michael's formal proof for MultiCompUnit
* helped Cesar with the parallel-simulation for MultiCompUnit
* started (with Cole) a "virtual port" on a register file
* reviewed Tobias's DataMerger data structure and added notes

this morning:

* spoke to tropicsquare (like their idea of doing a secure chip)
* moved the treereduce function from regfile.py into nmutil.utils and
  made it a map-reduce function.
* tried implementing the "virtual port" regfile only to find it had
 partially been done in RegFileArray (but not quite).

today:

* continue with the regfile thing (we really need it)
* keep an eye on list and bugtracker

_______________________________________________
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 26may2020

[Cesar Strauss]

Yesterday:

* Started with the parallel simulation for MultiCompUnit. In the
process, gained a good understanding of parallel simulation in nMigem,
as well as the issue_i/busy_o protocol.

This morning:

* Found out about ongoing formal proof work on the very module to which
I'm adding unit tests. Interesting subject, formal proofs. I've been
learning it myself, in order to apply it to my work, but have as yet no
practical experience.

Today:

* Advance on the parallel tests. Hopefully, get good progress on the
rd/wr protocol.

Regards,

Cesar

_______________________________________________
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 26may2020

[Michael Nolan]

Yesterday, I worked on familiarizing myself with the MultiCompUnit, and 
began writing a formal proof for it. Today, I'd like to refactor that 
proof to better match up with the description on the wiki page.

Also, summer classes began today for me, so I may be less productive on 
Libre-SOC for the next two months.

--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 26may2020

[Cole Poirier]

Yesterday:

Did a very small amount of work on the virtual port with luke, I believe
he's taken this over, which is good because I was struggling and this is important.

Today:

Yesterday Luke asked me to raise a bug report for RegFile and
RegFileArray proofs needed, so today I plan on trying to formally prove
regfile. Input or advice on this at bug 353 is appreciated.
(https://bugs.libre-soc.org/show_bug.cgi?id=353)

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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 5:44 PM Cesar Strauss <cestrauss@gmail.com> wrote:

> * Found out about ongoing formal proof work on the very module to which
> I'm adding unit tests. Interesting subject, formal proofs. I've been
> learning it myself, in order to apply it to my work, but have as yet no
> practical experience.

samuel falvo was the first one to explain the benefits of formal proofs.
http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/96ea88450c1a3fc6

the insight that he gave particularly hit home when we had to run
literally hundreds of thousands of tests (which takes about a week to
run) for the IEEE754 FPU...

... and yet, despite that, we *still have no guarantee of hitting all
corner-cases*.

so we have hundreds of thousands of tests - with no guarantee - or, we
write *ONE* formal proof that covers them all.

it's not a difficult choice to make.

> Today:
>
> * Advance on the parallel tests. Hopefully, get good progress on the
> rd/wr protocol.

one step at a time.

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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 5:47 PM Michael Nolan <mtnolan2640@gmail.com> wrote:
>
> Yesterday, I worked on familiarizing myself with the MultiCompUnit, and
> began writing a formal proof for it. Today, I'd like to refactor that
> proof to better match up with the description on the wiki page.

that's quite funny, because i am refactoring the wiki page to help
make it easier to write the proof :)

> Also, summer classes began today for me, so I may be less productive on
> Libre-SOC for the next two months.

ok cool, thanks for letting us know.  most of the pipelines has been
done, it should be plain sailing from here.

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 26may2020

[Luke Kenneth Casson Leighton]

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

On Tue, May 26, 2020 at 6:02 PM Cole Poirier <colepoirier@gmail.com> wrote:
>
> Yesterday:
>
> Did a very small amount of work on the virtual port with luke, I believe
> he's taken this over, which is good because I was struggling

so am i.  sigh.

> and this is important.

please do keep an eye on it, keep asking questions ok?

> Today:
>
> Yesterday Luke asked me to raise a bug report for RegFile and
> RegFileArray proofs needed, so today I plan on trying to formally prove
> regfile. Input or advice on this at bug 353 is appreciated.
> (https://bugs.libre-soc.org/show_bug.cgi?id=353)

start from the proof_bperm.py or proof_fu.py as the basic template.
we can work it out.

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 26may2020

[Cole Poirier]

On May 26 2020, at 10:24 am, Luke Kenneth Casson Leighton
<lkcl@lkcl.net> wrote:
> On Tue, May 26, 2020 at 6:02 PM Cole Poirier <colepoirier@gmail.com> wrote:
>> 
>> Yesterday:
>> 
>> Did a very small amount of work on the virtual port with luke, I believe
>> he's taken this over, which is good because I was struggling
> 
> so am i.  sigh.
> 
>> and this is important.
> 
> please do keep an eye on it, keep asking questions ok?

Will do. It's very, very helpful to have tried *some* kind of
implementation on my own, because now I am studying yours and filling in
the myriad missing things that I was searching my brain for but didn't
yet understand.
 
>> Today:
>> 
>> Yesterday Luke asked me to raise a bug report for RegFile and
>> RegFileArray proofs needed, so today I plan on trying to formally prove
>> regfile. Input or advice on this at bug 353 is appreciated.
>> (https://bugs.libre-soc.org/show_bug.cgi?id=353)
> 
> start from the proof_bperm.py or proof_fu.py as the basic template.
> we can work it out.

Great. Going to spend another half hour studying virtual_port then will
start on this.

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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 6:29 PM Cole Poirier <colepoirier@gmail.com> wrote:

> Great. Going to spend another half hour studying virtual_port then will
> start on this.

i have a feeling we just call RegFileArray.read_port() and write_port,
then not let anyone access the 8 reg-ports, throw away the "global"
thing and create the alternative one.

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 26may2020

[Luke Kenneth Casson Leighton]

michael, my partner, marie, who is from alaska, pointed out that the
work that you're doing on Libre-SOC should, if you ask the professors,
be considered coursework towards your degree.  worth considering?
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 26may2020

[Michael Nolan]

On 5/26/20 1:49 PM, Luke Kenneth Casson Leighton wrote:
> michael, my partner, marie, who is from alaska, pointed out that the
> work that you're doing on Libre-SOC should, if you ask the professors,
> be considered coursework towards your degree.  worth considering?
> l.
>
Thank you, yes I am considering it. This fall I'm taking "Senior Project 
Proposal" (or something like that), and I'm planning on asking if I can 
possibly use this as my senior project.

--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 26may2020

[Cole Poirier]

On May 26 2020, at 10:35 am, Luke Kenneth Casson Leighton
<lkcl@lkcl.net> wrote: 
> i have a feeling we just call RegFileArray.read_port() and write_port,
> then not let anyone access the 8 reg-ports, throw away the "global"
> thing and create the alternative one.

Having done a close read of regfile/virtual_port.py (apologies for
giving a "terrible name for a complex register"), and reviewing the
yosys show top logic diagram I think I mostly understand what's going on
in this module.

Regarding the "global" thing, are you referring to the self.wr/rd_ports
"for external use"? We should instead just use the existing methods on
RegFileArray to set up the external ports? How do we go about not
letting anyone access the 8 reg-ports?

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 26may2020

[Jacob Lifshay]

yesterday:
wrote a program to analyse the values POWER9 produces for instructions
where the spec doesn't define the results, see
https://bugs.libre-soc.org/show_bug.cgi?id=324#c5

today:
continuing working on the MUL and DIV pipelines.

Is Cesar taking over the load/store pipeline? I never got much done on it.

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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 7:00 PM Cole Poirier <colepoirier@gmail.com> wrote:
>
> On May 26 2020, at 10:35 am, Luke Kenneth Casson Leighton
> <lkcl@lkcl.net> wrote:
> > i have a feeling we just call RegFileArray.read_port() and write_port,
> > then not let anyone access the 8 reg-ports, throw away the "global"
> > thing and create the alternative one.
>
> Having done a close read of regfile/virtual_port.py (apologies for
> giving a "terrible name for a complex register"),

it works :)

> and reviewing the
> yosys show top logic diagram I think I mostly understand what's going on
> in this module.

it's basically multiplexing between 8 individual ports and 1 massive
port that hits absolutely all of the (8) ports at once.

which, when put like that, we might as well do exactly that.


> Regarding the "global" thing, are you referring to the self.wr/rd_ports
> "for external use"? We should instead just use the existing methods on
> RegFileArray to set up the external ports? How do we go about not
> letting anyone access the 8 reg-ports?

that's the Dep-Matrices job.  or, more to the point: the PriorityPickers.

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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 8:13 PM Jacob Lifshay <programmerjake@gmail.com> wrote:
>
> yesterday:
> wrote a program to analyse the values POWER9 produces for instructions
> where the spec doesn't define the results, see
> https://bugs.libre-soc.org/show_bug.cgi?id=324#c5

interesting.  and useful.

> today:
> continuing working on the MUL and DIV pipelines.

great.

> Is Cesar taking over the load/store pipeline?

Tobias is currently doing the data-merger "thing", Cesar is happy to
do a L0CacheBuffer unit test - between all of us we should get
something done.

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 26may2020

[Tobias Platen]

this morning:
	nothing
this evening:
	more work on DataMerger.elaborate which is now nearly finished.

_______________________________________________
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 26may2020

[Luke Kenneth Casson Leighton]

On Tue, May 26, 2020 at 8:54 PM Tobias Platen
<libre-soc@platen-software.de> wrote:
>
> this morning:
>         nothing
> this evening:
>         more work on DataMerger.elaborate which is now nearly finished.

great!

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