形式化验证方法用于核电厂数字化仪控系统HPD验证的探索与实践

Discussion and Practice on Formalized Verification Method Applied to HPD Verification of Nuclear Power Plant Digital I&C Systems

为提高核电厂数字化仪控系统中HPD(HDL-Programmed Device)验证工作的效率和有效性,从而帮助提高仪控系统可靠性,引入形式化验证方法。形式化验证方法与传统的基于功能仿真的验证方法相比可以更有效地发现系统设计中的错误,更充分地验证系统设计,更方便地对验证流程进行管理。目前基于断言的形式化验证方法已经在大规模ASIC设计,以及数字通信领域HPD设计的功能验证中取得了成功,本文将这一方法引入核安全级系统HPD验证实践中,主要介绍HPD形式化验证的特点、原理和方法,以及其在FirmSys系统安全级HPD验证工作中的初步应用。