陳波

【摘 要】形式化方法在硬件、軟件的設(shè)計(jì)和驗(yàn)證中的應(yīng)用越來越廣泛，基于不同理論的形式化驗(yàn)證工具應(yīng)運(yùn)而生。本文對(duì)形式化驗(yàn)證工具定理證明系統(tǒng)HOL作了介紹，并結(jié)合例子說明HOL系統(tǒng)在硬件設(shè)計(jì)中的應(yīng)用。

【關(guān)鍵詞】形式化驗(yàn)證方法；HOL邏輯；HOL系統(tǒng)；帶復(fù)位的奇偶校驗(yàn)器

中圖分類號(hào)： TP316；TP309 文獻(xiàn)標(biāo)識(shí)碼： A 文章編號(hào)： 2095-2457（2018）28-0162-002

DOI：10.19694/j.cnki.issn2095-2457.2018.28.074

【Abstract】Formal method has been used in both practical hardware and software design and verification widely， formal verification tools based on different theory emerge as the times require.The paper discusses the higher order logic theory prover HOL and illustrates specification and verification in hardware design.

【Key words】Formal Verification method；HOL logic；HOL system；Parity-reset checking device

0 引言

隨著數(shù)字系統(tǒng)設(shè)計(jì)技術(shù)的發(fā)展，傳統(tǒng)的模擬驗(yàn)證方法已不能滿足需求，形式化驗(yàn)證方法逐漸應(yīng)用到數(shù)字系統(tǒng)的驗(yàn)證中。一般來說，形式化驗(yàn)證方法可分為模型檢測、定理證明和等價(jià)性驗(yàn)證等三類[1]。HOL系統(tǒng)是基于高階邏輯的定理證明器，它即能進(jìn)行軟件驗(yàn)證，又能進(jìn)行硬件的形式化驗(yàn)證，是目前形式化領(lǐng)域的研究的熱點(diǎn)之一[2-3]。本文對(duì)HOL邏輯及HOL驗(yàn)證系統(tǒng)之間的關(guān)系進(jìn)行分析研究，并給出HOL系統(tǒng)在硬件設(shè)計(jì)驗(yàn)證中的一個(gè)應(yīng)用實(shí)例。

1 HOL系統(tǒng)

HOL系統(tǒng)是英國劍橋大學(xué)的M.J.C.Gordon教授在80年代開發(fā)的高階邏輯（HOL）定理證明系統(tǒng)[3]，該系統(tǒng)的基礎(chǔ)是Church的簡單帶類型演算，演算是由Alonzo Church提出的作為數(shù)學(xué)基礎(chǔ)的函數(shù)理論。帶類型 演算是用來表示函數(shù)的另一種方式，是函數(shù)語言的基礎(chǔ)，類型的引入保障了邏輯系統(tǒng)的健康性。HOL系統(tǒng)包含了函數(shù)式語言ML，它既是HOL系統(tǒng)的開發(fā)語言也是它的實(shí)現(xiàn)語言。函數(shù)式語言采用一種基于遞歸表示的函數(shù)定義的計(jì)算模型[4]。

1.1 HOL邏輯

HOL邏輯是對(duì)謂詞演算進(jìn)行了三項(xiàng)擴(kuò)展[5]：

變量可以為函數(shù)和謂詞。

邏輯是有類型的。

沒有公式的單獨(dú)語法類（類為bool的項(xiàng)為公式）。

由于HOL邏輯系統(tǒng)中的最基本的常量T都是用λ表達(dá)式T=（（λx.x）=（λx.x））進(jìn)行定義的，所以λ演算是HOL邏輯的基礎(chǔ)。HOL邏輯是HOL驗(yàn)證系統(tǒng)的邏輯基礎(chǔ)，為了避免不一致性HOL邏輯是有類型的，通常有4種類型：

σ：：=α|c|（σ1，…，σn）op|σ1→σ2，

其中σ表示變量，c表示原子類型，op表示類型操作符。

在HOL邏輯中出現(xiàn)的任何合法的符號(hào)都是項(xiàng)，項(xiàng)也有4種。

M：：=c|v|（MN）|λv.M

其中c表示常量，v表示變量，M和N表示項(xiàng)。

1.2 HOL邏輯在HOL定理證明系統(tǒng)中的表示

HOL定理證明系統(tǒng)的項(xiàng)是用ML的抽象數(shù)據(jù)類型表示的。抽象數(shù)據(jù)類型就是帶有其特有的一組運(yùn)算的數(shù)據(jù)類型。在HOL系統(tǒng)中，項(xiàng)的前后加上引號(hào)，系統(tǒng)在進(jìn)行詞法檢查時(shí)就認(rèn)為是邏輯項(xiàng)。HOL系統(tǒng)的項(xiàng)的類型構(gòu)成了一種叫做type的ML類型。HOL的邏輯類型是目標(biāo)語言的類型，而ML類型是元語言類型。

1.3 HOL定理證明系統(tǒng)的理論

在HOL系統(tǒng)中，一個(gè)理論（theory）包含一組類型、常元、定義、公理和定理等。關(guān)于理論的工具能夠維護(hù)不同的理論之間的關(guān)系，例如增加、結(jié)合、擴(kuò)展和保存理論。每個(gè)理論記錄了某些類型、常數(shù)、公理、定義和定理，同時(shí)具有指向它的上級(jí)理論的指針。所有的理論構(gòu)成了一個(gè)分層的樹形結(jié)構(gòu)。最基本的理論是min，它定義了最基本的類型和常量符號(hào)。在這基礎(chǔ)上，逐步構(gòu)成各種數(shù)據(jù)類型和經(jīng)過證明的定理，并為以后更高層的理論及相關(guān)定理的證明所使用，現(xiàn)在HOL系統(tǒng)的理論庫已經(jīng)非常龐大。

