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

• 作者: 林争辉 王彬
• 来源期刊: 上海交通大学学报
• 学科: 工学
• 关键词: 基于事务的形式验证 功能验证模型 状态爆炸
• 年，卷（期）: 2003,（10）
• 所属期刊栏目: 无线电电子学、电信技术
• 页码范围: 1574-1577
• 页数: 4页
• 分类号: TN702
• 字数: 2214字
• 语种: 中文
• DOI: 10.3321/j.issn:1006-2467.2003.10.021

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	林争辉	上海交通大学电子工程系	116	603	12.0	20.0
2	王彬	上海交通大学电子工程系	27	88	6.0	7.0