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

王彬; 林争辉

首页> 中文期刊> 《上海交通大学学报》 >基于事务形式验证(TBFV)及8051的TBFV模型

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

开具论文收录证明 >>

期刊封面封底目录下载 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

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

著录项

来源
《上海交通大学学报》 |2003年第10期|1574-1577|共4页
作者
王彬; 林争辉;
展开▼
作者单位

上海交通大学电子工程系;

展开▼
原文格式 PDF
正文语种 chi
中图分类设计、分析、计算;
关键词
基于事务的形式验证; 功能验证模型; 状态爆炸;

相似文献

中文文献
外文文献
专利

1. 事务级形式验证技术及8051验证模型 [J] . 王彬 ,任艳颖 ,林争辉 . 计算机辅助设计与图形学学报 . 2003,第008期
2. 基于Petri网的Web服务事务模型形式化构建及基于贝叶斯网络的事务可靠性研究 [J] . 陈平 ,王兴建 ,党德鹏 . 通信学报 . 2018,第0z1期
3. 事务所变更的“年报形式质量之谜”及其经济后果--基于模板化披露的经验证据 [J] . 王嘉鑫 ,王永海 . 审计研究 . 2020,第3期
4. 基于细胞膜演算的Web服务事务处理形式化描述与验证 [J] . 戚正伟 ,尤晋元 . 计算机学报 . 2006,第007期
5. 基于服务协调模型的业务事务验证方法 [J] . 袁敏 ,黄志球 ,李祥 . 计算机集成制造系统 . 2012,第003期
6. 基于Petri网的Web服务事务模型形式化构建及基于贝叶斯网络的事务可靠性研究 [C] . CHEN Ping ,陈平 ,WANG Xinjian . 中国教育和科研计算机网CERNET第二十五届学术年会 . 2018
7. 基于PWA模型的显式模型预测控制与形式验证 [A] . 杨璞 . 2016

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

摘要

著录项

相似文献

相关主题

期刊订阅