Chapter 9 Finite Automata

9.1 Finite Automata and Regular Languages

这一小节的内容是有限状态机和正则语言。其实很多讲解编译器的书籍都有相关的论述，而且都比本书更加严谨和通俗易懂。没什么难度，我就不详细讲解了。只是列出几个关键点

NFA与DFA
$\epsilon$ 闭包
string与tape的区别，一个有限，一个无限
正则表达式中的运算如*,|,+..都是作用于sting not tape

9.2 DFA Synthesis

主要有三步

给定一个正则表达式(a*b)*构建一个二叉解析树
深度搜索解析树，后序访问各个节点，按照节点的操作符合并左右孩子的NFA。合并规则很简单，一看就懂。比如已知NFA a和NFA b，如何构造出NFA c = ab.
将NFA转换成DFA，两种-------子集构造法和deterministic image法

9.2.2 The Subset Construction

经典的方法，每本编译器的教材都有相关的内容。基本思路就是从NVA的起始集合 $S_0$ 开始，求出 $S_0$ 的 $\epsilon$ 闭包 $\epsilon(S_0)$ ，作为DFA的起始状态. 依次遍历输入集合，假设访问到输入x，求出 $\epsilon(S_0)$ 中每个状态遇到x后可能到达的状态集合，求这些集合的并集 $S_1$ ，继而求出 $S_1$ 的 $\epsilon$ 闭包 $\epsilon(S_1)$ . 如果 $\epsilon(S_1)$ 之前没有出现过，就把它加入DFA的状态集合，并从 $\epsilon(S_0)$ 到 $\epsilon(S_1)$ 加一条标记为x的边。这个过程持续下去，就得到DFA。可见DFA的一个状态对应了NFA的一个状态集。如果这个NFA状态集包含了NFA的接受状态，相应的DFA状态也标记为接收状态。

书中给出的子集构造法的伪代码是错的。从某个NFA状态集合闭包起，对每个输入x都做出一个DFA的状态。而不是像书中那样，对所有输入得到的状态集合再求并集。可以参考编译器领域的龙书。

9.2.3 The Deterministic Image

由于子集构造法中，DFA的状态空间是NFA状态空间的幂集，在极不走运的情况下，可能面临存储空间过大的问题。本节介绍另一种NFA转DFA的方法------The deterministic image。

可见NFA $\tau$ 的deterministic image是一个DFA $\tau'$ . 二者的状态集一样，但是输入集合大不相同。 $\tau'$ 的输入集是 $\tau$ 的输入集与状态集的笛卡尔积。假设 $\tau$ 中有两个转换， $s\overset{x}{\rightarrow} t_1$ 和 $s \overset{x}{\rightarrow} t_2$ ，在 $\tau'$ 中转化成另外两个变换 $s\overset{xt_1}{\rightarrow}t1$ 和 $s\overset{xt_2}{\rightarrow}t_2$ 。显然这些变换分别符合NFA和DFA的特点。

Deterministic image方法的状态空间不变，输入空间增长了|S|倍。显然小于S的幂集的数目。

9.3 $\omega$ -Regular Automata

从本节开始，进入本章的难点。NFA和DFA通常是用来处理string的，即有限的序列。它们都需要指定一些接受或终止状态。而 $\omega$ -自动机是处理tape，即无限的序列。其中简单的一种叫做L-automaton。

定义很复杂，但是关键点如下

没有了终止状态，但是如何判断一个tape属于该L-自动机，换句话说，如何判断一个输入tape是合法的呢。L-automaton定义了一个cycle sets------- $C^A = (C_1, ... , C_k)$ , $C_i$ 是自动机状态集合的一个子集。L-自动机判定输入合法的条件有两个，任何一个成立都行。

输入会无数次经过自动机有向图的某条边，该条边被成为recur edge。
输入无数次经过的哪些状态的集合 $S^\infty(s^x)$ 是某个 $C_i$ 的子集。由于输入是无限的tape，而L-自动机的状态是有限的，假设某个状态ss被无数次经过，说明ss必然属于某个cycle中。这就是cycle sets名字的由来。

9.4 Formal Verification with L-Automata

9.4.1 $\omega$ -Regular Languages

主要定义了两种操作 $lim(\mathcal{L})$ 和 $\mathcal{L}^\omega$ 。需要注意 $\omega$ 和*的区别，前者用于产生tape，后者用于产生string。假设 $X=\{a,b,c\}$ ，则 $X^\omega$ 表示由a，b，c组成的所有无限长的tape的集合，而 $X^*$ 表示由a，b，c组成的所有有限长string的集合。

