Wrote a post about limitations of the ISA-Formal technique for verifying processors #CAV2016 #ARM
https://alastairreid.github.io/alastairreid.github.io/isa-formal-limitations/ …
-
-
Replying to @alastair_d_reid
The issues with tools having bad Verilog language support you mentioned in the blog post: Verilog or SystemVerilog / SVA?
1 reply 0 retweets 0 likes -
Replying to @oe1cxw
Worst with SV. Made worse by me machine generating code so my code was already a bit unusual.
1 reply 0 retweets 1 like -
Replying to @alastair_d_reid
The big problem with SV is that there is no standard that defines a synthesizable subset (other than with Verilog). 1/
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @alastair_d_reid
So every vendor has to make its own definition where to draw the line between synthesizable and non-synthesizable. 2/
1 reply 0 retweets 0 likes -
Replying to @oe1cxw @alastair_d_reid
And formal is an entirely new 3rd category of something that must be some subset of full SV, but isn't well defined.. 3/
1 reply 0 retweets 0 likes
Are you using SV only in your checker code, or is the design SV as well? Any chance you guys will release code examples? /4
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.