張鵬飛，葉永升

（1.淮北師范大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，安徽 淮北 235000；2.淮北師范大學(xué) 數(shù)學(xué)科學(xué)學(xué)院，安徽 淮北 235000）

數(shù)字系統(tǒng)投影時序邏輯描述及驗證

張鵬飛1，葉永升2

（1.淮北師范大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，安徽 淮北 235000；2.淮北師范大學(xué) 數(shù)學(xué)科學(xué)學(xué)院，安徽 淮北 235000）

投影時序邏輯是一種具有離散時間模型的時序邏輯，其部分子集又是一種程序設(shè)計語言，可處理順序和并發(fā)計算.文章討論應(yīng)用投影時序邏輯對數(shù)字系統(tǒng)進(jìn)行形式描述和驗證的方法，該方法可在數(shù)字系統(tǒng)的不同層級設(shè)計過程中，使用投影時序邏輯對其系統(tǒng)行為和性質(zhì)進(jìn)行形式化的描述及驗證，從而提高系統(tǒng)設(shè)計的可信性.

投影時序邏輯；形式化描述；系統(tǒng)驗證

電器設(shè)備的數(shù)字化以不可阻擋的趨勢成為當(dāng)今電器設(shè)計的主題，從小到大的電器設(shè)備被加上或?qū)⒈患由蠑?shù)字之芯.在數(shù)字系統(tǒng)設(shè)計中，在經(jīng)過一系列步驟后，才能把設(shè)計思想轉(zhuǎn)化為具體的產(chǎn)品.隨著系統(tǒng)復(fù)雜性的提高，如何對系統(tǒng)進(jìn)行描述以避免產(chǎn)生歧義，如何對系統(tǒng)進(jìn)行驗證以保證系統(tǒng)的活性和安全性也是數(shù)字系統(tǒng)設(shè)計中的重要問題.現(xiàn)階段數(shù)字系統(tǒng)設(shè)計的各階段所用的描述語言不僅不同，而且缺乏精確的數(shù)學(xué)語義，不能保證各級描述的一致性.在驗證方面，傳統(tǒng)的驗證方法由于不能提供系統(tǒng)的完整覆蓋，所以不能在未發(fā)現(xiàn)錯誤時確認(rèn)系統(tǒng)無錯誤.形式化方法起源于20世紀(jì)60年代的軟件危機(jī)，是一種基于數(shù)學(xué)的描述和驗證方法，用以提高設(shè)計的正確性和可靠性.在保證軟件和硬件設(shè)計正確性方面，形式化方法的使用和研究取得了很多成果.

投影時序邏輯（Projection Temporal Logic）是一種離散區(qū)間或時段的時態(tài)邏輯，具有在統(tǒng)一數(shù)學(xué)框架下對實(shí)時、并發(fā)系統(tǒng)進(jìn)行形式描述和驗證的能力.投影時序邏輯的優(yōu)點(diǎn)在于它的表達(dá)能力強(qiáng)，既能刻畫系統(tǒng)的性質(zhì)又能表示系統(tǒng)的實(shí)現(xiàn)，系統(tǒng)的驗證可在統(tǒng)一的數(shù)學(xué)模型框架下進(jìn)行.除定理證明和模型檢測之外，PTL具有可執(zhí)行子集MSVL語言，可通過編寫并執(zhí)行規(guī)范程序的方式來達(dá)到驗證的目的.所以應(yīng)用投影時序邏輯對數(shù)字系統(tǒng)進(jìn)行形式化描述，可為數(shù)字系統(tǒng)設(shè)計及其驗證提供一系列的支持，提高數(shù)字系統(tǒng)設(shè)計正確性.

1 投影時序邏輯

1.1 語法

設(shè)∏是命題的可數(shù)集合，V是有類型定義的靜態(tài)變量和動態(tài)變量的可數(shù)集合（在區(qū)間內(nèi)其值保持不變的稱靜態(tài)變量，否則為動態(tài)變量）.項（terms）和公式（formulas）由下列語法給出.

其中x是一個動態(tài)變量，u是一個靜態(tài)變量.在f（e1，…，em）和P（e1，…，en）中，f是一個函數(shù)而P是一個謂詞，假定項的類型和f及P中的類型相兼容.公式（項）被稱為是狀態(tài)公式（項）如果它不含任何時序操作符；否則是一個時序公式（項）.

1.2 語義

2 數(shù)字系統(tǒng)的投影時序邏輯描述

