[libre-riscv-dev] [Bug 318] fix LDSTCompUnit

[bugzilla-daemon@libre-soc.org]

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

--- Comment #17 from Luke Kenneth Casson Leighton <lkcl@lkcl.net> ---
(In reply to Cesar Strauss from comment #16)
> I'll now proceed to improve the unit test for LDSTCompUnit.
> 
> I'll take into account your several ideas in comment #11.
> 
> Some of my own ideas are:
> 
> 1) The test driver should only present data during a single cycle,
> coincident with the activation of "go". This detects data being latched at
> the wrong time.

oh yeh, really good point.

> 
> 2) Add some behavioral assertions.
> For instance, busy_o must rise if, and only if, issue_i was active on the
> previous clock.
> Likewise "rel" signals must go low if, and only if, the corresponding "go"
> was active on the previous clock.
> And so on.

i believe these kinds of things are what Formal Proofs are for.  in particular,
when you use Past() to assert things from previous cycles.

> There could be a simulation "process" monitoring these kind of conditions.
> Or, using nMigen assertions, and/or formal verification. I must find out
> more about this.

bug 316, look up the formal_bperm.py code.  it's really well documented.

> I still need to study the interface and functionality of the L0CacheBuffer.

i tried two LDs in the score6600 code - they failed.  the first place to check
is the [prototype] L0CacheBuffer, with a twin-process.

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