高阶逻辑与硬件验证(2) Refinement风格的硬件验证简述

Pre

这里的笔记内容主要是在一个非常高层面介绍使用Refinement风格的硬件验证（hhhhh这个其实和我的研究方向没啥关系2333）。使用之前提到过的Higher Order logic.

在硬件开发的过程中为了保证硬件的安全性和逻辑功能的正确性，通常我们需要进行硬件验证。而其中一种方式就是使用交互式定理证明工具(Interactive Theorem Prover)来从数学上证明硬件设计的数学模型(model)能够正确的反映硬件的特性(specification)。常见的定理证明器有HOL家族的定理证明器(HOL4,HOL Light, Isabella/HOL)， Coq， ACL2, PVS, Agda 等等。不同的定理证明器有不一样的逻辑系统, 好像在公司在硬件验证的话用的比较多的还是HOL系的Theorem Prover,，在结下来的介绍也主要基于HOL.

总体来说这种风格硬件验证有以下的步骤：

把硬件的行为和功能用形式化的Specification S表达出来
把组成硬件的基本的也形式化的写出来，这一步一定需要表达出每一个电路原件真实确切的行为。
定义一个表达式D来反映硬件各个组件之间的组合关系，一般有如下的形式：
$D~~\stackrel{def}{=} P_1+...+P_n$
其中+是组合操作符， P是之前步骤2中定义的组件。
证明如下定理
$\vdash D~ satisfies ~ S$

1 Specifying Hardware Behaviour

直接方式

一种比较直接的表达硬件行为的方式是使用带有自由变量的布尔Term,比如对于如下的电路元件：

Dev的行为（behaviour）就可以用布尔表达式来表达，如果这个表达式的值为T那么a,b,c,d四个信号在四个引脚上会同时出现。但是我们看到如果我们使用这种值关注引脚的方式有，我们对硬件的内部其实是一无所知的。在HOL中，我们可以把这个表达进行宾语缩写，定义一个常量Dev来表示：

$\vdash Dev(a,b,c,d)=S[a,b,c,d]$
也可以用类似偏函数的形式来表达,把Dev进行科里化,把Dev变成一个高阶函数。

$\vdash Dev ~a~b~c~d=S[a,b,c,d]$

组合逻辑

数电里我们很多时候都会使用组合逻辑关系，在验证中当然也要用上。来看一个最基本的异或门(xor)吧

xor

$\vdash Xor(i_1,i_2,o)=(o=\neg(i_1=i_2))$
不过通过观察我们不难发现, 其实输出o这个变量是多余的，因为这里的输出其实是为了表达两个输入之间的关系所以可以简化下
$\vdash Xor(i_1,i_2) =\neg(i_1=i_2)$
这种基于关系式的定义在表达比如管子的时候会非常好用，比如对于N-trans

N-type transistor

$\vdash Ntrans(g,s,d)=(g \supset (d=s))$
这种逻辑的表达当然是不能表达管子的所有特性的比如导通的延迟，甚至不能完全反映管子的工作情况，电压，完整的各级关系但是他能比较好的反映管子的逻辑特性（尤其是很多时候，我们需要的部分的逻辑）。关于这方面的研究具体的可以看Mike Gordon 对与MOS管逻辑表示的研究。

时序逻辑

器件的时序特性也是一个重要的部分，不如对于锁存器之类的东西

d flip图画的比较搓，还错了2333凑或看，懂意思就行了

$\vdash Rise ~ck ~t = \neg ck(t) \land ck(t+1) \\ \vdash Dtype(ck ,d,q) =\forall t.q(t+1)=(Rise ~ck ~t \implies d ~t ~|~q~t)$

这个例子就很好的体现了高阶逻辑对于一阶逻辑在表达能力上具有的优势利用高阶函数和推出之类的常量我们的逻辑表达式可以非常的自然。

2 一些简化和结构化的方法

Partial

其实在实际使用中，如果我们完整描述一个器件的所有引脚很多时候是不必要的，我们只需要使用Partial Spec就可以了。这是说我们可以省略掉和我们需要验证的东西不相关的硬件特性，这样可以让我们的模型更加的简单，证明也会更加的清晰。

Composition

硬件往往都是结构化的，一个比较大的硬件往往是由很多小的部分组成的，这时候我们可以灵活运用HOL方便的组合能力来让我们的证明变得更加可行，有实际价值。
比如：
我们已经定义了两个元件 $D_1$ 和 $D_2$ ,他们的接线图如下：

就可以表达为

Hiding

在上面的例子中我们可以看到变量x只有在Model内部中被使用了，我们很多时候需要把这个变量隐藏起来，一个比较简单的做法是使用存在量词去catch这个变量,上边的例子在Hide 之后可以写为:
$\exists x. S_1[a,x] \land S_2[x,b]$

3.correctness proof

接下来我们将以一个最简单的逻辑器件反向器为例子来简单说明以下证明硬件正确性的流程。实际的使用中当然不需要从MOS出发去证明一个实际的器件，这完全取决于问题到底是什么。先看下反向器的CMOS电路图和逻辑符号

