| 基于事务形式验证(TBFV)及8051的TBFV模型 |
| |
| 引用本文： | 王彬,林争辉.基于事务形式验证(TBFV)及8051的TBFV模型[J].上海交通大学学报,2003,37(10):1574-1577. |
| |
| 作者姓名： | 王彬 林争辉 |
| |
| 作者单位： | 上海交通大学,电子工程系,上海,200030 |
| |
| 基金项目： | 美国国家科学基金(5978EastAsiaandPacificProgram-9602485)，国家教育部博士点基金资助项目 |
| |
| 摘 要： | 提出了一种基于事务的形式验证方法(TBFV)，为待验证的系统构造功能验证模型，每个模型包括指令序列、输入变量、输出变量、输出函数、输出判定函数．这些可用Kripke结构来描述．这些功能验证模型实现了特定的事务，从而可以将一般的验证要求映射为具体的实现属性．这样，验证者无需了解设计的细节，可在较高层次上对系统行为进行验证．为了证明该方法的效率，分别用该方法和传统的形式验证方法验证了8051的RTL实现．8051中所有的指令都进行了验证，并给出了相应的功能验证模型．实验结果表明，采用该方法可大大节省验证工程师的时间．功能验证模型和验证指令可以在其他设计中复用．
|
| 关 键 词： | 基于事务的形式验证 功能验证模型 状态爆炸 |
| 文章编号： | 1006-2467(2003)10-1574-04 |
| 修稿时间： | 2002年11月10 |
Transaction Based Formal Verification (TBFV) and TBFV Models for 8051 |
| |
| Abstract: | |
| |
| Keywords: | transaction based formal verification(TBFV) functional verification model state explosion |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
