基于事务形式验证(TBFV)及8051的TBFV模型

Transaction Based Formal Verification (TBFV) and TBFV Models for 8051

提出了一种基于事务的形式验证方法(TBFV),为待验证的系统构造功能验证模型,每个模型包括指令序列、输入变量、输出变量、输出函数、输出判定函数.这些可用Kripke结构来描述.这些功能验证模型实现了特定的事务,从而可以将一般的验证要求映射为具体的实现属性.这样,验证者无需了解设计的细节,可在较高层次上对系统行为进行验证.为了证明该方法的效率,分别用该方法和传统的形式验证方法验证了8051的RTL实现.8051中所有的指令都进行了验证,并给出了相应的功能验证模型.实验结果表明,采用该方法可大大节省验证工程师的时间.功能验证模型和验证指令可以在其他设计中复用.

A TBFV (transaction based formal verification) methodology for verification of circuit system was presented. The functional verification models should be constructed for the system under validation. Every model includes instruction sequence, input variables, output variables, output functions and output judgment functions. They can be described in Kripke structure. These functional verification models implement some specific transactions, can map the common verification requirements into detailed implementation properties, so the validation engineer can verify their system at a behavior level, needn't understand the detailed implementation. For illustration, the RTL implementation of 8051 is verified in this method and in the traditional formal verification method respectively. All the instructions in 8051 are verified, and the functional verification models are given. The experimental results show that this method can greatly save the time. The functional verification models and verification instructions can be reused in other designs.