模型检验器前端系统的设计与实现

摘要

设计大规模的复杂的数字系统中关键问题之一是如何检查设计的正确性。但是，传统的验证技术例如模拟、仿真和测试，只能针对某些典型的情况或随机进行，这就难以完全排除所有设计错误。传统的验证技术已经无法适应目前集成电路芯片技术高速发展的需求。
　　本论文就是针对上述问题，研究一种新的验证技术－模型检验。模型检验的基本思想是用分支时态逻辑公式 f表达系统（程序或电路）的所期望的性质，用有限状态机（Kripke结构）M={S，R，L}表示系统的状态转移结构，通过遍历有限状态机来检验时态逻辑公式的正确性 f:{s∈S|M，s|=f}。如不能验证公式 f的正确性，系统将给出一个反例，使用户发现公式不成立的原因。
　　模型检验不能直接对硬件电路设计描述文件（如Verilog程序）进行验证，必须将硬件电路设计描述文件转换为有限状态机。本论文就是为了解决这个问题，研究模型检验器的前端系统，即如何从硬件描述语言Verilog提取有限状态机。
　　主要的工作是开发了两个软件编译器：VL2BLIF编译器和BLIF2FSM编译器。VL2BLIF编译器的核心功能是把Verilog程序编译为BLIF-MV程序。BLIF2FSM编译器的核心功能是从BLIF-MV程序中提取出有限状态机，并使用二叉判定图表示有限状态机。主要工作内容为：
　　1.编写lex与yacc源程序，使编译器能够自动地分析Verilog程序与BLIF-MV程序的词法、语法、语义。生成编译器可处理的中间数据结构，并自动检查Verilog程序与BLIF-MV程序的静态语义错误。
　　2．详细研究 Verilog程序中的各种语句如何描述数字电路的状态转换关系。并研究在BLIF-MV程序中如何使用时间机和非时间机来描述状态转换关系和更新状态变量。重点分析含有延迟与事件控制的过程赋值语句如何转变为时间机。
　　3．研究如何使用布尔函数来描述 BLIF-MV语言的状态转换关系和多值变量的关系。
　　4．研究二叉判定图表示布尔函数的方法。并分析二叉判定图减小存储空间的方法。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 引言

1.1 研究模型检验的重要意义

1.2主要工作

第二章 模型检验器的前端系统

2.1 前端系统框架

2.2 VL2BLIF编译器

2.3 BLIF2FSM编译器

第三章 词法、语法、语义分析与生成中间结构

3.1 lex与yacc语言的概述

3.2 生成中间结构的基本方法

3.3 Verilog文件转换为中间数据结构

3.4 BLIF-MV文件转换为中间数据结构

第四章 Verilog编译为BLIF-MV

4.1 常量变量的编译方法

4.2 持续赋值编译为逻辑门

4.3 模块实例化编译为subckt语句

4.4 门实例化编译为subckt语句

4.5 always语句编译为时间机与非时间机

4.6 例子

4.7 分析与小结

第五章 从BLIF-MV提取Kripke结构

5.1 二叉判定图

5.2 Kripke结构

5.3 从BLIF-MV提取Kripke结构

5.4 例子

5.5 实验结果

第六章 结论

附 录

致谢

参考文献

攻硕期间取得的研究成果