隨著數(shù)字系統(tǒng)的日益復(fù)雜，在系統(tǒng)開發(fā)的各個階段寫出清晰、完整和一致的系統(tǒng)規(guī)范是件十分重要的事情.數(shù)字系統(tǒng)設(shè)計各階段的規(guī)范工具既不統(tǒng)一又缺少精確的數(shù)學(xué)語義，而模擬形式的驗證也不能保證設(shè)計的正確性.投影時序邏輯既可作為有精確語義的形式化的規(guī)范工具，又可以用來描述系統(tǒng)的某些重要性質(zhì)（如安全性和活性），這樣為在統(tǒng)一數(shù)學(xué)框架內(nèi)對系統(tǒng)性質(zhì)進(jìn)行形式驗證提供了方便.

2.1 硬件的行為語義

1）時態(tài)賦值

延時是電路中的常見現(xiàn)象.設(shè)A是一個輸入信號，B是一個與A對應(yīng)的輸出信號.在每個長度為1個單位的子區(qū)間，輸出信號B在區(qū)間結(jié)束時的值等于輸入信號A在區(qū)間開始時的值，這稱為單位延時.在投影時序邏輯中對延時進(jìn)行定義后就可以用來驗證系統(tǒng)的一些時間性約束性質(zhì).

表示如果某個區(qū)間（時間段）內(nèi)表達(dá)式A的初始值等于表達(dá)式B的終值，此處a為一個靜態(tài)變量.單位時態(tài)賦值，表示電路從一個狀態(tài)變化到另一個狀態(tài)的區(qū)間長度是1，變化后x的值為e.

2）時態(tài)相等

如果當(dāng)兩個表達(dá)式在一個區(qū)間內(nèi)永遠(yuǎn)相等時，稱這兩個表達(dá)式是在該區(qū)間時態(tài)相等的.

3）信號的穩(wěn)定性

如果一個信號的值在所考慮的時間段內(nèi)固定不變，則稱該信號是穩(wěn)定的.信號的穩(wěn)定性可用stb操作符表示.

2.2 組合邏輯電路描述

最基本的組合邏輯電路如與門、或門、非門、三態(tài)門，如果不考慮時延，對這種電路用投影時序邏輯公式可描述為：

三輸入與門可用兩個兩輸入與門適當(dāng)連接而成，對其公式的描述可用兩個與門的投影時序邏輯公式相與而得到.

可以證明這兩種公式是等價的.這說明使用投影時序邏輯對電路進(jìn)行建模具有抽象性，設(shè)備無關(guān)性，適合電路的高層設(shè)計.

圖1 多路選擇器的框圖及邏輯功能

使用投影時序邏輯可對組合邏輯電路進(jìn)行描述.圖1是一個2-to-1多路選擇器，從邏輯功能上，該電路可用下式描述（I0表示信號Input0，I1表示信號Input1）：

如果考慮電路的時間延遲（設(shè)延遲時間為n個時間單位），則其行為可用下式描述：

pMUX（E，S，I0，I1，Output，n）=def（if（E=0）then Z）else（if S=0 then I0）else I1））delnOutput.

2.3 基本時序元件

基本時序元件是鎖存器、觸發(fā)器，其中D觸發(fā)器（鎖存器）最為常用.下面通過實(shí)例說明投影時序邏輯對基本時序元件建模的方法.

如圖2a是一個正向邊沿觸發(fā)的D觸發(fā)器功能表.當(dāng)LD=0時，不論輸入端是什么信號，D觸發(fā)器狀態(tài)保持不變，而當(dāng)LD=1且時鐘信號從0到1變化，則D觸發(fā)器的狀態(tài)變?yōu)镈的輸入信號.當(dāng)LD=1但時鐘信號不是從0到1變化，則D觸發(fā)器的狀態(tài)也不變.

圖2 D觸發(fā)器（鎖存器）

圖3 D觸發(fā)器組成的4位計數(shù)器

2.4 寄存器傳送語言（RTL）

RTL用于描述微操作執(zhí)行數(shù)據(jù)傳送的條件和過程.RTL獨(dú)立于實(shí)現(xiàn)系統(tǒng)的元件，同一RTL代碼可以用不同的電路實(shí)現(xiàn).但RTL又是最接近實(shí)際電路設(shè)計的一種抽象描述，使用RTL對系統(tǒng)行為進(jìn)行描述后，就可以用硬件來匹配這些規(guī)范，從而得到具體的數(shù)字電路.RTL是對更高層系統(tǒng)描述—狀態(tài)圖進(jìn)行分析處理而得到的，所以又可以認(rèn)為是狀態(tài)圖這一系統(tǒng)規(guī)范的實(shí)現(xiàn).在所有RTL代碼中，時鐘信號是隱含的.RTL的符號形式：

