You can add location information to your Tweets, such as your city or precise location, from the web and via third-party applications. You always have the option to delete your Tweet location history. Learn more
I built an interlock for a nontrivial 8-stage pipeline with 3 stages that access the same single-port mem. Instruction sequences where multiple stages access mem at the same time are hazardous and must by avoided by adding bubbles. I completed the task in under 30 minutes. #ABVpic.twitter.com/O5CVCuvCu2
Here are some pieces of the interlock itself. As you can see the code is rather simple. But verifying that it is actually correct for all possible instruction sequences would be close to implossible using non-formal approaches such as functional coverage. #ABV #Formalpic.twitter.com/0un7XRoZZr
Have you got a link to a non-trivial case study for this kind of formal verification?
See for example this paper from 2013: https://link.springer.com/chapter/10.1007/978-3-642-41010-9_6 … They used PSL insted of SVA for their properties, but for the most part that's just another syntax. (PSL used to be popular with VHDL. Now SVA pretty much won and people just write their properties in SystemVerilog.)
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.
