[Libre-soc-dev] daily kanban update 7-FEB-2021

[Cole Poirier]

On Sunday, February 7, 2021, Luke Kenneth Casson Leighton <lkcl at lkcl.net>
wrote:

> On Sunday, February 7, 2021, Cole Poirier <colepoirier at gmail.com> wrote:
>
> link it to the coriolis2 bugs so it doesn't get lost.


It’s linked to the ‘determine SRAM block size’ one, bug 502. Should I link
it to additional bugs?


> > I have also filed a bug for
> > my attempt at formally verifying icache.py.
>
> mmm yeah that one's a handful.  open-ended massive amounts of work.
>

Yeah I was immediately overwhelmed.


> > Is there a budget available for these tasks? Please let me know if I
> > have incorrectly filled in any of the fields on these bug reports.
>
> icache is too large.  others ok.


Understood. Can you comment on the ‘icache formal verification’ bug I
opened so we can discuss the approach to formally verify it, if at all?

I’d like to focus on writing formal proofs after doing the yosys SRAM
scripts, I think this would be helpful to the project as well as helping me
understand how the fu’s and architecture works throughly. Should I perhaps
start with formally verifying much smaller and simpler modules and
eventually work my way up to the caches? Is there a list of outstanding
modules that need formal proofs and some kind of priority or order that I
should work through them in?

> I'm now going to finish up the work on the JTAG debugger setup page
> > from last year;
>
> great.  we need that.
>

:)


> > I'm not going to take time on list with this,
> > except once I've solved it/it's done, tested, and potentially ready
> > for use (after the tapeout obviously), but I wanted to fill in the
> > team on the list just because.
>
> let JP know.
>

I think I should wait to let him know until after the tapeout so as to not
distract him or stress him unnecessarily. Is there a reason I should tell
him now?

Cole