$lim(\mathcal{L})$ 是基于正则语言 $\mathcal{L}\subseteq{X^*}$ 定义的。 $lim(\mathcal{L})$ 包含了这样一些tape，他们有无限多的递增的前缀，而这些前缀都属于正则语言。
$\mathcal{L}^\omega$ 同样是基于正则语言 $\mathcal{L}\subseteq{X^*}$ 定义的。 $\mathcal{L}^\omega$ 包含了这样一些tape，他们是由正则语言 $\mathcal{L}$ 中无数个string组成。

了解就行，和本章其他内容关系不大。 $\mathcal{L}^\omega$ 可以拆成有限长 $\mathcal{L}^*$ 和无限长的 $lim{\widetilde{L}}$ 的concatenation。

9.5 $\omega$ -Regular Language Containment

9.5.1 Lifting Acceptance Conditions to a Product L-Automaton

难点来了， $\omega$ -Regular Automaton的主要应用是验证某个Design是否符合/满足某个property。这正是形式验证(Formal Verification)的一大分支(另一分支是验证逻辑等价)。

给定一个有限状态机 $M_P$ (sometimes called process) 和一个task L-Automaton $A_T$ (sometimes called property automaton). $M_P$ 对应了某个Design， $A_T$ 对应了我们要求design必须满足的property或约束。我们构造一个L自动机 $A_\times = M_P \times A_T$ 。两个自动机/状态机的积在本书的第七章有介绍， $A_\times$ 的状态集 $S_\times$ 为 $M_P$ 状态集 $S_P$ 和 $A_T$ 状态集 $S_T$ 的笛卡尔积 $S_\times = S_P \times S_T$ 。既然 $A_\times$

是一个L-Automaton，就需要定义它的cycle sets和recur edges来判定一个输入是否合法。

设 $C_T$ 是 $A_T$ 的某个cycle set，则我们在 $A_\times$ 中可以构造一个对应的 cycle set $C_\times$

假设 $A_\times$ 中有一条边 $(v_1, w_1) -> (v_2,w_2)$ ，而在 $A_T$ 中有一条recur边 $(w_1,w_2)$ ，则 $(v_1, w_1) -> (v_2,w_2)$ 为 $A_\times$ 的一条recur边。

以上两个操作，被称为Lifting Acceptance Conditions，即把 $A_T$ 的acception contions提升到 $A_\times$

我们知道 $M_P$ 是一个状态机，可以视为一个正则自动机。我们从正则表达式的角度理解， $M_P$ 实际上定义了一个正则language $L_P$ ，即一个string的集合。我们把 $L_P$ 中所有的string输入到 $A_\times$ 中，如果都被 $A_\times$ 接受的话，说明design $M_P$ 满足 $A_T$ 定义的property。

从另一个角度， $A_T$ 本身也定义了一个language $L_T$ , 如果 design $M_P$ 满足 $A_T$ 定义的property，这说明 $L_P \subseteq L_T$ 。所以用L-Automaton来验证某个Design 状态机的property的问题被称为language containment problem。其实 $A_\times$ 本身也表示了一个language $L_\times$ ， $L_\times$ 实际上是 $L_P$ 和 $L_T$ 的交集。如果language containment检测成立，即 $L_P \subseteq L_T$ 成立的话，应该有 $L_P = L_\times$ 。

9.5.2 Example of Product L-Automaton

第一个图是 $M_P$ ，对应了正则表达式 $(ab^+c)+$ ，第二个图是 $A_T$ ，表示了这样一个property：只要输入中出现了一个a，则后面某处必然会出现一个b。比如， $A_T$ 不允许这样的输入aaaaa......。第三个图是 $A_\times = M_P \times A_T$ ，表示了 $L_P$ 中的哪些string满足 $A_T$ ，如果全部满足，则说明 $L_P = L_\times$ ，从而 $M_P$ 满足 $A_T$ 。

在实际应用中，直接验证 $L_P$ 中每个string是否满足L-Automaton的cycle set检验或recur edge检验太困难了。我们换一个思路，对 $A_T$ 取反，令 $\overline{A_\times} = M_P \times \overline{A_T}$ ，如果 $\overline{A_\times}$ 表示的语言 $\overline{L_\times}$ 是空集，说明没有string能够在满足 $M_P$ 的同时不满足 $A_T$ 。换句话说， $M_P$ 表示的语言 $L_P$ 必然同时满足 $A_T$ ，即 $L_P \subseteq L_T$ 。也就是说，为了验证 $M_P$ 是否满足 $A_T$ ，我们通常要构造一个相应的language emptiness问题。构造language emptiness对偶问题的方法有很多，后面会介绍一种比较经典的方法。