其中X←Y表示數(shù)據(jù)從寄存器Y流入X，α表示發(fā)生這一傳送的條件.

把RTL代碼轉(zhuǎn)化為投影時序邏輯公式是一件有意義的事，它可以用形式化方法檢查所描述的系統(tǒng)是否能完成相應(yīng)的功能，條件是否互斥，對寄存器的操作是否相矛盾等（例如不能對其同時進(jìn)行清零和置數(shù)的操作）.下面以一個模6計數(shù)器為例，說明如何使用投影時序邏輯對RTL代碼進(jìn)行描述.

模6計數(shù)器按000→001→010→011→100→101→000的規(guī)律計數(shù).當(dāng)輸入信號U=0時，寄存器中值不變，當(dāng)U=1時，在時鐘脈沖上升沿到來后，寄存器中值加1.當(dāng)計數(shù)器從5變到0時產(chǎn)生進(jìn)位（C=1），圖4是模6計數(shù)器的狀態(tài)圖表示.該計數(shù)器有8個狀態(tài)（S0，S1，S2，S3，S4，S5，S6，S7），其中S6，S7用于解決電源開啟時處于無效狀態(tài)的情形

圖4 模6計數(shù)器的狀態(tài)圖

圖5 模6計數(shù)器的RTL代碼

2.5 狀態(tài)圖

3 對數(shù)字系統(tǒng)的形式驗證

在數(shù)字系統(tǒng)設(shè)計過程中，往往采用自頂向下的設(shè)計方法，首先給出系統(tǒng)的文字描述，然后使用諸如狀態(tài)圖之類的工具對系統(tǒng)建模，以描述系統(tǒng)的行為.再根據(jù)這個系統(tǒng)模型細(xì)化，使用寄存器傳送語言或硬件描述語言對系統(tǒng)進(jìn)行高層（或低層）設(shè)計，最后使用常用的集成邏輯部件來搭建實(shí)際電路.在每一級設(shè)計中的錯誤都會導(dǎo)致失敗.投影時序邏輯在數(shù)字系統(tǒng)設(shè)計中除可以對系統(tǒng)的各級設(shè)計用統(tǒng)一的語言進(jìn)行建模外，還可描述系統(tǒng)應(yīng)滿足的活性、安全性及時間約束等性質(zhì)，這為使用模型檢測技術(shù)或定理證明技術(shù)對系統(tǒng)級設(shè)計進(jìn)行活性及安全性驗證提供了方便.

psc是模6計數(shù)器的狀態(tài)圖描述公式，pRTL是模6計數(shù)器RTL描述公式，如果這個描述正確反映系統(tǒng)的頂層設(shè)計（狀態(tài)圖），則一定有|=pRTL→psc.pAND3（x，y，z，A）是三輸入與門的行為描述公式，p′AND3（x，y，z，A）是用2個與門連接成的電路的公式，如果這個電路能正確實(shí)現(xiàn)三輸入與門的功能，則在邏輯上可以推導(dǎo)出：

設(shè)pM是某數(shù)字系統(tǒng)模型的投影時序邏輯描述公式，pI是由該模型經(jīng)細(xì)化后得到的更接近電路實(shí)現(xiàn)的模型描述公式，我們稱前者是系統(tǒng)的規(guī)范，后者是系統(tǒng)的實(shí)現(xiàn).如|=pI→pM成立，則稱系統(tǒng)的實(shí)現(xiàn)pI滿足系統(tǒng)的規(guī)范pM.

在投影時序邏輯中，通過驗證系統(tǒng)級規(guī)范與RTL級實(shí)現(xiàn)間的滿足關(guān)系、RTL規(guī)范與寄存器電路級間實(shí)現(xiàn)的滿足關(guān)系可以形式地證明實(shí)際的電路和系統(tǒng)模型間的一致.

數(shù)字系統(tǒng)設(shè)計驗證中的另一個問題是系統(tǒng)的活性、安全性及時間性約束問題.我們把系統(tǒng)應(yīng)該具有的某些特征或約束稱為系統(tǒng)的性質(zhì).投影時序邏輯可以很好地對這些性質(zhì)進(jìn)行描述.例如模6計數(shù)器在啟動后，應(yīng)滿足在任何時候都不應(yīng)有V>5的情況.這一系統(tǒng)的安全性問題用投影時序邏輯可表示為（V<6）.所設(shè)計的系統(tǒng)（psc）是否具有這一性質(zhì)，轉(zhuǎn)化為驗證|=psc→（V<6）是否成立的問題.如果|=pRTL→psc且|=psc→（V<6），則一定有|=pRTL→（V<6）.所以有以下定理.