逻辑符号

cmos实现

（累死我了。。。。。我要去acm dl把这本书的pdf下来。。。。画图太傻逼了）

1）写出required behaviour的specification
$\vdash Not(i,o) = (o=\neg i)$

2)写出组成反向器的器件的specification(电源，地，N/P MOS)

$\vdash Gnd ~g = (g = F) \quad \quad \vdash Pwr ~p = (p = T)$
$\vdash Ntran(g,s,d) =(g \supset (d=s))$
$\vdash Ptran(g,s,d) =(\neg g \supset (d=s))$

3)写出反向器CMOS实现的具体Model
$\vdash Inv(i,o) = \exists g ~p.Pwr ~p \land Gnd ~g \land Ntran(i,g,o) \land Ptran(i,p,o)$

证明正确性
这里就手写一个简单的证明过程吧，放到HOL4里还是要定义一堆的Type啥的还是挺麻烦的，这里用了一个前向证明，等我回头有空了再做吧。。。。

Theorem
$\quad \vdash \forall i ~o ~ Inv(i,o) = Not(i,o)$
Proof

展开Gnd, Pwd,Ntran,Ptran的定义，可得 Inv变为
$\vdash Inv(i,o) = \exists g ~p.(p = T)\land (g = F) \land (i \supset (o=g)) \land (\neg i \supset (o=p))$
通过meta-theorem $\vdash (\exists v.(v=E) \land P) = P[E/v]$ 上面的式子等价与
$\vdash Inv(i,o) = (i \supset (o = F)) \land (\neg i \supset (o=p))$
使用排中律(是的，在HOL里有这个)
$\vdash Inv(i,o) = (i \supset \neg o) \land (\neg i \supset o)$
使用 $\neg$ 的定义
$\vdash Inv(i,o) = (o \supset \neg i) \land (\neg i \supset o)$
根据布尔想等性，等价于
$\vdash Inv(i,o) = (o = \neg i)$
根据Not的定义，再genl一下,不难得到
$\vdash \forall i ~o.Inv(i,o)= Not(i,o)$

$\square$

HOL 实现

下面给出在HOL4中的实现，在HOL4中写出定义非常直接，基本上和我们上面的完全一致，在证明的过程中不难发现，这个纯组合逻辑的东西其实过于简单打开定义之后是一个纯的一阶逻辑的东西， HOL4内置的SAT Solver可以非常快速的解决, HOL 的自动化策略非常非常的丰富但是也非常的复杂，这也是这类Theorem Prover强大于Coq/Agda之类的地方，这里我选择最简单的一种，化简布尔表达式后使用meson search (prove_tac)来解决，也可以直接调用强大的metis来解决。


(******************************************************************************)
(*  This file is to show how hardware verification works in HOL4 k13          *)
(*  Author: Yihao Sun                                                         *)
(*  2019  in Syracuse                                                         *)
(*  <ysun67@syr.edu>                                                          *)
(******************************************************************************)

structure HardwareScript = struct

open HolKernel Parse boolLib bossLib;
open TypeBase boolSimps;

val _ = new_theory "Hardware";

(* -------------------------------------------------------------------------- *)
(*  Definition of reverse gate                                                *)
(* -------------------------------------------------------------------------- *)
val not_gate_def = Define `
  not_gate (input:bool) (output:bool) ⇔ (output = (¬ input))`;

(* -------------------------------------------------------------------------- *)
(* Definition of power(vcc) and ground(vss) node                              *)
(* -------------------------------------------------------------------------- *)
val gnd_def = Define `gnd (g:bool) ⇔ g = F`;

val pwr_def = Define `pwr (p:bool) ⇔ p = T`;

(* -------------------------------------------------------------------------- *)
(*  Definition of n-type&p-type transistor                                    *)
(* -------------------------------------------------------------------------- *)
val ntrans_def = Define `
  ntrans (g:bool) (s:bool) (d:bool) = (g ⇒ (d = s))`;

val ptrans_def = Define `
  ptrans (g:bool) (s:bool) (d:bool) = (¬g ⇒ (d = s))`;

(* -------------------------------------------------------------------------- *)
(* This is the transsitor level model of a CMOS inverter, which is just a not *)
(* gate in RTL level                                                          *)
(* -------------------------------------------------------------------------- *)
val inv_def = Define `
  inv (input:bool) (output:bool) ⇔
  ∃ (g:bool) (p:bool).
  pwr p∧ gnd g ∧
  ntrans input g output ∧
  ptrans input p output`;

(* ========================================================================== *)
(* proof of model is the same of specification (using automation of HOL)      *)
(* ========================================================================== *)
Theorem inv_correctness:
  ∀ input output. inv input output ⇔ not_gate input output
Proof
  rewrite_tac [not_gate_def, inv_def, ntrans_def,
               ptrans_def, pwr_def, gnd_def] \\
  simp_tac (bool_ss) [] \\
  prove_tac []
QED;

val _ = export_theory();

end (* strcuture *)