9.5.3 BDD Representation of Cycle Sets and Recur Edges

我们知道BDD是用来表示bool表达式的。所以本小节的核心在于如何用bool表达式来表示自动机的一些特性。比如图9.23中最后一个子图，有三个状态，可以用两个bool变量表示。假设将 $v_1w_1$ 编码为 $x_1^{'}x_2^{'}$ ，将 $v_3w_1$ 编码为 $x_1x_2{'}$ ，则cycle set $C_1 = \{v_1w_1, v_3w_1\}$ 可以表示为 $x_1^{'}x_2^{'} + x_1x_2^{'} = x_2^{'}$ 。

这里还要回顾一下

可以看出transition relation本质上是一个描述了状态机行为的bool表达式。下标 $i = 1,...,n$ 表示用了n个bool变量编码状态机的状态。如果 $T(s,x,t) = 1$ ，表示 $(s,x,t)$ 这组取值是状态机的一个合法状态转换。所以transition relation等价于transition function $t = \delta(s,x)$ ，都是对状态机转换函数的描述。

L-automaton是特殊的状态机，需要额外一个变量 $r$ 来表示某个状态转换，也就是某条边是否是recur edge。扩展以后的transition relation如下

x和y是n维bool向量，分别表示现在和下一个状态。 $\sigma$ 是m维bool向量，表示输入。r是变量，表示该转换是不是一个recur edge。扩展的transition relatioin可以写成 $\left\{ \begin{matrix} \widehat{T}(x,\sigma,r,y) = T(x,\sigma,y).r & ; x\rightarrow y \ \text{is recur edge}\\ \widehat{T}(x,\sigma,r,y) = T(x,\sigma,y) & ;x\rightarrow y \ \text{is not recur edge} \end{matrix} \right.$

请注意，如果我们强行将recur edge上的r变量设成0，则 $\widehat{T}(x,\sigma,r,y) = \widehat{T}(x,\sigma,0,y) = 0$ ，这相当于从L-自动机删除了该转换。如果对应到L自动机的有向图， $r = 0$ 相当于删除了该recur edge。

9.5.4 The Language Containment Algorithm

最难理解的部分来了。记得Language containment问题最终会转化成L-automaton的language emptiness检测问题。在算法运行之前，我们需要对先对L-automaton的transition relation进行existential abstraction预处理。我们回顾一下什么叫做existential abstraction(第七章)

通俗地说，如果有一组bool变量的取值 $(x_1,...,x_{i-1},x_{i+1})$ 使得 $\exists_{x_i}f=1$ ，则对于原bool函数f，必然存在一组取值 $f(x_1,...,x_{i-1},0,x_{i+1},...,x_n) \ or\ f(x_1,...,x_{i-1},1,x_{i+1},...,x_n)$ ，使得 $f=1$ 。

我们用existential abstraction对L-automaton的transition relation进行预处理

预处理之后的bool表达式 $T(x,r,y)$ =1表示如果现状态是x，原L-自动机中存在某个转换 $x\overset{\sigma}{\rightarrow} y$ ，输入为 $\sigma$ ，并且连接x和y的边是或者不是recur edge(依赖于r是否为1)。 $\sigma$ 具体的值是什么并不重要，我们只要知道存在这样一个合法的转换就可以了。别忘了我们的问题是L-自动机是否为language empty，我们只关心有没有合法的输入string，不关心输入string到底是什么。这就是我们用exitential abstraction做预处理的原因。

下面是language containment的算法

判断一个L-自动机 $A_1$ 是否接受某个tape，需要检验该tape是否无限次经过某条recur edge或者该tape无限次经过的状态集是 $A_1$ 某个cycle set的子集。由于tape是无限的，如果无数次经过某个状态，那么意味着该状态一定处于某个cycle里，且cycle中其他的状态也被无数次经过。同样，recur edge被无数次经过，recur edge也一定处于某个cycle中。想象一下，如果我们把L-自动机 $A_1$ 的recur edge去掉，得到一个新的自动机 $A_2$ ，并且我们为 $A_2$ 定义新的cycle sets。首先我们取出 $A_1$ 中所有的被无数次经过的cycle(只是为了说明，不是要实际这么做)，得到一个cycle(对应了一个状态的集合)的集合 $\mathcal{Z}$ ，接着我们从 $\mathcal{Z}$ 中删除那些包含 $A_1$ 的recur edge的cycle，再删除那些被 $A_1$ 某个cycle set包含的cycle，得到 $\mathcal{Z}^{'}$ 。 $\mathcal{Z}^{'}$ 就是 $A_2$ 的cycle sets。可以看出， $A_2$ 没有recur edge，只有cycle sets一个接受条件。显然，如果一个tape被 $A_2$ 接受，就一定不会被 $A_1$ 接受。因此，我们可以将 $A_2$ 视为 $A_1$ 的取反。只要我们验证 $A_2$ 是language empty的， $A_1$ 的language containment检验就是successfull的。以上的分析是帮助理解的，算法具体的步骤如下

第一步：计算L-automaton的可达集合R(x). 注意每个状态可以表示为一个bool表达式，R(x)是这些bool表达式的和，因此也是一个bool表达式。

第二步：删除recur edge，等价于对r变量取0，即 $T(x,0,y)$ 。然后把transition relation限定在可达集合R(x)上，得到新的transition relation $\widetilde{T}(x,y) = T(x,0,y).R(x)$ 。我们可以认为 $\widetilde{T}$ 描述了前面说的 $A_2$ 。

第三步：计算transition relation $\widetilde{T}$ 的闭包 $\widetilde{T}^*$ 。 $\widetilde{T}$ 实际上定义了一种关系relation，即pair的集合。如果 $\widetilde{T}(x,y) = 1$ ，则(x,y)属于这个relation。 $\widetilde{T}^*$ 同样是一种关系，如果 $\widetilde{T}(x_1,x_2)=1, \widetilde{T}(x_2,x_3) = 1,...,\widetilde{T}(x_{n-1},x_n) = 1$ ，则 $\widetilde{T}^*(x_1,x_n) = 1$ 。如何从 $\widetilde{T}$ 得到 $\widetilde{T}^*$ 的bool表达式不是容易的事，有兴趣的读者可以去看原始论文“Testing language containment for $\omega$ -Automata using BDDs. 这里简单描述一下， $\widetilde{T}(c)(x,y) = \widetilde{T}(x,y) + \exists z (\widetilde{T}(x,z).c(z,y)))$ ，这里又用到了existential abstraction。函数c实际上是表示状态pair集合的一个特征函数，c(z,y)=1表示pair (z,y)属于c表示的集合。同样地，我们可以把 $\widetilde{T}(c)(x,y)$ 视为定义域为pair集合的函数。而我们要求的 $\widetilde{T}^*$ 就是 $\widetilde{T}(c)(x,y)$ 的最小不动点。具体如下

$\widetilde{T}^*(x,y) = lfp(\widetilde{T}(c)(x,y)) = \bigcap_{\widetilde{T}(c)(x,y)(A) = A}A$

可见， $\widetilde{T}^*$ 同 $\widetilde{T}$ 一样，都是状态pair集合的bool特征函数。

第四步，设原L-自动机的cycle sets $C = \{C_1, ..., C_i, ..., C_k\}$ 。首先我们看一下 $\widetilde{T}^*(x,y). \widetilde{T}^*(y,x)$ 代表了什么。由于 $\widetilde{T}^*$ 是 $\widetilde{T}$ 的闭包， $\widetilde{T}^*(x,y)$ 表示从x到y有一条路径，所以 $\widetilde{T}^*(x,y). \widetilde{T}^*(y,x)$ 描述的是一个包含状态x和y的环cycle。 $C_i^{'}(y)$ 表示状态y不属于cycle set $C_i$ . 接下来计算

$NC_i(x) = \exists_y(\widetilde{T}^*(x,y). \widetilde{T}^*(y,x).C_i^{'}(y))$

$NC_i(x)$ 描述了这样一些环，这些环至少存在某个状态y不属于cycle set $C_i$ 。而当前状态x属于或者不属于 $C_i$ 无关紧要。书中还有一个图对此做了形象的说明。

第五步：判断 $\bigcap_{1 < i < k}NC_i$ 是否为空集。如果不是空集，说明至少有一个环没有被原始L自动机的任何一个cycle set包含。我们就可以构造一个无数次经过这个环的tape，该tape被 $A_2$ 即(原始L-自动机的取反)所接受。因此 $A_2$ 不是language empty的。所以原始的L-automaton也通过不了language containment的检验。相反地，如果是空集，则说明language containment的检验成功。

9.5.5 Example of Containment Check

假设我们要对前面的图9.23做containment检验。

对第一个子图中的状态进行编码

对应到第二个子图中的(00,10,01)。第一个子图中带加号的边是recur edge，对应到第二个子图中标记为1的边，表示r=1。状态 $x_1x_2$ (11)不可达。

从第二个子图中去除recur edge和不可达状态 $x_1x_2$ (11)，得到子图三。子图三种只有一个环就是状态10本身，而原始L-自动机的cycle sets中只有一个cycle set $C_1$ ，就是{10,00}。显然环{10}被 $C_1$ 包含。换句话说，我们找不出一个不被 $C_1$ 包含的环，所以

$\bigcap_{NC_i} = NC_1 = \O$

从而language containment检验成功。回到图9.23，说明第一个子图描述的process $M_P$ 满足第二个子图描述的property $A_T$ 。

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第九章相关推荐

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第十章
Chapter 10 Multi-Level Logic Synthesis 10.1 Introduction 一个SOP F = xz + yz的电路如下图所示是两级的. 而multi-level ...
微软研究院研究员Ryan Beckett 博士论文《Network Control Plane Synthesis and Verification》下载—2018ACM最佳博士论文题目奖
欢迎关注微信公众号[计算机视觉联盟] 获取更多前沿AI.CV资讯论文下载关注微信公众号[计算机视觉联盟],回复关键词[Ryan]即可下载全文! 论文封面论文目录目前,Beckett 是微软研究 ...
《逻辑综合(logic synthesis)入门指南》
Hello, 欢迎来到逻辑综合的世界,在这里我将用尽可能通俗的语言,介绍什么是逻辑综合. 技术是不断进步的,因此本文会不断更,持续更新,记得收藏哦~~ 目录逻辑综合概述技术概述一.翻译二.高阶 ...
【Logic synthesis】ABC Command
ABC Command Combinational synthesis resyn,resyn2,resyn2rs(delay) rewrite;refactor;balance;多次迭代 balan ...
手机屏幕xy坐标软件_软件工程中的xy问题
手机屏幕xy坐标软件 XY problem is classified as a communication problem in which the person who asks the ques ...
Altera的几个常用的Synthesis attributes（转载）
各厂商综合工具,对HDL综合时都定义了一些综合属性这些属性可指定a declaration,a module item,a statement, or a port connection 不同的综合方 ...
(转)Altera的几个常用的Synthesis attributes
各厂商综合工具,对HDL综合时都定义了一些综合属性这些属性可指定a declaration,a module item,a statement, or a port connection 不同的综合方 ...
Formal equivalence verification 形式验证之等价验证 FEV 第8章
目录一.要检查的等价类型 1.组合等价 2.序列等价 3.基于事务的等价二.FEV用例 1.RTL -- netlist FEV 2.RTL--RTL FEV 1)参数化 2)序列修复--逻辑再分 ...
verilog synthesis
各厂商综合工具,对HDL综合时都定义了一些综合属性这些属性可指定a declaration,a module item,a statement, or a port connection 不同的综合方 ...

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第九章

Chapter 9 Finite Automata

9.1 Finite Automata and Regular Languages

9.2 DFA Synthesis

9.2.2 The Subset Construction

9.2.3 The Deterministic Image

9.3 $\omega$ -Regular Automata

9.4 Formal Verification with L-Automata

9.4.1 $\omega$ -Regular Languages

9.5 $\omega$ -Regular Language Containment

9.5.1 Lifting Acceptance Conditions to a Product L-Automaton

9.5.2 Example of Product L-Automaton

9.5.3 BDD Representation of Cycle Sets and Recur Edges

9.5.4 The Language Containment Algorithm

9.5.5 Example of Containment Check

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第九章相关推荐

最新文章

热门文章

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第九章

Chapter 9 Finite Automata

9.1 Finite Automata and Regular Languages

9.2 DFA Synthesis

9.2.2 The Subset Construction

9.2.3 The Deterministic Image

9.3 -Regular Automata

9.4 Formal Verification with L-Automata

9.4.1 -Regular Languages

9.5 -Regular Language Containment

9.5.1 Lifting Acceptance Conditions to a Product L-Automaton

9.5.2 Example of Product L-Automaton

9.5.3 BDD Representation of Cycle Sets and Recur Edges

9.5.4 The Language Containment Algorithm

9.5.5 Example of Containment Check

Logic Synthesis And Verification Algorithms Gary D. Hachtel Fabio Somenzi 第九章相关推荐

最新文章

热门文章

9.3 $\omega$ -Regular Automata

9.4.1 $\omega$ -Regular Languages

9.5 $\omega$ -Regular Language Containment