投影時序邏輯具有嚴(yán)格的語法和語義，其命題投影時序邏輯（PPTL）的判定性、表達(dá)性和復(fù)雜性問題已經(jīng)得到解決，建立有PTL和PPTL的模型理論和公理系統(tǒng).MSVL是以投影時序邏輯的可執(zhí)行子集Tem?pura語言為基礎(chǔ)，建模、仿真、驗證為一體的形式化工具，和常見的程序設(shè)計語言不同，MSVL程序的執(zhí)行實(shí)質(zhì)是一個邏輯推理的過程.使用投影時序邏輯的模型檢查技術(shù)或公理證明系統(tǒng)可以驗證上面所討論的公式滿足關(guān)系.在開發(fā)的不同階段用于描述數(shù)字系統(tǒng)的狀態(tài)圖、RTL、電路等經(jīng)投影時序邏輯公式描述后，可以轉(zhuǎn)化成MSVL程序以進(jìn)行模擬驗證.

4 結(jié)論

本文討論了使用投影時序邏輯及MSVL語言對數(shù)字系統(tǒng)進(jìn)行形式描述和驗證的方法.把投影時序邏輯引入數(shù)字系統(tǒng)設(shè)計過程，通過對系統(tǒng)級和實(shí)現(xiàn)級的數(shù)字系統(tǒng)進(jìn)行形式描述，可以使系統(tǒng)的設(shè)計更加清楚明確，如果系統(tǒng)的一些性質(zhì)也用PTL公式來表示，就可在同一邏輯框架下對系統(tǒng)應(yīng)滿足的性質(zhì)進(jìn)行證明，同時可把系統(tǒng)形式描述轉(zhuǎn)換為MSVL程序進(jìn)行模擬.

［1］JURGEN R，ROLAND J，WEISS T K，et al.Modeling and formal verification of production automation systems［C］// INT2004，LNCS3174，Springer Verlag，2004：541-566.

［2］王永祥，吳盡昭，蔣建民.進(jìn)程代數(shù)——對稱與動作細(xì)化［M］.北京：科學(xué)出版社，2007.

［3］林惠民，張文輝.模型檢測：理論、方法與應(yīng)用［J］.電子學(xué)報，2002，30（12A）:1907-1912.

［4］DUAN Z，KOUTNY M，HOLT C.Projection in temporal logic programming［C］//Proc 5th International Conference on Logic Programming and Automated Reasoning，Lecture Notes in Computer Science 822，Springer，1994：333-344.

［5］王小兵.面向?qū)ο驧SVL語言及其在組合Web服務(wù)驗證中的應(yīng)用［D］.西安：西安電子科技大學(xué)計算機(jī)學(xué)院，2009.

［6］CARPINELLI J D.計算機(jī)系統(tǒng)組成與體系結(jié)構(gòu)［M］.李仁發(fā)，彭蔓蔓，譯.北京：人民郵電出版社，2003.

［7］DUAN Zhenhua，TIAN Cong.A unified model checking approach with projection temporal logic［C］//ICFEM2008，LNCS5256，Springer-verlag，2008：167-186.

［8］TIAN Cong，DUAN Zhenhua.Model checking propositional projection temporal logic based on SPIN［C］//ICFEM 2007，LNCS4789，Springer-verlag，2007：246-265.

［9］舒新峰，段振華.有窮時間投影時序邏輯的完備公理系統(tǒng)［J］.軟件學(xué)報，2011，22（3）：366-380.

PTL Specification and Verification of Digital System

ZHANG Peng-fei1，YE Yong-sheng2
（1.School of Computer Science and Technology，Huaibei Normal University，235000，Huaibei，Anhui，China；
2.School of Mathematical Sciences，Huaibei Normal University，235000，Huaibei，Anhui，China）

PTL（Projection Temporal Logic）is a kind of temporal logic which can handle both sequential and parallel computa?tion.A formal approach of specification and verification of digital system using PTL is proposed in this paper.With this ap?proach，PTL and its executable subset（MSVL）are used for formal specification and verification in different level design of a digital system.

projection temporal logic；formal specification and verification；digital system

TP 301

A

2095-0691（2013）04-0061-06

2013-09-18

淮北市科技局基金項目（20120309）

張鵬飛（1968- ），男，安徽利辛人，碩士，研究方向：嵌入式系統(tǒng)形式化描述與驗證.