| 形式验证中同步时序电路的VHDL描述到S2-FSM的转换 |
| |
| 引用本文： | 贝劲松,李洪星,边计年,薛宏熙,洪先龙. 形式验证中同步时序电路的VHDL描述到S2-FSM的转换[J]. 计算机辅助设计与图形学学报, 1999, 0(3) |
| |
| 作者姓名： | 贝劲松 李洪星 边计年 薛宏熙 洪先龙 |
| |
| 作者单位： | 清华大学计算机科学与技术系,北京,100084 |
| |
| 基金项目： | 国家“九五”项目,211工程资助 |
| |
| 摘 要： | 符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ，ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模，即如何建立并用有限内存来表示电路的状态机模型；另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的，因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ，并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的，消去了与时钟无关的大量中间变量，所以同Ｄｅｈａｒｂｅ提出的模型相比，它的状态数大大减少．若干电路的实验结果表明，该模型由于减少了状态规模，建模时间和可达性分析时间大大减少，效果十分显著．
|
| 关 键 词： | 形式验证 符号模型检查 有限状态机 二叉判决图 |
S2-FSM:A VERIFICATION-ORIENTED MODEL OF SYNCHRONOUS SEQUENTIAL CIRCUITS AND ITS MODELING ALGORITHM |
| |
| BEI Jin-Song,LI Hong-Xing,BIAN Ji-Nian,XUE Hong-Xi,HONG Xian-Long. S2-FSM:A VERIFICATION-ORIENTED MODEL OF SYNCHRONOUS SEQUENTIAL CIRCUITS AND ITS MODELING ALGORITHM[J]. Journal of Computer-Aided Design & Computer Graphics, 1999, 0(3) |
| |
| Authors: | BEI Jin-Song LI Hong-Xing BIAN Ji-Nian XUE Hong-Xi HONG Xian-Long |
| |
| Abstract: | |
| |
| Keywords: | VHDL |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
