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

[bugzilla-daemon@libre-soc.org]

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

Cesar Strauss <cestrauss@gmail.com> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |cestrauss@gmail.com

--- Comment #29 from Cesar Strauss <cestrauss@gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #27)
> basically i have no idea what i am doing with Formal Proofs.  i can read
> them, i can *maybe* spot omissions once they're written, and i can just about
> manage combinatorial ones.  these sync/time-based ones: really no idea.

Hi Luke,

As I learned about formal verification, I found the initial slides of
http://www.clifford.at/papers/2017/smtbmc-sby/slides.pdf very enlightening for
basic concepts. See for instance slides 6 to 16.

(In reply to Luke Kenneth Casson Leighton from comment #28)
> https://zipcpu.com/blog/2018/03/10/induction-exercise.html
> 
> all i can say is: argh :)

This illustrates the difficulties in induction proofs.

It is apparent, from the circuit, that the two shift-registers will be equal
for all time, so the XOR output will be always zero.

However, bounded model check can only check for a finite number of cycles. To
prove it for all time, you prove it that, whenever the assertions hold for n
cycles, it will hold for the n+1 cycle.

The problem with induction, is that it does not start with the initial state
(see slide 11). So, the "initial" state can be in the unreachable state area
(see slide 9).

In the example, an initial state in which the shift register are different, is
unreachable. But the proof checker does not know that. So, it can choose an
initial state where the last bit is equal, passing the assertion, but the
next-to-last bit is different.

Then, it holds the shift enable de-asserted for n cycles and asserts it for the
n+1 cycle, finally shifting out the differing bits. So, it passes for n cycles,
but fails in n+1.

The easy way to solve this is to assert that the shift register contents are
always equal.

Another way is limiting the time in which the shift-enable can be kept
de-asserted. This is done with an assumption.

Without an assumption, the proof checker is free to toggle any unconnected
input signal, in the most perverse way possible, to make the proof fail. In
reality, the input signals must obey some protocol. For instance, you tell the
proof checker that it must keep (assume) issue_i low whenever busy_o is high.
Otherwise it would be free to assert issue_i in the middle of a busy_o cycle,
which it's a violation of the protocol.

Hope it helps,

Cesar

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