形式验证中同步时序电路的VHDL描述到S2-FSM的转换

• 作者: 李洪星 洪先龙 薛宏熙 贝劲松 边计年
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 形式验证 符号模型检查 VHDL 有限状态机 二叉判决图
• 年，卷（期）: 1999,（3）
• 所属期刊栏目: 全国第10届CAD与CG学术会议论文选
• 页码范围: 196-199
• 页数: 4页
• 分类号: TP302
• 字数: 5319字
• 语种: 中文
• DOI: 10.3321/j.issn:1003-9775.1999.03.002

摘要

符号模型检查(Symbolic Model Checking, SMC)是一种有效的形式验证方法.该方法主要有2个难点:一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法.由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为SMC中的关键问题.本文提出一种基于同步电路行为描述的新的有限状态机模型S2-FSM，并给出从同步电路的VHDL描述建立这种模型的过程.由于该模型的状态转换函数是基于时钟周期的，消去了与时钟无关的大量中间变量，所以同Deharbe提出的模型相比，它的状态数大大减少.若干电路的实验结果表明，该模型由于减少了状态规模，建模时间和可达性分析时间大大减少，效果十分显著.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	边计年	清华大学计算机科学与技术系	50	326	9.0	16.0
2	薛宏熙	清华大学计算机科学与技术系	15	93	6.0	9.0
3	洪先龙	清华大学计算机科学与技术系	114	410	9.0	11.0
4	贝劲松	清华大学计算机科学与技术系	3	19	2.0	3.0
5	李洪星	清华大学计算机科学与技术系	1	9	1.0	1.0