面向敏捷硬件设计的符号模拟器设计与实现*

邹鸿基，李 暾，罗 丹，方雨德

(国防科技大学计算机学院,湖南 长沙 410073)

1 引言

缩短设计周期，降低设计成本，提高设计生产率，一直是集成电路设计面临的重要挑战。为应对这些挑战，研究人员提出了多种设计方法和设计理念，敏捷硬件设计方法正是近年来出现的一种新设计方法。该方法借鉴敏捷软件设计方法，通过设计方法、设计工具链的革新，使得集成电路设计流程变“轻”，以提高设计生产率。一些成功案例显示了该方法强大的设计效能[1,2]。

在敏捷硬件设计方法中，前端建模主流技术是依托某种高级程序设计语言(如Scala、Python)设计领域特定语言DSL(Domain Specific Language)，通过定义支持寄存器传输级RTL(Regist-er Transfer Level)建模的端口、寄存器、连线和逻辑单元类等语言机制，扩展现有语言的硬件描述能力，并在运行程序时自动生成Verilog或其他格式的RTL电路描述，这种DSL又称为硬件构建语言HCL(Hardware Construction Language)。

HCL运行时生成硬件借鉴了编译技术，引入了类似于LLVM(Low Level Virtual Machine)[3]的中间格式。在将HCL描述编译为中间格式后，可在此基础上快速地评估各种后端设计参数对设计的影响，或围绕中间格式研究各种设计验证技术，如等价性检查、模型检验、限界模型检验和测试生成等。上述各种验证技术所需要的共性技术是符号模拟，但目前还未有针对敏捷硬件设计前端建模的符号模拟支持。

针对该问题，本文以PyRTL DSL[4]为目标，设计并实现了一个符号模拟器，以支持后续测试生成、限界模型检验和等价性检查等验证技术的研究。本文主要贡献为：

(1)探讨了基于中间格式的符号模拟方法；

(2)建立了中间格式与可满足性模理论SMT(Satisfiability Modulo Theory)[5]之间的映射规则；

(3)为敏捷硬件设计形式化验证构建了基础。

本文给出的方法不局限于PyRTL，还可迁移到任何中间格式上，例如FIRRTL[6]、CoreIR[7]和LLHD[8]等。

2 背景

2.1 PyRTL简介

PyRTL是由加州大学圣巴巴拉分校体系结构实验室基于Python设计的一种硬件设计DSL。PyRTL在Python的基础上提供了一组RTL级建模的原语，以支持精准的设计描述，利用设计模式技术提高设计建模的效率。它要求所有逻辑都是同步和可综合的，也是一种基于执行的设计构建语言。PyRTL的目标是简单、易用和可扩展，支持RTL级设计描述、模拟、测试与跟踪等。目前，PyRTL支持与Xilinx PYNQ的集成，便于快速开发片上系统SoC(System on Chip)原型。

PyRTL设计背后的主要动机是通过一组Python类帮助用户精确地描述数字硬件结构。为了实现简单性和清晰性，PyRTL有意将用户限制在一组合理的数字设计实践中。例如，时钟和复位信号是隐式的，默认情况下块内存是同步的，不存在未驱动或高阻抗状态，不允许未注册的反馈，等等。这样，任何以有效代码表示的设计总是与可综合的硬件相对应。

PyRTL提供了WireVector数据结构来构建逻辑单元之间的连线，共有5种不同类型的WireVector：Basic、Input、Output、Const和Register。Basic将2个或多个不同的逻辑元件连接在一起，Input和Output表示电路的输入和输出信号，Const表示电路中的常量，而Register表示寄存器，存储下一拍的输出信号值。为支持构建复杂的电路逻辑，WireVector上重载了算数运算符、逻辑运算符和比较运算符等多种运算符。除此之外，PyRTL还提供了concat、concat_list等函数来支持对WireVector进行位操作，提供了Conditional Blocks来支持条件语句，提供了select、mux等函数来支持选择操作。

图1给出一个简单的PyRTL电路，描述了一位加法器，它有3个输入a、b、c,2个输出sum、carrry_out：

Figure 1 adder图1 加法器

2.2 PyRTL中间格式

