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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Wed May 27 17:45:13 BST 2020


--- Comment #3 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #2)
> (In reply to Cole Poirier from comment #1)
> > if this proof is needed before then for the virtual_port tests,
> it's not.  i have a preliminary virtual_port test running, yesterday.

Saw your 'proof-of-concept' test case yesterday, was helpful for understanding
the functionality of the module further. Unfortunately, I think this test is
now failing with the following error:

Traceback (most recent call last):
  File "virtual_port.py", line 203, in <module>
  File "virtual_port.py", line 200, in test_regfile
  File "/home/colepoirier/src/nmigen/nmigen/compat/sim/__init__.py", line 22,
in run_simulation
    fragment.domains += ClockDomain("sync")
AttributeError: 'VirtualRegPort' object has no attribute 'domains'

I suspect it's a simple fix, but the answer is not immediately apparent to me.

> > 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.

Indeed, it seems to be a very productive strategy. Looking forward to working
with you on the proof today. Just reviewing my notes now, should have some code
for some of the basic assumptions committed in the next hour.

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

More information about the libre-riscv-dev mailing list