硬件设计的形式化验证技术

Formal Verification of Hardware Designs

形式化验证用数学可证明的方式来验证系统.硬件设计的形式化验证通常有三种方法:定理证明、等价性检验和模型检验.文章着重分析了这三种方法的优缺点,探讨了形式化验证技术所面临的挑战,以及目前形式化验证技术可能的一些研究方向.

Formal verification use a provable approach to verification the system. There are three methods for Hardware design verificat ion,namely theorem proving,equivalence checking, and model checking. An overview of these methods is presented. The merits and demerits of each method are dis cussed. We also make a few comments of the challenges that formal verification faced and the future research directions.