運用可滿足性求解之歸納式等同驗證與關係確定

Inductive Equivalence Checking and Relation Determinization via SAT Solving

洪偉倫(Wei-Lun Hung)

指導教授 ： 江介宏

國立臺灣大學/電機資訊學院/電子工程學研究所/碩士(2008年)

https://doi.org/10.6342/NTU.2008.01131

摘要

在這篇論文的第一部份，我們著眼於驗證。時序重整與再生轉換是兩種重要的電路最佳化技術，但是由於驗證的困難，使得它們的應用受到了限制。如果能克服這瓶頸，相信他們的應用會更廣泛。我們針對時序重整與再生轉換的電路，研究他們在歸納式等同驗證方法中的完備條件。此外，以往的研究沒有同時考慮時序重整和再生轉換，他們只對其中一項技術的驗證有完備性。我們的方法，能到對一次時序重整，再做再生轉換，最後再做一次時序重整的電路有完備性。實驗結果顯示我們的方法可以應用在較大的電路上，我們也可以驗證之前研究無法解決的一些電路。

第二部份我們研究布林關係確定。很多硬體和軟體的合成問題都可以簡化成條件求解。而可行的解法是將這些條件是用布林關係來表示。但是這些關係並不能直接解決問題。除非關係是被決定而且可以轉換成相對應的函數，否則關係無法用電路來表示。我們運用內插法來求取關係的對應函數，這方法利用關係的彈性並且不需去考慮它的不相關項。

關鍵字

等同驗證 ； 歸納式驗證 ； 時序重整 ； 再生轉換 ； 布林關係 ； 決定 ； 可滿足性問題求解 ； 內插法

並列摘要

The first part of this thesis focuses on verification. Retiming and resynthesis are both important techniques for sequential circuit optimization, but their applicability is limited because the verification is hard. Overcoming the verification bottleneck can enhance the practicality of retiming and resynthesis. We study the completeness condition of the inductive approach for equivalence checking under retiming and resynthesis. Besides, the prior work is only complete for circuits transformed under retiming or resynthesis, but not both. Our approach is complete for circuits transformed up to retiming+resynthesis+retiming. The experimental results show the capability and scalability of our approach. Several previously unverifiable instances can be verified effectively.

The second part of this thesis studies the determinization of Boolean relations. Many problems in hardware and software synthesis can be reduced to constraint solving. The feasible solutions of such constraints are often in the form of Boolean relations. Boolean relations however are not directly useful. Unless a Boolean is determinized and transformed into a set of Boolean functions, it cannot be implemented as a circuit. We derive the functional implementation of a Boolean relation through SAT solving and Craig interpolation. The computation provides a way exploit flexibility without computing don't care and is more scalable compared with prior BDD-based methods.

並列關鍵字

equivalence checking ； inductive verification ； retiming ； resynthesis ； Boolean relation ； determinization ； SAT solving ； Craig interpolation

參考文獻

[AYAP03] K. Albin, J. Yuan, A. Aziz, and C. Pixley. Constraint synthesis for environment modeling in functional verification. Design Automation Conference, pages 296--299, June 2003.

[Cra57] William Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. The Journal of Symbolic Logic, 22(3):250--268, 1957.

[DLL62] Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5 (7):394--397, 1962.

[DM91] G. De Micheli. Synchronous logic synthesis: algorithms for cycle-time minimization. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 10(1):63--73, Jan 1991.

[DP60] Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201--215, 1960.