Does anyone have a simple VHDL project with formal safety properties that I could use as test case for Yosys+Verific+SymbiYosys?
-
-
Replying to @oe1cxw
If you're looking for something as simple as a FIFO, I got it here https://github.com/olofk/libstorage …
1 reply 0 retweets 0 likes -
Replying to @OlofKindgren
I don't see any formal properties. Am I missing something?
1 reply 0 retweets 0 likes -
Replying to @oe1cxw
Oh, sorry. Just thought you wanted something that could easily be formally verified
1 reply 0 retweets 1 like -
Replying to @OlofKindgren
might still be a good starting point, if I figure out the syntax for safety properties in VHDL.. not many examples online.
1 reply 0 retweets 0 likes -
Replying to @oe1cxw
Safety properties == PSL? I used to do formal verification of VHDL with PSL ~10 years ago
1 reply 0 retweets 0 likes -
Replying to @OlofKindgren
PSL would be one way. assert/assume in processes another. I'm now testing with this example using PSL that I found online.pic.twitter.com/MNrljwuAa2
2 replies 0 retweets 0 likes -
Replying to @oe1cxw @OlofKindgren
How about you use our PSL book code?
@ajeetha_cvc can send it via email if needed1 reply 0 retweets 0 likes
thanks, that would be very useful.
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.