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

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

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