模型检验器前端系统的设计与实现
| 摘要 | 第1-5页 |
| Abstract | 第5-8页 |
| 第一章 引言 | 第8-11页 |
| ·研究模型检验的重要意义 | 第8-9页 |
| ·验证工作在电路设计中的重要意义 | 第8页 |
| ·传统验证方法的不足之处 | 第8-9页 |
| ·模型检验方法的重要意义与国内外研究现状 | 第9页 |
| ·主要工作 | 第9-11页 |
| 第二章 模型检验器的前端系统 | 第11-14页 |
| ·前端系统框架 | 第11-12页 |
| ·VL2BLIF 编译器 | 第12-13页 |
| ·BLIF2FSM 编译器 | 第13-14页 |
| 第三章 词法、语法、语义分析与生成中间结构 | 第14-25页 |
| ·lex 与yacc 语言的概述 | 第14-16页 |
| ·词法分析程序lex | 第14-15页 |
| ·语法分析程序yacc | 第15-16页 |
| ·生成中间结构的基本方法 | 第16-19页 |
| ·lex 与yacc 程序转化为C 程序 | 第16页 |
| ·生成中间结构的方法 | 第16-17页 |
| ·语义分析 | 第17-19页 |
| ·Verilog 文件转换为中间数据结构 | 第19-22页 |
| ·Verilog 词法分析 | 第19页 |
| ·Verilog 语法分析 | 第19-21页 |
| ·生成中间结构 | 第21-22页 |
| ·BLIF-MV 文件转换为中间数据结构 | 第22-25页 |
| ·BLIF-MV 词法分析 | 第22页 |
| ·BLIF-MV 语法分析 | 第22-23页 |
| ·生成中间结构 | 第23-25页 |
| 第四章 Verilog 编译为BLIF-MV | 第25-63页 |
| ·常量变量的编译方法 | 第25-29页 |
| ·常量编译方法 | 第25-27页 |
| ·变量声明与使用的编译方法 | 第27-29页 |
| ·持续赋值编译为逻辑门 | 第29页 |
| ·模块实例化编译为subckt 语句 | 第29-31页 |
| ·门实例化编译为subckt 语句 | 第31-32页 |
| ·always 语句编译为时间机与非时间机 | 第32-57页 |
| ·隐含时钟与明显时钟 | 第33-34页 |
| ·Verilog 模拟器 | 第34-37页 |
| ·时间机的提取 | 第37-44页 |
| ·非时间机的提取 | 第44-51页 |
| ·判断器 | 第51-57页 |
| ·例子 | 第57-61页 |
| ·分析与小结 | 第61-63页 |
| 第五章 从BLIF-MV 提取Kripke 结构 | 第63-71页 |
| ·二叉判定图 | 第63-65页 |
| ·Kripke 结构 | 第65-66页 |
| ·状态的布尔表示 | 第65页 |
| ·状态转换关系的布尔表示 | 第65-66页 |
| ·从BLIF-MV 提取Kripke 结构 | 第66-68页 |
| ·编译逻辑门 | 第66-68页 |
| ·编译模块实例化 | 第68页 |
| ·编译锁存器 | 第68页 |
| ·例子 | 第68-69页 |
| ·实验结果 | 第69-71页 |
| 第六章 结论 | 第71-72页 |
| 附录 | 第72-75页 |
| 致谢 | 第75-76页 |
| 参考文献 | 第76-79页 |
| 攻硕期间取得的研究成果 | 第79-80页 |
