A novel formal verification approach for RTL hardware IP cores

摘要

We present a promising formal verification methodology based on the inductive approach using the imPROVE-HDL tool. This methodology is dedicated for RTL IPs or IP-based digital/logic hardware designs to prove the correctness of their temporal properties related to the control-dominated architecture model. Each temporal property can be checked through the IP interface where all properties have to be proved or disproved. We developed a new methodology to generate the appropriate environment of the IP interface according to the design context (master, slave, arbiter and decoder) before starting the verification of all properties one by one. When all temporal properties are verified, we generate some test sequences that contain a complex scenario to check the compatibility between all properties. We implemented our methodology to generate the appropriate environment and applied the inductive approach to verify various properties of two real IP designs using the imPROVE-HDL tool developed by TNI-Valiosys. The first design is an RTL IP-based digital hardware dedicated for real time video processing, where the second one performs an AHB to AHB Bridge. On these designs, we successfully proved few properties and discovered a design violation.