PyRTL中间格式的目标是为RTL之后的硬件设计处理提供一套完整的操作和结构。PyRTL提供了Block和WireVector 2种内置的数据结构，支持以自底向上的方式构建硬件。Block是由基本逻辑单元组成的设计，它存储基本逻辑单元以及它们之间的互连。每个逻辑单元用一个LogicNet来表示，每个LogicNet是一个4元组，一般形式如下所示：

(operator,parameters,args,dests)

其中，operator表示LogicNet可执行的操作，用单个字符表示；parameters表示LogicNet完成操作时，除输入信号外可能需要的额外参数，这些参数不能在运行时更改；args表示LogicNet的输入信号集；dests表示LogicNet的输出信号集。

PyRTL中间格式定义了一些基本的LogicNet操作，如下所列：

(1)逻辑运算和算术运算：如加减、与或等，按其标准定义执行指定的算术或逻辑运算，每一种运算都有2个参数。

(2)基本的比较操作：“=”检查WireVector的每一位是否相等，而“<”和“>”执行无符号算术比较。所有比较操作的输出是位宽为1的WireVector。

(3)w和n运算：w是一个没有逻辑函数的缓冲区，而n为非运算。

(4)x运算：表示一个多路选择器，含3个参数，第1个参数是1位选择信号(select bit)，如果第1个参数的值为0，选择第2个参数；如果为1，选择第3个参数。

(5)c运算：为concat操作符，将任意数量的线向量(a0,a1,…,an)拼接成一个新的WireVector，其中a0为最高位，an为最低位。

(6)s运算：为选择操作符，它根据指定的常量参数，选择WireVector的一个子段。

(7)r运算：代表一个寄存器，在时钟上升沿，它将值从输入复制到寄存器的输出。

(8)m运算：代表内存的一个读取端口，它支持异步或同步读取。

(9)@运算：代表内存的一个写端口，支持同步写。

图2为图1中间格式对应的电路图。

Figure 2 Circuit diagram图2 电路图

图2中，a、b、c对应图1中定义的输入，sum和carry_out对应图1中定义的输出；tmp1=a∧b，tmp2=tmp1∧c，sum=tmp2，对应图1中的sum<<=a∧b∧c；tmp3=a&b，TEMP1=tmp3，对应图1中的temp1<<=a&b；tmp4=a&c，tmp0=tmp4，对应图1中的temp2<<=a&c；tmp5=b&c，对应图1中的temp3=b&c；tmp6=TEMP1∧tmp0，tmp7=tmp5∧tmp6，carry_out=tmp7对应图1中的carry_out<<=temp1|temp2|temp3。

3 符号模拟器设计

模拟是集成电路设计验证常用技术之一，对集成电路进行模拟时，首先建立电路模拟模型，然后注入模拟激励以激活电路模拟模型，通过运行模拟程序验证该模型。通常输入的模拟激励是0、1这样的二进制值。模拟算法通常分为事件驱动的模拟方法和基于节拍(cycle-based)的模拟方法。

3.1 主要原理

符号模拟仍是一种模拟验证方法，但其接收的模拟激励不仅是具体的值，还包含符号。符号模拟的主要思想是用符号代替具体值作为电路模拟模型的输入，利用模拟算法，由初始输入出发，依次经过电路的各个节点，计算出每个节点的符号表达式，直到电路的输出端，得到由初始符号组成的表达式，该表达式是一种体现电路功能的约束函数。

对组合电路，可从初始输入开始至最终输出，将逻辑单元输入输出连接起来，形成用初始输入表示的最终输出的逻辑函数。而对时序电路，则需对电路按一定的节拍数展开，得到组合电路后再进行处理。而在展开时序电路时，需要根据所使用的模拟算法考虑或忽略逻辑单元的延时。

本文基于PyRTL中间格式，采用基于节拍的模拟算法，设计并实现符号模拟器，主要挑战是如何利用中间格式将电路展开并表示为SMT约束，且能用于其他验证任务。为处理PyRTL中间格式表示的电路既包含字级信号，又包含位级信号，本文选用了SMTLIB2(Statisfiability Modulo Theories LIBrary 2.x)[9]格式作为转换目标。SMTLIB2表示是标准格式，可被遵循该标准的各种SMT求解器求解，如Z3[10]、CVC4[11]和Boolector[12]等。

