基于切片的软硬件协同设计方法及其实用性研究

理论计算机科学电子笔记159（2006）265-280www.elsevier.com/locate/entcs基于切片的软硬件协同设计方法佐佐木俊介1东京大学大学院工学研究科电子工学科2-11-16 Yayoi，Bunkyo-ku，东京都，日本Masahiro Fujita3东京大学VLSI设计教育中心2-11-16弥生，文京区，东京，日本摘要程序切片是一种软件分析技术，它生成系统依赖图（SDG），通过SDG可以识别程序语句之间的依赖关系。在本文中，我们提出了一种新的软硬件协同设计方法的基础上的静态和部分动态依赖分析SDG。我们从C，C++和SpecC描述的任何组合开始，以便可以对硬件/软件系统进行灵活的功能规范。首先，对输入描述进行分析，并使用从输入描述生成的SDG进行验证。实际的分析和验证是基于静态的，但也有一部分动态的，可以处理相当大的描述。在这些分析之后，我们通过优化设计描述和在必要时引入并行性将系统分为硬件和软件部分。在此HW/SW划分中，充分利用从C / C++ / SpecC设计描述生成的SDG从整个描述中提取/转换/打包HW部分。这种硬件/软件划分的灵活性是与以前的硬件/软件划分方法的主要区别之一。 提取的硬件部分进一步优化，然后转换为RTL描述现有的行为合成工具。作为最后一步，将生成的RTL描述与SW部分一起与原始描述进行比较，以确保它们在逻辑上等效。此外，设计师指定的属性可以使用这些最终设计描述进行模型检查。这些等价性检查和模型检查可以通过首先将硬件/软件设计描述转换为FSM类型表示来实现。翻译后的FSM类型表示由现有的形式验证器进一步处理。我们提出了建议的硬件/软件协同设计方法与一个说明性的例子，以及实际应用到真正的设计，并证明我们的方法的实用性。关键词：程序分析，系统依赖图，程序切片，系统级设计，软硬件协同设计1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.071266S. Sasaki等人/理论计算机科学电子笔记159（2006）2651引言由于超大规模集成电路和片上系统（SoC）技术的进步，芯片制造的复杂性正在迅速增长。然而，SoC设计的设计和验证并没有赶上如此快速的增长。这使得生产和设计/验证之间的效率差距变得更大，这是当今SoC设计中的一个关键问题迫切需要新的设计方法，使设计和验证过程更具生产力提高设计效率最有效的方法之一是从更高层次的设计抽象中最近，已经提出了几种支持IP重用的系统级设计（硬件/软件协同设计）语言，例如SpecC [3]或SystemC [4在系统级设计中，不仅要考虑硬件的开发，还要考虑软件的开发。在软件开发领域，程序切片技术是一种在整个程序代码中提取目标变量或语句的依赖关系的技术[11]。切片技术在软件开发的分析、维护、调试、测试和重用等方面都有很好的应用在硬件和系统级设计领域，SpecC的程序切片工具已由Tanabe [6]提出该工具使用商用ANSI-C/ C++的程序切片工具，可以处理ANSI-C、C++和SpecC代码的任意组合。本文提出了一种基于C / C++ / SpecC程序切片工具的方法。 在设计过程的每一步，我们使用切片工具构造的系统依赖图（SDG）来分析语句之间的依赖关系。SDG也用于引入并行性，因为扩展切片工具[6]也可以表示并发进程中变量之间的所有依赖关系因此，SDGs不仅可以实现设计分析，而且可以实现设计优化本文的其余部分组织如下。第二节介绍了程序切片、等价性检验和模型检验的背景知识在第3节中，我们提出了使用SDG的协同设计方法。在第4节中，我们展示了如何将这种方法应用于硬件/软件协同，1电子邮件：shun@cad.t.u-to ky o.a c。JP2电子邮件：tasuku@cad.t.u-tokyo.ac.jp3电子邮件：fujita@ee.t.u-tokyo.ac.jpS. Sasaki等人/理论计算机科学电子笔记159（2006）265267MPEG2编码器和JPEG2000编码器的设计，并证明了我们的方法的有效性。2背景2.1程序切片程序切片是一种提取原始程序中与用户指定的某些语句中的变量相关的部分的技术。最初，程序切片是由Weiser在[11]中提出的在[11]中，切片是用给定的两个参数计算的，程序点p和出现在p中的变量集v。他通过使用控制流图（CFG）为过程和过程调用开发了一种程序切片方法后来，Otten-stein和Ottern [8]提出了一种基于依赖图的新方法他们从一个给定的程序中构造了一个依赖图，并通过跟踪图中的数据和控制依赖边，从用户给出的变量v中识别出切片代码在该算法中，切片的计算时间随着依赖图中节点的数目线性增加此外，Horwitz [5]等人定义了系统依赖图（SDG），它包含多个过程依赖图（PDG）并表示过程之间的依赖关系为了获得更精确的切片结果，他们开发了一种新的遍历方法，该方法包含SDG上的两个阶段遍历。基于使用SDG的工作，提出了几种程序切片方法，包括面向对象程序的切片[7]和具有多线程的JAVA程序基本上，程序切片分为两种类型：向后切片和向前切片。给定一个程序点p和一组出现在p中的变量v，后向切片提取程序的所有部分，v. 另一方面，前向切片提取程序中由v表示的所有部分。基于这些基本的切片操作，用于调试和分析程序。例如，斩波是一种切片操作，它计算前向切片和后向切片的乘积当给定程序点p中的一组变量v作为起始点和pJ中的另一组变量vJ作为结束点时，斩波提取所有的部分，这些部分是v和vJ的集合。例如，对于ANSI-C和C++语言，GrammaTech Inc.提供了一个商业工具CodeSurfer[1]关于系统级描述语言的切片，Tanabe等人开发了SpecC语言的切片工具[6]。他们提出了如何表示SpecC描述，包括行为、通道和接口等层次结构，并行执行语法如par和同步268S. Sasaki等人/理论计算机科学电子笔记159（2006）265语法为wait和notify，作为其SDG，并通过使用Codesurfer将原始SpecC描述转换为C++描述在我们的方法中，我们使用这个工具来分析C / C++ /SpecC描述的组合。2.2正式验证形式验证是使用基于数学的技术的形式方法证明或反驳系统关于特定形式规范或属性的正确性的行为。形式验证技术可以分为模型检查（属性检查）和等价性检查。模型检测是一种算法验证模型的方法，通常来自硬件或软件设计。这是通过检查模型是否满足逻辑规范（属性）来实现的。该属性通常被写成时态逻辑公式。等效性检查验证处于相同或不同抽象级别的两个设计的功能等效性。高级硬件描述或系统级描述的正式验证方法[10]是一种模型检查方法，用于验证并发SpecC描述，包括同步。 目标属性是同步属性，如死锁。[9]给出了一种基于符号模拟的等价性检验方法。符号模拟是硬件验证中最常见的技术之一，它将描述中的变量视为符号而不是位向量。RTL描述的形式化验证方法是成熟的技术，因此有许多商业软件。3我们的方法图1显示了我们的方法的概述该方法的输入是C、C++和SpecC描述的任意组合，因此设计人员可以以更灵活的方式对硬件/软件系统进行功能规范作为第一步，可以使用从输入描述生成的SDG分析和验证输入描述我们在第3.1小节中给出了有关此步骤的详细信息。如果设计通过第一步，我们通过优化设计描述并在必要时引入并行性将系统分为硬件详情见第3.2小节。S. Sasaki等人/理论计算机科学电子笔记159（2006）265269Fig. 1. 我们的方法概述。作为最后一步，将划分和合成的硬件部分与软件部分与原始描述进行比较，以检查逻辑等效性。此外，设计者指定的属性可以由模型检查器使用这些最终描述进行检查。详情见第3.3小节。3.1静态程序检查首先，我们从输入的设计描述中生成SDG，以分析和验证它们。在本小节中，我们将展示两种静态程序检查方法。当然，也可以使用其他模型检查工具或其他各种检查算法。检测未使用的变量/未使用的语句通常，设计说明中的每一句话都应该对270S. Sasaki等人/理论计算机科学电子笔记159（2006）2651234567891011121314151617181920图二. 源代码示例：检测未使用的变量。图三. 示例源代码的SDG：检测未使用的变量（1）。一些产出。如果有一些语句对输出没有影响，则设计描述可能存在很大可能性的错误。为了检测这样的语句，可以使用后向切片算法如下。计算每个输出语句的后向切片之和，所有未被此步骤选中的节点在输出上没有结果，因此这些节点表示未使用的语句。图2显示了一个包含未使用变量“sz0”和“sz1”的示例源代码，图3显示了从它生成的SDG。为了简单起见，控制依赖边、声明节点和声明边都被缩写了。此示例设计具有输出端口在SpecC语言中，输入行为主体（int x，int y，void main（void）{inta0=2，a1=4;int sx，sy;int sx0，sx1，sy0，sy1;intsz 0，sz 1; /* 未使用*/sx 0 =a0* x 0;sx1=a1*x1;sz 0 =a1* x 0; /* 未使用*/ sx = sx 0 + sx 1sy0=a0*y0;sy1=a1*y1;sz 1 =a0*y1; /* 未使用 */sy = sy 0 + sy 1;z =sx+sy;}}S. Sasaki等人/理论计算机科学电子笔记159（2006）265271图四、示例源代码的SDG：检测未使用的变量（2）。并且输出在行为的参数中被清楚地指示并且容易指定它们。图4显示了从原始源代码第4行中的“out int z”向后切片的结果未被后向切片选择的节点表示未使用的语句。(In图4，声明节点检测未初始化变量当多个线程并行运行时，有许多执行顺序如果一个变量在一个线程上初始化，而该变量在另一个并行运行的线程上使用，则该变量可以在某些执行顺序中在初始化之前使用。这是多个线程并行运行时的典型错误图5示出了用SDG检测这些变量的算法图6和图7显示了该算法的一个示例。例如，我们展示了如何检查节点(i) 此节点使用变量(ii) 检查“sx0”是否(a) 从“sx = sx 0 + sx 1”开始向后遍历数据依赖边，并(b) 检查“sx 0 = a0*x0”是否* x0”和“sx = sx 0 + sx 1”来寻找公共节点找到了两个“par”节点，但它们不是正确的。找到入口节点“sx272S. Sasaki等人/理论计算机科学电子笔记159（2006）265N1、N2、N： SDG中的节点V： SDG中的变量foreach N1 in assignment nodes{ foreach V in variables used in N1 {对于每个N2在分配节点，使得（（N2是从N1可达的，只有数据依赖边缘），（V在N2处初始化））{如果存在N，使得（（N不是(N1仅通过控制依赖边从N可达）和(N2仅在控制依赖边的情况下不传递控制节点））{//N1处的变量V在下一个V的N2}}显示警告信息}}图五. 未初始化变量检查算法的伪代码。1234567891011121314151617181920212223见图6。 一个示例源代码：使用未初始化的变量.边缘“sx0 = a0 * x0” is NOT reachable from “main()” without passing“par” control行为主体（int x，int y，void main（void）{inta0=2，a1=4;int sx，sy;int sx0，sx1，sy0，sy1; par{par{sx0=a0*x0;sx1=a1*x1;sx =sx0+sx1}par{sy0=a0*y0;sy1=a1*y1;sy =sy0+sy1;}}z =sx+sy;}}S. Sasaki等人/理论计算机科学电子笔记159（2006）265273图7.第一次会议。示例源代码的SDG：使用未初始化的变量。因此，不能保证“sx 0 = a0 * x0”在“sx”= sx0 + sx1(c) “sx0” is found not to be guaranteed to be(iii) 其中一个变量被发现不能保证被初始化，因此其他变量不需要被检查。在本小节中，我们展示了两个静态检查算法。也可以使用其他模型检查算法或等价性检查算法。3.2硬件/软件划分和优化在对输入描述进行静态检查之后，进行了具有并行性的硬件/软件划分用SDG提取了相似性。当一个节点和另一个节点不相互依赖时，它们可以并行执行例如，在图3的SDG中，可以并行执行四个语句“sx 〇 = a0 * x0”、“sxl =al * xl”、“sy0 = a0 * y0”和“syl = al * yl”，并且也可以并行执行两个语句“sx= sx 〇 + sxl”和“sy = sy0 + syl”。（省略第3.1节中发现的未使用语句。）在此之后，硬件/软件划分是在提取的并行性的基础上完成的。如果希望并行执行两个可以并行执行的语句，则将其中一个分配给SW，另一个分配给HW，或者两者都分配给HW。图8是划分的示例，图9是基于原始描述和图8的HW/SW划分描述。274S. Sasaki等人/理论计算机科学电子笔记159（2006）265见图8。 示例源代码的SDG：硬件/软件分区。这种硬件描述可以进一步优化，并将通过现有的行为综合工具转换为RTL描述3.3使用FSM进行在硬件行为综合之后，必须检查过程是否已经完全完成，换句话说，我们必须确保原始描述和硬件综合之后的描述在逻辑上是等价的。此外，设计人员可能希望静态验证这些最终设计描述。因此，我们提出了与原始设计描述和最终描述进行等价性检查的方法，以及与最终描述进行模型检查的方法。最后一个在两点上与原来的不同。最终的硬件部分和软件部分在不同的级别（如内存级和RTL）进行描述，它们通过内存映射I/O或中断驱动I/O进行通信我们通过将硬件/软件描述转换为通信抽象的有限状态机来解决这些问题。有两个原因将它们转换为FSM。首先，有限状态机模型其次，硬件描述通常用RTL编写，RTL与FSM处于同一级别通过用状态变量标识寄存器，RTL描述可以很容易地转换为FSM。 这里，我们将验证目标限制为硬件部件和软件部件通过内存映射I/O进行通信的设计。由我们的方法生成的接口在硬件部分和软件部分都有相应的变量。在存储器映射I/O中，HW寄存器被分配给SW地址空间中的特定地址，并且HW寄存器和SW地址之间的对应关系是已知的。S. Sasaki等人/理论计算机科学电子笔记159（2006）26527512345678910111213141516171819202122232425262728293031323334353637383940414243444546见图9。 一个示例源代码：硬件/软件分区后。通过指针访问软件中的地址图. 10显示了我们正式验证的流程首先，将最终设计中的软件描述转换为FSM，如图左侧所示。十一岁此示例是图的软件部分。9 .第九条。SW描述被转换成仅由赋值、“if”和“while”语句组成的描述也就是说，用变量替换局部指针，用“while”语句替换行为主体（int x，int y，int a0=2，a1=4;bool hw_start，hw_end;Main_SW sw（a0，a1，x0，x1，y0，y1，z，sx，hw_start，hw_end）; Main_HW hw（a0，x0，a1，x1，sx，hw_start，hw_end）;void main（void）{ par{sw.main（）;return（）;}}};01 - 02 - 2016刘晓波（int a0，int x0，int a1，int x1，publicint findDuplicate（int findDuplicate，int findDuplicate）{void main（void）{ intsx0，sx1;while（！start）;par{sx0=a0*x0;sx1=a1*x1;}sx= sx 0 +sx 1;end=1;}};01 - 02 - 03张晓波（int x0，intx1，inty0，inty1，intsx）{void main（void）{ hw_start=1; sy0=a0*y0;sy1=a1*y1;sy =sy0+sy2;同时（！hw_end）;z=sx+sy;}};276S. Sasaki等人/理论计算机科学电子笔记159（2006）265系统级描述等价性验证在硬件/软件划分和硬件行为综合见图10。 使用FSM进行main（）{hw_start=1jsyO=aO*yOjsy1=a1*y1jsy=syO+sy1jwhile（！hw_end）jz=s×+syj}开始开始hw_start START硬件端hw_start=1s×端SXSTART=1syO=aO*yO syO=aO*yOsy1=a1*y1hw_end！=Osy= sy0 +sy1结束！= Osy1=a1*y1hw_end==1Jsy= sy0+sy1END==OJhw_end！= O hw_end==1 END！=O END==Oz=s×+sy z=SX+sy端端开始！=O开始START==OJ开始！= OSTART==OSXO=AO*XOSX1=A1*X1SX=SXO+SX1END=1CSWFSMSW FSM将指针替换为硬件资源硬件FSM见图11。 从C到FSM的在，已经完成。之后，描述被转换为FSM，作为对一个状态的一个赋值“if”和“while”状态中的条件表达式另外，指向分配HW寄存器的地址的指针被相应的单独HW寄存器替换。接下来，最终设计中的硬件描述被转换为FSM。如前所述，通过用状态变量标识寄存器，可以很容易地将RTL描述转换为FSM此时，将来自总线的数据分配给与SW地址对应的寄存器的HW的一部分与整个HW分离分离的部分可以独立验证，因为它它通常很小，很容易被验证。如果它已经被提前验证，那么通过内存映射I/O的通信是有保证的。图右侧显示了硬件FSM的示例。十一岁此示例是图的硬件部分。9 .第九条。系统（C/C++/系统（FSM系统（顺序FSM）系统（顺序FSM）SW（软件（FS硬件+软件硬件+软件（顺序硬件（RT硬件（FS硬件+软件（顺序硬件部分（RT验证模型检查◼◼◼◼◼◼S. Sasaki等人/理论计算机科学电子笔记159（2006）265277开始开始s×O=aO*×Os×1=a1*×1syO=aO*yOsy1=a1*y1s×=s×O+s×1sy=syO+sy1Z=s×+syend从原始描述START=1START！=OSTART==OJ开始！= OSTART==OSXO=AO*XOSX1=A1*X1sy0 = a0 * y0sy1=a1*y1SX=SXO+SX1sy= sy0 +sy1END=1END！=OEND==OJ结束！= OEND==OZ=SX+sy端从并发FSM转换的硬件+软件顺序FSM见图12。 最终步骤因此，HW/SW描述被转换为通过HW寄存器作为共享变量进行通信的并发此外，我们整理并发FSM的可执行命令。我们不必考虑在没有转换的时间段内的所有订单，因此我们可以将并发FSM转换为实际数量的顺序FSM。此外，我们可以合并赋值语句之间没有依赖关系。生成的FSM并不复杂，因为这些基本上是顺序的。而且，合并状态后，它们中的状态数也没有那么大。这些可以在用模型检查器的输入语言（如Verilog）描述后，用现有的模型检查器进行形式化验证图中显示了一个示例12个。右边的四个FSM来自图。十一岁所有这些都应该进行模型检查。只有全部通过检查，才能保证设计的正确性。需要额外的翻译来与原始设计描述和最终描述进行等效性检查原始描述以与前面提到的C-to-FSM转换方法相同的方式转换为FSM。图中最左边的FSM。12是图中的例子。六、现在，这些问题已经被简化为在同一表示中描述的两个不同设计的等价性检查。必须对两个设计的FSM的所有对进行等效性检查。在图的例子12、必须进行四次等价性检查。如果每次检查都是一个接一个地进行，可能效率不高，而且可能非常耗时。在那里，最好用[9]中所示的技术来象征性地模拟它们虽然这个方法是针对C开始开始开始开始！= O START==O START！=O START==Oj START=1START=1开始！= OSTART==OJj START=1开始！= OSTART==OSXO=AO*XOSX1=A1*X1sy0 = a0* y0开始！= OSTART==OSXO=AO*XOSX1=A1*X1sy0 = a0* y0开始！= OSTART==OSXO=AO*XOSX1=A1*X1sy0 = a0* y0SX=SXO+SX1sy= sy0 +sy1END=1END！=OEND==OJSX=SXO+SX1sy= sy0 +sy1结束！= OEND==OSX=SXO+SX1sy= sy0 +sy1结束！= OEND==OJ结束=1J结束=1结束！= 结束了！结束了！结束了！结束了！O END==OZ=SX+sy Z=SX+sy Z=SX+sy端端端278S. Sasaki等人/理论计算机科学电子笔记159（2006）265语言，类似的工具可以开发并用于FSM。4为例在本节中，我们将展示如何将这种方法应用于MPEG 2编码器和JPEG 2000编码器的硬件/软件协同设计，以证明我们的方法的有用性4.1MPEG2我们使用MPEG2编码器的源代码作为原始输入描述。它是用C语言编写的，有7600行。首先，我们将IDCT函数从原始数据源中分离出来。这可以使用斩波（从函数Fast IDCT（）的输出进行后向切片，从函数Fast IDCT（）的输入进行前向切片）来完成。结果代码有200行。将IDCT函数与其它部分分离后，对源代码进行了静态检查。生成SDG需要0.4秒，检测未初始化变量的使用需要0.7因为这段代码没有未使用的变量，所以这个未使用的变量检查的结果不包含任何语句。然后，考虑到并行性，将系统划分为硬件部分和软件部分。在这个设计中，有两个for循环，我们需要展开它来检查循环迭代之间的依赖关系每个循环有8次迭代。使用3.2节中提出的方法，很在划分之后，硬件部分被编译成RTL verilog描述。虽然这可以用现有的行为合成工具来完成，但我们已经手工完成了作为最后一步，硬件的RTL描述和软件部分的C描述我们使用具有“计算成功完成”属性的模型检查器（Solidify [2]）验证了此设计。花了715秒，设计被证明是正确的。4.2JPEG2000我们使用libj2k的源代码作为原始输入描述。它是用C语言编写的，有4300行。S. Sasaki等人/理论计算机科学电子笔记159（2006）265279123456图十三. 虚假警告的例子首先，原始源包括解码器和编码器，因此我们将编码器代码与其他部分分开。这可以使用斩波（从函数j2k encoder（）的输出进行后向切片，从函数j2k encoder（）的输入进行前向切片）来完成结果代码有2500行。在将编码器与其他部分分离后，我们对源代码进行了静态检查生成SDG需要0.6秒，检测未初始化变量的使用需要0.5秒，检测未使用的语句需要0.5秒当检测到使用未初始化的变量时，会报告许多看似已初始化我们正在解决这些错误警告的问题。这个问题的一个原因是切片工具不解释控制节点的条件，例如“if（）"、“switch（）"等。图13示出了一个变量然后，考虑到并行性，将系统划分为硬件部分和软件部分。在本设计中，我们决定用硬件来处理离散小波变换（DWT），其余的用软件来处理。小波变换包含三重折叠循环，这可以与现有的方法并行化。我们可以使用SDG来确定哪些语句是可转置的，并且它可以是现有并行化方法的预处理。划分后，硬件部分，处理DWT，编译与现有的行为合成工具，产生RTL描述。5结论提出了一种基于程序切片技术的软硬件协同设计方法。我们用一个小的示例代码和一个MPEG 2编码器和一个JPEG2000编码器的案例研究展示了这种方法的流程。该方法具有可处理大型设计、可提取并行性和高度可扩展性、可采用多种验证方法验证设计等优点确认作者感谢匿名评审的宝贵意见。public void run（）{return 0;}否则{a=1;}b=a;280S. Sasaki等人/理论计算机科学电子笔记159（2006）265引用[1] CodeSurfer http://www.grammatech.com/products/codesurfer/网站。[2] 固化。 http://www.averant.com/products.htm网站。[3] SpecC. http://www.cecs.uci.edu/.cnspec/.[4] 系统C。http://www.systemc.org/网站。[5] 苏珊·霍维茨，托马斯·雷普斯，大卫·宾克利.使用依赖图的过程间切片。第12卷第26ACM Press，1990.[6] K.田边，S. Sasaki和M. 藤田 SpecC中系统级设计的程序切片。 在Proc. of the IASTED，International Conference on Advances in Computer Science and Technology，pages 252-258，Nov. 2004年[7] 洛伦·拉森和玛丽·简·哈罗德面向对象软件的切片。第18届国际软件工程会议，第495IEEE计算机学会，1996年。[8] 作者声明：Karl J.奥特曼软件开发环境中的程序依赖图。在第一届ACM SIGSOFT/SIGPLAN软件工程研讨会上，实用软件开发环境，第177-184页。ACM Press，1984.[9] T.松本，H。Saito和M.藤田一种基于符号模拟与文本区分的C语言描述等价性检验方法。IASTEDInternational Conference on Advances in Computer Science and Technology，第246-251页，11月11日2004年[10] T. Sakunkonchak，S. Komatsu和M.藤田用区别判定图验证规范描述中的同步性。IEICE Trans.Fundamentals，E86- A（12）：3192-3199，Dec. 2003年。[11] M. 威瑟程序切片。IEEE软件工程学报，10（4）：352