[libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed

[bugzilla-daemon at libre-soc.org]

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

--- Comment #2 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cole Poirier from comment #1)
> Made some very minimal progress on this today. Since I'm still learning how
> to write proofs it takes a long time to get the most basic assumptions of
> the most basic class (Register) from regfile.py sorted enough that I can
> start to reason about them. I think the foundation that I laid today will
> enable me to write some code for this (instead of just written notes from
> working and reasoning through the assumptions of the module) tomorrow. But,
> if this proof is needed before then for the virtual_port tests,

it's not.  i have a preliminary virtual_port test running, yesterday.

> Luke please
> feel free to take it over like you did with virtual_port today. I want to
> help, so I don't want my learning while working slowly to be a blocker :)

i don't totally get them either, so we work on it together, over time, ok?

as you have probably noticed, i tend to write "proof-of-concept" unit
tests that at least give a basic level of confidence then move quickly
on.  this will allow rapid progress but will bite us in corner-cases.

-- 
You are receiving this mail because:
You are on the CC list for the bug.