[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

--- Comment #36 from Cole Poirier <colepoirier@gmail.com> ---
(In reply to Cesar Strauss from comment #29)
> (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

Thank you very much for sharing this to help me Cesar, it's super helpful, and
I'm incredibly grateful for your help.

Cole

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