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

From: bugzilla-daemon@libre-soc.org
To: libre-riscv-dev@lists.libre-riscv.org
Subject: [libre-riscv-dev] [Bug 353] formal proof of soc.regfile classes RegFile and RegFileArray needed
Date: Wed, 27 May 2020 16:45:13 +0000
Message-ID: <bug-353-13-0PUtcMqZoo@https.bugs.libre-soc.org/> (raw)
In-Reply-To: <bug-353-13@https.bugs.libre-soc.org/>

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

--- Comment #3 from Cole Poirier <colepoirier@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>
    test_regfile()
  File "virtual_port.py", line 200, in test_regfile
    vcd_name='test_regfile_array.vcd')
  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.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev