基于对偶综合的解码器自动生成方法

第1章 绪论
1．1 背景知识
1．1．1 基本记法
1．1．2 基于命题逻辑的可满足性问题
1．1．3 有限状态机
1．1．4 基于迁移关系（函数）展开的形式化验证算法的一般性原理
1．2 对偶综合研究现状
1．2．1 早期的充分非完备算法
1．2．2 完备停机算法
1．2．3 在对偶综合领域的其他相关工作
1．3 基于白盒模型的对偶综合
1．3．1 研究意义
1．3．2 面临的挑战
1．4 研究内容与创新点
1．5 本书组织结构

第2章 对偶综合相关研究概述
2．1 对偶综合
2．2 程序求反
2．3 超属性模型检验
2．4 协议转换
2．5 可满足赋值遍历和量词削减
2．6 基于Craig插值的逻辑综合算法
2．7 本章小结

第3章 基于余子式和Craig插值的迭代特征化算法
3．1 引言
3．2 Craig插值的原理和实现
3．2．1 相关背景知识和记法
3．2．2 不可满足证明
3．2．3 Craig插值算法
3．3 非迭代的特征化算法
3．4 迭代的特征化算法
3．5 可选的BDD整理和化简
3．6 本章小结

第4章 面向流控制的对偶综合
4．1 引言
……
第5章 面向流水线的对偶综合
第6章 面向流控制和流水线的对偶综合
第7章 原型系统的实现
第8章 结束语
附录1 词法分析程序代码
附录2 语法分析程序代码
参考文献
后记