自動機理論在驗證PSL中的應(yīng)用.pdf

1、隨著信息技術(shù)的發(fā)展，集成電路的規(guī)模和復(fù)雜度不斷擴大，驗證在這個項目的開發(fā)周期越來越長，而且集成電路市場競爭也越來越激烈。保證設(shè)計功能的正確性并盡量縮短產(chǎn)品投入市場的時間成為產(chǎn)品成功的關(guān)鍵，這也對驗證技術(shù)和方法提出了越來越高的要求。要保證功能正確性，就要保證設(shè)計在實現(xiàn)時符合設(shè)計規(guī)范。因此，作為設(shè)計規(guī)范的描述語言必須有強大的表達能力，能夠精確描述設(shè)計要求，同時還要易于使用。PSL就是符合這種要求的語言之一。 PSL可以描述斷言，并且

2、可以嵌入到設(shè)計之中，為驗證提供便利，能有效地縮短了驗證時間。PSL還有一個更吸引人的地方：它既可以用于動態(tài)驗證的輸入，也可以作為形式驗證工具的屬性刻畫語言。憑借著這些優(yōu)點，PSL已經(jīng)成為工業(yè)界屬性刻畫語言的標(biāo)準(zhǔn)。 本文研究了如何使用自動機理論實現(xiàn)PSL的動態(tài)驗證與模型檢驗。在動態(tài)驗證PSL的討論中，本文介紹了序列自動機以及如何將PSL轉(zhuǎn)化為序列自動機。在模型檢驗PSL的研究中，本文提出了一個為PSL構(gòu)造Biichi自動機的方法，