3.2 算法设计

针对PyRTL的中间格式，符号模拟器算法的具体步骤如下所示：

Step1通过Block对象，获得电路的中间格式。

Step2记录LogicNet中出现的所有Const类型的常量。

Step3判断电路类型，如果是组合逻辑电路，跳转到Step 4；如果是时序逻辑电路，跳转到Step 5。

Step4直接遍历中间格式保存的每一个LogicNet，判断符号是否已定义，再根据其功能转换成不同的SMT语句，具体转换方法见3.3节的转换规则，最后将Step 2中保存的常量转换成SMT语句，一并写入文件。

Step5对时序逻辑电路进行展开，利用节拍计数对不同周期的同一符号进行区分，得到一个组合逻辑电路。按Step 4对展开的每一拍电路进行转换。

符号模拟器的应用方法如图3所示。

Figure 3 Symbolic simulation process图3 符号模拟过程

算法Step 1中，如前所述，所有的LogicNet及其连接关系都保存在Block对象中，因此可以从对应的Block对象中得到设计中包含的所有逻辑单元，以及逻辑单元之间的连接关系。

算法的核心在Step 4，需要将电路从PyRTL的中间格式转换为SMTLIB2格式，以便于后续使用。这种转换需要按照LogicNet逻辑运算含义，按一定规则转换为SMTLIB2中相应的运算及其约束表示。

当需要进行符号模拟的电路为时序电路时(算法Step 5)，必须将电路展开，展开后的电路为一个组合逻辑电路。除了按照转换规则将电路转换为SMTLIB2格式外，还需要为电路中的信号名换名，以区分不同周期间的同名信号。其换名方法是为信号名增加一个标记，用于标识是第几拍的信号。

3.3 转换规则

2.2节表示LogicNet的4元组可写成如式(1)所示函数形式：

dests=operator([parameters],args)

(1)

该函数表示利用参数parameters和输入args执行操作operator得到输出dests，其中parameters为选择使用。

在SMTLIB2中表达式用前缀形式表示，格式如式(2)所示：

(opa1a2…an)

(2)

表示对a1,a2,…,an执行操作op。

因此，根据操作语义，可将式(1)中赋值符号右边部分operator([parameters],args)转化成SMT表达式，如式(3)所示:

(operatorargs[0]args[1] …args[n])

(3)

而SMT表达式中的等号可表示为:

(=ab)

(4)

综合式(3)和式(4)，可知式(1)转化为SMT表达式的规则如式(5)所示:

(=dests(opargs[0]args[1] …args[n]))

(5)

最后使用assert将此表达式转换为SMT约束，即在约束求解过程中需被满足的条件，规则如式(6)所示：

(assert(=

dests(operatorargs[0]args[1] …args[n])))

(6)

对于LogicNet中无法直接对应SMTLIB2的operator，需要使用多个SMTLIB2的操作op进行转化。由于如式(2)所示的表达式依然可作为操作数嵌套使用，因此，多个操作op可表示成:

(op1(op2a1a2…an)(op3…)… (opn…))

(7)

一般而言，需要用到LogicNet中参数para-meters的情况主要有以下2种：

(1)利用参数parameters和输入args共同得到输出dests，即parameters也是LogicNet输入参数之一，按照式(7)的规则，此时可将式(6)的输入args替换为参数parameters和输入args的表达式：

(assert(=dests(op1((op2param[0] …param[n])args[0])((op2param[0] …param[n])args[1]))))

(2)参数parameters将作为LogicNet输出之一被修改，此时，parameters的功能与情况(1)中的dests一致。此时，可在将式(1)转换为式(5)之外，再增加一条约束，规则同式(5)，如下所示：

(assert(=parameters(operatorargs[0] …args[n])))

对LogicNet转换的关键是对其operator的转换，经对比operator与SMT中运算的语义，本文给出operator的转换规则，如下所示：

(1)当operator为&、|、∧、n、+、-、*、=、<、>、c时，参数parameters为空，args的长度为2，dests的长度为1，具体含义为dests[0] =args[0]opargs[1]。故此时生成的SMT约束为:

(assert(=dests[0] (opargs[0]args[1])))

