Can semi-formal be made more formal?

Capacity limitations continue to impede widespread adoption of formal property verification in the design validation flow of software and hardware systems. The more popular choice (at least in the hardware domain) has been dynamic property verification (DPV), which is a semi-formal approach where the formal properties are checked over simulation runs. DPV is highly scalable and can Support a significantly richer specification language as compared to languages Supported by formal property verification tools. Though the main limitations of DPV revolve around its dependence on the coverage of the relevant scenarios by simulation, there appears to be ample scope of addressing these issues through new formal methods for coverage and consistency analysis. We survey some of the formal methods developed by us in this direction, that can aid DPV in becoming more effective in practice and more formal in nature. We also present a new platform for performing DPV over state-event based software systems.