[高层综合动态等效检查器] 高层动态

　　摘要：本文介绍的是一种介于未定时序（Untimed）的行为描述（如ANSI C）与RTL间的动态等效检查方法。高层综合（High Level Synthesis; HLS）提供了一条快速和简便的路径，将使用高阶语言所描述的行为综合为RTL。而本文介绍的检查方法，其好处之一在于软件工程师和硬件工程师可共享相同的测试数据。该方法可让硬件工程师复用原本用于软件验证的未定时序输入测试向量（Test Vector），并将RTL仿真（Simulation）产生之结果与进行软件验证时所获得的黄金参考输出来做比较。我们将这一方法称为动态等效检查方法，这种方法可将未定时序的输出与RTL仿真结果的已定时序（Timed）输出进行比较，并将出现的任何不匹配结果显示出来。为了验证我们的方法，我们加强既有的一个HLS工具后端并制作了一个测试平台（Testbench）的自动产生器。此方法可运用于各种不同的设计时间，这在本文中均有提及。结果显示，此方法非常有效且用法极其简单。
　　
　　1 简介
　　
　　 在超大规模集成电路的设计中进行更高层的抽象设计，与传统的RTL设计相比有一些明显的优势。首先，大多数的设计都开始于高层模型，以方便验证所要实行的应用。高层综合方法在这些模型和RTL之间提供了一条直接的途径。根据实际经验[1]，通常1行的C程序代码可被转换成7行的RTL代码。这代表着行为描述更加容易被维护，并排除错误，而且由设计人员带来的程序错误也会更少。其次，许多情况下，设计规格的不确定，规格的任何变化都会导致不同的设计架构变更（如on-die存储或外部存储、总线的分层）。在传统RTL的设计中，这将导致大规模的重新设计。而在行为层，这些变更则变得容易处理。第三，提供抽象的层级使得软件和硬件的设计人员能够使用同一种语言来沟通。现今在特定硬件上运行的应用已变得越来越复杂，且大都以复杂的数学模型为基础，在许多情况下变得难以被硬件设计人员所理解。而采用同一种行为描述语言则可让硬件和软件设计人员在同样的抽象层级上进行交流。这一些复杂应用的例子包括：基于复杂加解密算法的专用硬件安全引擎[2]。
　　 下面我们将从验证的角度说明行为综合（Behavioral Synthesis）的优势。高层综合与模型产生器在不同设计时间的结合使软件设计员可复用测试向量。此外，这些模型产生器使得可复用的不仅是未定时序的输入测试向量，也包括了以软件仿真（SW Simulation）的输出作为已定时序硬件仿真的黄金参考输出。再者，这些模型的优点还包含能够加速传统耗时的RTL仿真。传统RTL的仿真速度非常慢，常常无法利用它来完成整个SoC仿真。相比之下，行为仿真的模型则可使仿真的速度加快，因此可允许对更大型的设计来进行仿真。
　　 我们在文中提供了完整的验证流程，可使HLS在不同的抽象层次利用模型产生器来充分发挥HLS的能力。我们还展示了一种动态的等效检查方法，可复用未定时序的软件输入向量，以及使用软件仿真的输出向量作为周期准确模型以及RTL仿真的黄金参考输出。
　　
　　2 动机
　　
　　 NEC在过去的20年里发展了一种ESL综合环境，称为CyberWorkBench（CWB）[3]。CWB可用来将未定时序的C、SystemC或SpecC 的程序代码，以传统的HLS方式，即通过为控制单元和数据通路单元创建FSM的方式生成Verilog 或VHDL。数据通路单元主要是由一些功能单元（Function Unit; FU）加上寄存器和多任务器所构成。
　　 本文的重点在HLS的验证部分。我们的办法是，在可能的最高抽象层级提供路径来验证设计并排除其中的故障程序，从而加快验证过程，缩短验证周期。为了达到这一目的，我们研发了模型产生器（Model Generator），可根据须进行验证的不同设计时间而产生不同的仿真模型。如图1所显示的，就是在不同验证阶段所需的各种模型产生器。在采用HLS时，设计人员所要做的第一步就是手动调整原先的软件描述，使其成为能被综合的程序代码。那些在HLS无法被支持的典型结构，主要就是动态存储分配（Dynamic Memory Allocation）和递归函式（Recursion）。在此阶段，设计人员还要细化数据型态（Data Type）以尽可能获得最小、最有效率的设计模型。为此，大多数的HLS透过将C的语法扩展来提供符合硬件设计的数据型态。为了进行数据型态细化后的验证，我们创建了一个行为模型产生器；并可用它得到一个C++程序模型，此模型可用来代表经手动调整后的行为描述。这种模型产生器所产生的模型不仅是数据型态经过细化的C++程序，还包括了一个测试平台（Testbench），除了允许复用原本用于软件仿真的输入向量，也可让软件仿真的结果与行为仿真中所获得的结果来做比较。
　　 HLS之后，就可执行一个周期准确（Cycle-accurate）的仿真来进行已定时序的验证，这时需要一个能快速产生SystemC仿真模型的周期准确模型产生器。在HLS的排程阶段执行后，这些能周期准确地仿真RTL行为的SystemC模型（通过HLS后产生的副产品）将得以被创建。而一个可复用未定时序的软件输入和输出的测试平台也会被创建出来。每个输入输出端口的有效信号也自动产生，因为什么时候需要读取数据，以及什么时候有效的数据会被写出，都需要在测试平台上显示出来。这是此验证方法对我们所做的最主要贡献，也会在下一节内容中加以详细说明。我们将这种验证方法称为‘动态等效检查法’，因为用这种方法可以在一个已定时序的仿真中完全地复用未定时序的输入和输出测试向量。设计流程的最后一步验证是要验证HLS所产生的最终RTL。为此，要有一个RTL测试平台产生器来创建一个可复用未定时序输入测试样本（Test Pattern）的测试平台，并将测试的输出与原有未定时序的黄金参考输出进行比较。
　　 这些不同模型产生器的结合与RTL的测试平台产生器将允许该电路设计在不同的阶段得到验证，而不需返回到缓慢的RTL仿真程序去。经证实，行为模型产生器的仿真速度比传统RTL仿真快 1,000倍，而周期准确模型则比RTL仿真快上100倍！[4]
　　
　　3 HLS设计空间探索
　　
　　 在继续说明验证方法之前，我们需要进行一些额外的说明来了解我们方法的优点。高层抽象与高层综合结合的优点之一就是能够快速且容易地进行架构取舍性（trade-off）的空间探索，例如，数组可被映像到不同的存储（双口或单口）、或寄存器及其扩展。设计空间探索（Design Space Exploration; DSE）可通过手动改变原始的未定时序描述或令其完全地自动化运行；其中包括以前置处理指令（Pragma）的插入来进行综合指示，或通过改变功能单元（FU）的数量限制文件（Constraint file）来进行。这些前置处理指令可告诉行为综合器如何进行各种不同的综合操作。可探索（Explorable）操作指的是针对那些具有可多重硬件实现的架构（例如数组、循环和函式），来进行探索。
　　 图2显示的是一个利用乘法与加法的计算来实现FIR filter的源代码。经由DSE，可得到一个由二组数组（其中分别存输入的主数据和附属系数）与二个循环所组成的结构。在代码右侧表格显示的是HLS在不同综合属性下执行的结果，这些属性通过前置处理指令在DSE操作中被设定。从这里可看出，面积最小但最慢的设计与面积最大但最快的设计中存在显着的差异，从7033个到9927个逻辑门数，而延迟时间（Latency）则从1个到12个周期不等。根据不同属性及副属性（如数组对映至存储的存取端口数）的组合，这些设计通常含有多个帕累托最优（Pareto-optimal）组合，但这里我们只列出三组。在这些设计组合中，只要能符合设计者的限制要求，则其RTL将被自动生成。但现在的问题是，如何在含有不同延迟时间的帕累托最优组合下，去验证各种不同的设计。在传统的RTL验证方法里，输入向量为了不同的设计得要重新订定时序以进行调整，这很耗费时间且容易出错。因此，我们提出了这个自动的动态等效检查方法，对于输入和输出，它不需要任何的时序信息，因此可完全自动地复用原先用于软件验证时的未定时序输入和输出测试向量。
　　
　　4 动态等效检查方法
　　
　　 动态等效检查（Dynamic Equivalence Checking; DEC） 相对于形式等效检查（Formal Equivalence Checking），后者主要是用于门-网表（Gate-netlist）与RTL间的等效检查。形式等效检查技术所依据的是70年代开始发展自软件的验证技术[5][6]。到了70年代末期，这种技术才第一次被用于硬件验证[7]，之后市面上出现了多种Gate-RTL的形式等效检查器[8][9]，甚至是用于HLS-RTL的形式等效检查器[10]。图3显示的是设计流程在不同阶段的概观，这些设计流程通常采用等效检查。而我们在此提供一个DEC，其作用与形式等效检查一样，告诉设计者较低层级的设计是否与原有高层级设计的描述等效。在此，就是C或SystemC转换为RTL。如前所述，通过改变区域性综合指令、全局性综合属性或FU数量的限制文件，HLS就可综合出各种不同的设计。由此得到的设计有不同的延迟和吞吐量，这些都必需被等效检查器考虑进去才行。图4显示的是前一节所讨论过的FIR filter程序，其执行完DSE的结果。在此我们特别列出三组设计及其相对应的信号表（Signal Table）。信号表主要是在HLS之后所一起产生出来的，主要用来显示数据在各个输入和输出端口进行读取与写入的状态。在此，状态00则代表重置（Reset）的状态。第一个设计只有1个周期的延迟，而第二个设计则有2个周期，最后一个设计则多达6个周期。最下面一行显示的是各个设计所使用的FU数量。依图表显示，只有一个周期延迟的电路设计需要最多的FU，并且占用较大的面积；而较慢的设计，其所需要的FU数量就越少。通常情况下，原本用于软件验证时的测试向量，均需要调整以适应硬件的测试平台。设计者应根据不同设计所改变的延迟或吞吐量（如图4），对测试样本进行同步的修改。
　　 为了避免这样的情况，我们提出了一种事务级（Transaction Level）的仿真环境。HLS环境为每个输入和输出端口产生一个有效信号。每次当输入需要被读取或有效输出被写到端口时，这些有效信号就会产生一个脉冲。HLS工具可以很容易地生成这些信号，因为它知道状态转换图表（State Transition Diagram）。因此，图1中的RTL生成后端被修改为可自动生成这些有效信号。图5显示的是一个FIR filter程序的例子。图5 （a）为带有主要数据、系数输入端口和数据输出端口的原始模型；图5 （b）则为HLS工具自动生成带有效信号的模型，其目的是用以表明（assert）输入信号被需要时，及代表有效输出的产生。这一个简单但极其有效的方法，加上自动的测试平台产生器允许再次有效率地使用未定时序的输入向量和输出向量作为黄金参考模型。在我们的方法里，使用者只需将每个端口的测试向量分写成与该端口相同名称的文件。则当输入的有效信号产生时，测试平台就会输入新数据。而当输出端口的有效信号产生时，测试平台则会自动把输出值与输出文件中存储的参考数值进行比较。
　　
　　5 实验结果
　　
　　 通过验证在DSE过程中所产生的不同FIR filter设计，我们展示了所提方法的有效性。为此，我们利用了之前为了HLS所开发的自动探索器[11]。探索的结果可再次于图4中被观察到。在取舍性曲线上的每个设计点，都可生成一个行为模型、周期准确模型和一个RTL测试平台。接着用同样用于软件验证的未定时序输入测试向量来执行这些模型。软件仿真的结果可作为黄金参考输出而用来检查仿真的结果。图6是一个由周期准确模型仿真后所输出的波形图（waveform, VCD file）。图6（a）为2个延迟的FIR filter设计所产生的仿真结果，而图6（b）则为8个延迟的filter所产生的结果。我们可以观察到，这二个例子中所得到的是相同的结果（0x05, 0x01 与 0x04），而这里使用的是完全相同的输入测试向量。有效信号在此以圆圈标示出来，当有效信号变高时，可观察到新的数据会被输入到相对应的端口。而当有效输出产生时，也会告诉测试平台将其结果与黄金参考输出的数据进行比较。这证明了我们的方法是可行的，并可运用于行为描述的源代码、已定时序的C行为模型与最终RTL间的等效检查。
　　
　　6 结论
　　
　　 我们在此提出了在行为层设计SoC所面临的挑战与机会，尤其是对验证方法的关注。我们研发了一系列的模型产生器，从对数据型态细化的仿真产生器到进行已定时序验证的周期精确模型都有。我们还提出了一种方法，能复用原本软件验证时所用的未定时序测试向量来进行周期精确模型或RTL的已定时序验证。再来就是，软件仿真的输出向量亦可用来作为黄金参考模型，并对HLS和RTL的正确性进行验证。在实验结果说明一节里，我们用自动运行的设计空间探索器来验证我们的方法的确有效，并说明我们的方法健全且运行良好。
　　
　　 致谢
　　 对于NEC公司中央研究实验室、NEC信息系统和NEC-HCL-ST中每位参与此项研究工作的人员，作者谨对这些人员所提供的帮助表示衷心感谢。
　　
　　参考文献
　　[1] N. Kobayashi, K. Wakabayashi, H. Tanaka, N. Shinohara, T. Kanoh, “Design experiences with high-level synthesis system Cyber I and behavioral description language BDL,” Proc. of Asia Pacific Conf on Hardware Description Languages, Oct 1994.
　　[2] S. Morioka, K. Wakabayashi, B. Carrion Schafer, “Complex Security Engine Design with High Level Synthesis”. MPSoC, 2009.
　　[3] CyberWorkBench, “https://www.省略”
　　[4] P. Coussy and A. Moraweic, “High-Level Synthesis from Algorithm Digital Circuit”, Springer, ISBN 978-1-4020-8587-1, pp 113-127, 2008.
　　[5] J.C. King. “A new approach to program testing. SIGPLAN Notices”, Proc. International Conf. on Reliable Software, 10（6）:228-233, 1975
　　[6] J.A. Darringer and J.C. King, “Applications of symbolic execution to program testing”, IEEE Computer, 11. Vol.4, pp.51-60, 1978
　　[7] J.A. Darringer, “The application of program verification techniques to hardware verification”, Proc. ACM/IEEE Design Automation Conference （DAC）, 1979.
　　[8] Formality, www.省略
　　[9] Encounter Conformal ,www.省略
　　[10] SLEC, www.calypto
　　[11] B. Carrion Schafer and K. Wakabayashi, “Design Space Exploration Acceleration through Operation Clustering”, IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems （TCAD）, 29（1）, pp. 153-157