(2)当operator为～、w、r时，参数parameters为空，args的长度为1，dests的长度为1，具体含义为dests[0] =opargs[0]。故此时生成的SMT语句为：

(assert(=dests[0] (opargs[0])))

注意，r表示寄存器单元，表示前一个周期的args[0]与当前周期的dests[0]相等，因此需要对符号所在周期进行区分，如寄存器输入为la，输出为lb，则在第1个周期中，生成的SMT约束为(assert(=lb_0la_1))，其中_0和_1分别表示第0拍和第1拍。

(3)当operator为x时，表示一个多路选择器，此时参数parameters为空，args的长度为3，dests的长度为1。多路选择器定义的操作为ifargs[0] =0 thendests[0] =args[1] elsedests[0] =args[2]。利用SMT的ite(if-then-else)运算，转换后得到的SMT语句为：

(assert(ite (=args[0] #b0)(=dests[0]args[1])(=dests[0]args[2])))

其中#b0表示二进制0。

(4)当operator为c时，表示将args中的信号拼接为一个新信号。引入SMT中的concat后，转换得到的SMT语句为：

(assert(=dests[0] concat (args[0]args[1] …args[n])))

(5)当operator为s时，表示根据parameters指定的位，将args的某些位挑选出来，再合并为一个新的WireVector信号。引入SMT的extract操作选择相应的位，((_extractlalb)lc)表示选择lc[la:lb]位。由于parameters中保存的是选择的每一位，可以用n个((_extractparam[i]param[i])args[0])选出所有的位，再利用concat将这些位串联起来。此时，需要注意，WireVector类似于Python中的list，但WireVector中的最低有效位LSB(Least Significant Bit)保存在索引为0处。而在SMT提供的BitVec类型中LSB在最右边。所以，最后将选择的所有位合并时，需要将顺序颠倒后再合并，最终转换得到的SMT语句为：

(assert(=dests[0] concat(((_extractparam[n]param[n])args[0])… ((_extractparam[0]param[0])args[0]))))

(6)当operator为m时，它执行的是读存储器功能，参数parameters为一个元组，包含2个引用，一个是内存端口memid，另一个是对包含该端口的内存实例的引用mem。此时args的长度为1，dests的长度为1。

引入SMT的Array类型来表示存储器，定义为：

(declare-constmem(Array(_BitVecm)(_BitVecn)))

其中_BitVecm定义一个m位的_BitVec，mem为存储器的符号，m为存储器的地址位数，n为存储单元的位数。对于读存储器，可以利用select操作处理，转换得到的SMT语句为：

(assert(=(selectmemargs[0])dests[0]))，表示dests[0] =mem[args[0]]。

(7)当operator为@时，它执行的是写存储器功能，参数parameters为一个元组，包含2个引用，一个是内存端口memid，另一个是对包含该端口的内存实例的引用mem。此时args的长度为3，分别为存储地址、数据和写使能信号，dests的长度为0。只有写使能为高电平时，才能对存储器进行写入。引入SMT的store操作进行转换，最终得到的SMT语句为：

(assert(ite (=args[2] #b1)(=(storeargs[0]args[1])mem)(=memmem)))

其中#b1表示二进制1。

具体含义为：if 写使能 =1 thenmem[args[0]] =args[1] elsemem=mem。

(8)PyRTL支持提前定义一个存储器ROM。此时，存储器的数据存储由用户设定，存储在rom_blocks中。因此，将带有ROM的电路转换为SMT约束时，还需要利用类似写存储器的方法对ROM初始化，此时就没有写使能，直接利用store操作进行，如(assert(=(storeaddrdata)rom))，把rom_blocks中所有的数据转换为SMT语句。

以图1的加法器电路为例，由于加法器是组合逻辑电路，直接按照转换规则，得到的SMT语句如下所示：

1 (declare-consttmp2 (_ BitVec 1))

2 (declare-consttmp1 (_ BitVec 1))

3 (declare-constc(_ BitVec 1))

4 (assert(=tmp2 (bvxortmp1c)))

5 (declare-constsum(_ BitVec 1))

6 (assert(=sumtmp2))

7 (declare-constcarry_out(_ BitVec 1))

8 (declare-consttmp7 (_ BitVec 1))

9 (assert(=carry_outtmp7))

10 (declare-consttmp4 (_ BitVec 1))

11 (declare-consta(_ BitVec 1))

12 (assert(=tmp4 (bvandac)))

13 (declare-consttmp0 (_ BitVec 1))

14 (assert(=tmp0tmp4))

15 (declare-consttmp6 (_ BitVec 1))

16 (declare-constTEMP1 (_ BitVec 1))

17 (assert(=tmp6 (bvorTEMP1tmp0)))

18 (declare-constb(_ BitVec 1))

19 (assert(=tmp1 (bvxorab)))

20 (declare-consttmp3 (_ BitVec 1))

21 (assert(=tmp3 (bvandab)))

22 (assert(=TEMP1tmp3))

23 (declare-consttmp5 (_ BitVec 1))

24 (assert(=tmp7 (bvortmp6tmp5)))

25 (assert(=tmp5 (bvandbc)))

第1～3行定义3个1位的BitVec变量tmp1、tmp2、c。第4行表示tmp2 =tmp1 ^c，对应图2中用椭圆标记的异或门。

4 实现与实验结果

本文利用Python实现了符号模拟算法，约700行代码，并已集成到PyRTL中(本项目已开源到GitHub,地址为https://github.com/zou-sheng/PyRTL)。目前，已实现的符号模拟器用于模拟激励自动生成，底层使用Z3求解器，对符号模拟的结果进行求解，得到满足要求的模拟激励。

为验证所实现的符号模拟器的正确性，本节在一些设计实例上，以自动生成的模拟激励为输入，利用 PyRTL提供的模拟功能，通过对比模拟输出，来判断自动生成的模拟激励是否能恰好在指定节拍上得到预期的结果。

实验所用的机器为配备了Intel i5-8250U CPU和2 GB内存、操作系统为ubuntu 16.04的计算机系统。

实验电路包括一个简单状态机、简易乘法器、Wallace树形乘法器，以及128位AES加解密电路。实验电路性质如表1所示。

Table 1 Experimental circuits表1 实验电路

表1中，简单状态机有2个1位输入信号决定状态变化。简单乘法器有2个32位输入表示运算数，以及1个1位信号reset。Wallace树形乘法器与简单乘法器类似，有2个32位运算数和1个1位的reset信号，但该乘法器中还提供1个可配置参数shifts，表示每个周期的移位次数。当shifts=1时，乘法器就变成了简单加法器；当shifts=32时，只需要1个周期的延迟即可得到乘法的结果。AES加解密电路有2个128位的输入，分别表示明文和密钥，还有1个1位信号reset。

对每个电路，指定随机的输出结果，展开指定的节拍后，通过约束求解生成模拟激励。生成模拟激励的过程进行了多次，取平均耗时。实验结果如表2所示。表2列出了各电路展开的节拍数、自动生成模拟激励的平均时间。

Table 2 Experimental results表2 实验结果

此处需特别说明的是AES加密电路的模拟激励生成，将明文和密钥输入AES加密电路，经过10轮加密得到最终的密文。

(1)如果将明文和密钥作为符号模拟器的输入，大约需220.65 s，可以得到符号模拟的结果。加密过程中的字节替换和列混淆都需要读取预先设置的存储器。

(2)如果将密文和密钥作为符号模拟器的输入求解明文时，一些信号唯一对应存储器中的值，而Z3求解器需要逐一对存储器中的值进行测试，所需时间很长。

(3)如果将这53个对应存储器值的信号每个周期的值(共636个)，都作为符号模拟器的输入，大约需193.35 s，可以求解出正确的明文。

通过对比模拟结果可知，以表2指定节拍数为约束，自动生成的模拟激励为输入模拟后，一定能在指定节拍时观察到正确的输出结果。由此，本文实现的符号模拟器是正确的。

5 结束语

本文介绍了一个面向敏捷硬件设计的符号模拟器的设计与实现，核心工作是PyRTL中间格式至SMTLIB2格式的转换，以及时序电路展开后的变量命名。目前实现的符号模拟器较为直接，接下来的研究方向有2个：(1)加入更多的共性优化方法，发挥SMT求解器能力，使其能处理更大规模的设计；(2)根据具体应用，如限界模型检验、等价性检查进行针对性的优化。