08:16 <shorne> Anyone have much experience with formal verification? In particular yosys?

08:17 <shorne> I have been spending the last few weeks really deep diving into it to formally verify mor1kx dcache and LSU. This was done partially for Google Summer of Code last year, but I am changing the approach

08:17 <shorne> just want to talk out some idea's. So here we go...

08:18 <shorne> Someone said Test benches are for ensuring you system is valid for the TB provided inputs. Formal verification is for ensuring your system works for any valid inputs.

08:19 <shorne> My take-away, the formal verification is only as good as your definition of valid inputs. So its no silver bullet

08:19 <shorne> maybe I should chat on #yosys

15:17 <_florent_> shorne: I share the same feelings on formal: testbenches and formal verification complement each others. Testbenches are useful to design your system, test it in practical use-cases (and are useful for later for debug, to reinject behavior seen on hardware, etc...) and formal can ease some testing of some specific parts: testing an AsyncFIFO is for example a lot more efficient and will give more confidence with formal).

15:18 <_florent_> shorne: Injecting randomness on testbenches is also a good intermediary step before doing formal

15:21 <_florent_> shorne: but yes, saying that your system is formally verified does not have lot more value that saying it's passing the testbenches, both are complementary :)