基于約束的FPGA詳細布線.pdf

1、現(xiàn)場可編程邏輯門陣列(FPGA，F(xiàn)ield Programmable Gate Array)，是一個含有可編輯元件的半導體設(shè)備，可供使用者現(xiàn)場程式化邏輯門陣列元件。目前以硬件描述語言(Verilog或VHDL)所完成的電路設(shè)計，可以經(jīng)過綜合與布局布線，快速燒錄至FPGA上進行測試。
　　 本文主要研究基于約束的FPGA詳細布線問題，即通過將詳細布線問題轉(zhuǎn)化為約束表達式并求解以得到可行的詳細布線結(jié)果。本文中將分別使用SAT，SMT

2、，CSP三種技術(shù)作為求解引擎來解決這個問題。
　　 SAT(Boolean satisfiability problem)求解器用來解決對于給定的布爾方程式，是否存在一組變量賦值，使間題可滿足。因此，結(jié)合所要實現(xiàn)的口標，需要設(shè)計實現(xiàn)一個分析轉(zhuǎn)換程序，將詳細布線問題轉(zhuǎn)換為一組可滿足性問題的布爾方程式，從而可利用SAT問題求解器進行求解。在轉(zhuǎn)換過程中，尤其需要注意的是原問題與目標問題的等價，即轉(zhuǎn)換后的布爾方程能精確描述布線過程中的各

3、類約束，從而得到可用的詳細布線結(jié)果。
　　 SMT(Satisfiability Modulo Theories)工具與SAT工具一樣都是用來解決命題邏輯可滿足性問題。但不同的是，SAT僅僅能解決命題邏輯可滿足問題，而SMT可以解決更為廣泛的邏輯判定問題，這些問題可以包含整數(shù)變量，實數(shù)變量等。CSP(constraint satisfaction problem)在指定域中求出滿足所有給定約束的子集，這些結(jié)果集滿足所有的約束。本