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

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

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