Slides and additional materials for my #orconf talk on formal verification of safety properties with Yosys-SMTBMC: http://www.clifford.at/papers/2016/yosys-smtbmc/ …
-
Quick silly question -- are there inbuilt SysV constructs for asserting time-delayed properties, or you need to explicitly delay?
Right now only pure expressions are allowed as properties. So no ##1 etc. You have to build FSMs to check stuff like that atm
