[Libre-soc-bugs] [Bug 590] Formally verify experiments/icache.py

[bugzilla-daemon at libre-soc.org]

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

--- Comment #2 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Cole Poirier from comment #0)
> Presently, I'm taking inspiration from Cesar's excellent
> fu/compunits/formal/proof_fu.py, with detailed comments for each of the N
> properties that must hold for the formal verification to pass.

Thanks, but that's not my work. Here are some of mine:

A FSM Shifter with valid/ready handshake:

https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/experiment/formal/proof_alu_fsm.py;h=97f36a8f4529ab9515acea560cb33df73f0bbf51;hb=HEAD

The main thing here is counting input and output transfers, and asserting that
they are equal. Unless the unit is busy, then they differ by one.

Partitioned Signals:

https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part/formal/proof_partition.py;h=f2ef30740d6566774aa6812936ce8a5bdd437727;hb=HEAD

This one seems pretty complex, but it really is all about implementing the
strategy defined in the first paragraph.

Anyway, for the ICache I would recommend first to understand what it is
supposed to do. Maybe, capture a VCD trace from a Microwatt simulation, and
read the code while following the traces.

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