协同形式验证环境Co-Formal的建立与应用

Setup and Applications of the Co-Formal Verification Environment Co-Formal

形式验证存在状态爆炸的问题,特别是软硬件的协同验证难以解决.为此研究了片上系统的协同形式验证问题,给出了一种高效的协同形式验证环境Co-Formal,用于从行为级到具体实现级的软硬件协同形式验证.以一个实际的硬件系统验证了该环境的可用性.

Formal verification has attracted great interests in recent years. But the real world system is too complex to be verified directly by symbolic model checking because of state explosion. Another difficulty in validation of system on chip (SoC) is how to coverify of HW/SW. This paper is focused on the coformal verification for SoC. It presented an effective formal coverification environment CoFormal. In this environment, we can coverify a system at behavior level and implementation level. A real circuit system was verified to illustrate the usage of this environment.