第1章 緒論
1．1 背景知識(shí)
1．1．1 基本記法
1．1．2 基于命題邏輯的可滿足性問題
1．1．3 有限狀態(tài)機(jī)
1．1．4 基于遷移關(guān)系（函數(shù)）展開的形式化驗(yàn)證算法的一般性原理
1．2 對(duì)偶綜合研究現(xiàn)狀
1．2．1 早期的充分非完備算法
1．2．2 完備停機(jī)算法
1．2．3 在對(duì)偶綜合領(lǐng)域的其他相關(guān)工作
1．3 基于白盒模型的對(duì)偶綜合
1．3．1 研究意義
1．3．2 面臨的挑戰(zhàn)
1．4 研究?jī)?nèi)容與創(chuàng)新點(diǎn)
1．5 本書組織結(jié)構(gòu)

第2章 對(duì)偶綜合相關(guān)研究概述
2．1 對(duì)偶綜合
2．2 程序求反
2．3 超屬性模型檢驗(yàn)
2．4 協(xié)議轉(zhuǎn)換
2．5 可滿足賦值遍歷和量詞削減
2．6 基于Craig插值的邏輯綜合算法
2．7 本章小結(jié)

第3章 基于余子式和Craig插值的迭代特征化算法
3．1 引言
3．2 Craig插值的原理和實(shí)現(xiàn)
3．2．1 相關(guān)背景知識(shí)和記法
3．2．2 不可滿足證明
3．2．3 Craig插值算法
3．3 非迭代的特征化算法
3．4 迭代的特征化算法
3．5 可選的BDD整理和化簡(jiǎn)
3．6 本章小結(jié)

第4章 面向流控制的對(duì)偶綜合
4．1 引言
……
第5章 面向流水線的對(duì)偶綜合
第6章 面向流控制和流水線的對(duì)偶綜合
第7章 原型系統(tǒng)的實(shí)現(xiàn)
第8章 結(jié)束語
附錄1 詞法分析程序代碼
附錄2 語法分析程序代碼
參考文獻(xiàn)
后記