1.4 用HOL定理證明系統(tǒng)證明定理

要證明一個(gè)定理，實(shí)際上就是要找出一個(gè)公理或定理序列，由序列中前面的元素（公理或已經(jīng)證明的定理）利用推理規(guī)則可以得到其后面的元素，最后得到的就是要證明的定理。文獻(xiàn)[3]中給出了HOL系統(tǒng)內(nèi)核中五個(gè)公理和八條推理規(guī)則，見表1。

HOL支持兩種證明方式：正向證明方式：指從定理的假設(shè)條件和公理、定理、定義出發(fā)推導(dǎo)出結(jié)論的過程。目標(biāo)制導(dǎo)方式：指從要證明的目標(biāo)出發(fā)，即假定結(jié)論正確，利用已知條件和公理、定理、定義等推出需要證明的子目標(biāo)；如果證明了各個(gè)子目標(biāo)，原來的目標(biāo)也就證明了。在實(shí)際應(yīng)用中經(jīng)常正向證明和目標(biāo)制導(dǎo)方法結(jié)合起來使用。

2 HOL定理證明系統(tǒng)的應(yīng)用

HOL系統(tǒng)現(xiàn)在已經(jīng)應(yīng)用在工業(yè)和學(xué)術(shù)上進(jìn)行形式化推理的很多領(lǐng)域：硬件的設(shè)計(jì)與驗(yàn)證、安全性的推理、實(shí)時(shí)系統(tǒng)的證明、硬件描述語言的語義、編譯器的驗(yàn)證、程序正確性的證明、并發(fā)模型及程序細(xì)化等方面。結(jié)合例子說明。

2.1 驗(yàn)證步驟

在用HOL系統(tǒng)對(duì)系統(tǒng)進(jìn)行驗(yàn)證時(shí)，一般有以下四個(gè)步驟：

建立系統(tǒng)行為的形式化規(guī)范（SPEC）。

建立系統(tǒng)實(shí)現(xiàn)的形式化描述（IMP），包括子模塊的行為規(guī)范及各子模塊間連接的結(jié)構(gòu)描述。

用公式形式描述證明目標(biāo)，或者。

運(yùn)用推理規(guī)則對(duì)目標(biāo)進(jìn)行形式化驗(yàn)證。

在應(yīng)用時(shí)往往要先對(duì)系統(tǒng)用結(jié)構(gòu)抽象、行為抽象、數(shù)據(jù)抽象、時(shí)態(tài)抽象等抽象技術(shù)進(jìn)行處理，去掉不必要的細(xì)節(jié)，建立規(guī)范和實(shí)現(xiàn)的形式化描述。

2.2 實(shí)例

下面通過例子進(jìn)行說明，帶復(fù)位的奇偶校驗(yàn)器的設(shè)計(jì)與驗(yàn)證：主要包括一個(gè)能計(jì)算輸入序列中1的奇偶性的設(shè)備的規(guī)范說明和驗(yàn)證，此設(shè)備包括一個(gè)輸入 in， 一個(gè)復(fù)位reset和一個(gè)輸出鍵out.，從上一次進(jìn)行復(fù)位開始，當(dāng)且僅當(dāng)輸入二進(jìn)制序列中1的個(gè)數(shù)為偶數(shù)個(gè)時(shí)，輸出為真，否則為假。

規(guī)范說明：

val PARITY_RESET_SPEC =

|- （！f reset. PARITY_RESET_SPEC 0 f reset = T） /＼

！n f reset.

PARITY_RESET_SPEC （SUC n） f reset =

（if reset （SUC n） then

T

else

（if f （SUC n） then

～PARITY_RESET_SPEC n f reset

else

PARITY_RESET_SPEC n f reset）） ： thm

根據(jù)說明設(shè)計(jì)出電路并進(jìn)行形式化描述：

val PARITY_RESET_IMP =

|- ！inp reset out.

PARITY_RESET_IMP （inp，reset，out） =

？l1 l2 l3 l4 l5 l6.

NOT （l2，l1） /＼ MUX （inp，l1，l2，l3） /＼ REG （out，l2） /＼ ONE l4 /＼

REG （l4，l5） /＼ MUX （reset，l4，l3，l6） /＼ MUX （l5，l6，l4，out） ： thm

建立目標(biāo)及對(duì)目標(biāo)進(jìn)行推理證明（其中引理UNIQUENESS_LEMMA，PARITY_RESET_LEMMA已得以證明）：

3 結(jié)束語

高階邏輯驗(yàn)證系統(tǒng)HOL在驗(yàn)證過程中用到了各種相關(guān)的技術(shù)，特別是推理技術(shù)和抽象技術(shù)，對(duì)使用者的要求較高。以后的研究將注重HOL系統(tǒng)理論庫的擴(kuò)充以及與其它形式化技術(shù)的結(jié)合，特別是模型檢測技術(shù)，以使其在更多的領(lǐng)域中得到應(yīng)用。

【參考文獻(xiàn)】

[1]Rolf Drechsler.Advanced Formal Verification[M].Dordrecht：Kluwer Academic Publishers，2004.1-20.

[2]韓俊剛，杜慧敏. 數(shù)字硬件的形式化驗(yàn)證[M].北京大學(xué)出版社.2001.12.

[3]M.J.C.Gordon and T.F.Melham.Introduction to HOL：A Theorem Proving Environment for Higher-order Logic[M]. Cambridge University Press，1993.

[4]Lawrence C.Paulson著，柯韋譯.ML程序設(shè)計(jì)教程（第二版）[M].北京：機(jī)械工業(yè)出版社.2005.

[5]The HOL System Logic，2018，https：//hol-theorem-prover.org/.