SystemC到AsmL：抽象验证方法

理论计算机科学电子笔记131（2005）39-49www.elsevier.com/locate/entcsSystemC到AsmL的抽象解释Ali Habibi1电气与计算机工程ConcordiaUniversity加拿大蒙特利尔Sofiene Tahar2电气与计算机工程ConcordiaUniversity加拿大蒙特利尔摘要SystemC是一组系统级设计语言，旨在提高嵌入式系统设计和验证的抽象级别然而，考虑到该库的面向对象性质及其仿真环境的复杂性，通过SystemC设计的模型检查或定理证明进行直接和可靠的验证我们说明了，在以前的工作中，执行模型检查和断言监视器生成SystemC使用的抽象状态机（ASM）语言（AsmL）的变体的可行性和成功在本文中，我们通过证明从SystemC到AsmL的转换的正确性来建立我们的方法的可靠性关键词：SystemC，形式验证，抽象解释。1介绍SystemC [11]是一种面向对象的系统级语言，用于嵌入式系统的设计和验证。期望在体系结构、软硬件协同设计和集成等方面取得更大的成就。的1电子邮件：habibi@ece.concordia.ca2电子邮件：tahar@ece.concordia.ca1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.01.02140A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）39SystemC库由一组类和一个扩展C++的仿真内核组成，使复杂系统的建模比最先进的HDL（硬件描述语言）更抽象。然而，除了小型模型，SystemC设计的验证是系统设计流程中的一个严重瓶颈。由于SystemC库及其模拟器的复杂性，直接对SystemC设计进行模型检查是不可行的。为了解决这个问题，我们在[4]中提出将SystemC模型转换为AsmL [8]中更适合形式验证的中间表示这种方法从根本上降低了设计的复杂性，我们能够使用SMV模型检查器验证复杂的PCI架构[12]。在本文中，我们基于[7]中给出的OO一般情况，在fixpoint中提供SystemC和AsmL语义的形式化。然后，我们证明，对于每一个SystemC程序，存在一个AsmL程序保持相同的属性，w.r.t.观测函数α。这种可靠性证明的基本概念是基于[2]中定义的程序转换框架的系统设计。这样的结果将使得能够使用各种正式工具（例如，SMV用于模型检查[12]）或使用AsmL工具（Asmlt）生成设计的有限状态机与我们相关的工作特别关注的是，定义SystemC和AsmL的形式语义。例如，已经使用了几种方法来编写SystemC语义（例如，使用ASM [9]）。指称语义[10]被发现是最有效的，因为对象可以表示为合适域上的定点。Salem在[13]中提出了SystemC的指称语义。然而，[13]中的建议非常肤浅，没有将整个SystemC程序的语义与其类的语义联系起来。因此，为了构造SystemC和AsmL之间的转换关系并证明其可靠性，本文定义了我们自己的SystemC指称语义。关于程序转换，Patrick和Radhia Cousot在[2]中的工作是任何使用抽象解释的程序转换的本质。使用语义将主题程序链接到转换后的程序的策略选择是非常聪明的，因为它能够证明与观察语义相关的转换的可靠性证明第3.9节中描述的通用方法的预测[2]中关于SystemC主体程序和AsmL转换程序的定义可以用来执行转换的可靠性，也可以用来构造它。在这两种情况下，我们都需要定义AsmL和SystemC的语法，语义和观察函数。本文的其余部分组织如下：第2节和第3A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）3941分别介绍了fixpoint中的SystemC和AsmL语义。 第4节包含SystemC到AsmL转换的存在性和可靠性的证明。最后，第五部分对本文进行了总结。2SystemC定点语义2.1句法域SystemC有大量的语法域。然而，它们都基于单个SC模块域。因此，一般SystemC程序的最小表示是一组模块。定义2.1（SystemC模块：SC模块）SystemC Module是一个集合DMem，Ports，Chan，Mth，SC Ctr，其中DMem是一组模块数据成员，Ports是一组端口，Chan是一组SystemC Chan，Mth是一组方法（函数）定义，SC Ctr是模块构造函数。定义2.2（SystemC端口：SC端口）SystemC Port是一个集合IF，N，SC In，SC Out，SC InOut，其中IF是一组虚拟方法声明，N是可以连接到端口的接口的数量，SC In是输入端口（仅提供读取方法），SC Out是输出端口（仅提供写入方法），SC InOut是输入/输出端口（提供读取和写入功能）。与面向对象语言的默认类构造函数相比，SystemC模块构造函数SC Ctr包含有关将在模拟期间执行的进程和线程的信息。定义2.3（SystemC构造函数：SC Ctr）SystemC Constructor是一个集合，其中Name是指定模块名称的字符串，Init是默认的类构造函数，SC Pr是一组进程，SC SSt是一组敏感性语句（用于设置进程敏感性列表SC SL）。定义2.4（SystemC过程： SC Pr）SystemC进程是一个集合PMth，PTh，PCTh，其中PMth是一个方法进程（定义为一个集合PMth，SC SL，包括方法及其敏感性列表），PTh是一个线程进程（与方法进程相比接受等待语句），PTh是一个时钟线程进程（对时钟事件敏感）。定义2.5（SystemC程序：SC Pg）SystemC程序是一个集合，其中LSC Mod是一个集合，42A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）39∅SystemC模块和SC main是程序中执行模拟器初始化并包含模块声明的主函数。2.2不动点语义在本节中，我们定义了整个SystemC程序的语义，WSystemC模块，MSC模块，MSC模块。然后，给出了MSC的可靠性和完备性的证明（或证明草图）。定义2.6（增量延迟：δd）SystemC模拟器考虑两个阶段评估和更新。这两个阶段之间的分离称为增量延迟。定义2.7（SystemC环境：SC环境）SystemC环境是[7]中定义的默认C++环境（Env）和SystemC特定的信号环境（Sig Store）的总和：SC Env=Env+Sig Env= [Var → Addr]+ [SC Sig →Addr，Addr]，其中Var是一组变量，SC Sig是一组SystemC信号，AddrCDN是一组地址。定义2.8（SystemC商店：SC商店）SystemC存储是[7]中定义的默认C++存储（存储）和信号存储（信号存储）的总和：SC存储=存储+信号存储= [Addr → Val]+ [（Addr，Addr）→（Val，Val）]，其中Val是使得SC Env等于Val的值的集合。设R0∈ P（SC Env×SC Store）是一组初始状态，pc_in是主函数sc_main的入口点，→ pc：（SC Env×SC Store）×（SC环境×SC存储）是一个转移关系。定义2.9（整个SystemC程序语义：WSCPg）设SC Pg =SC Mod，SC main是一个SystemC程序. 然后，SC Pg，W<$SCPg<$∈ P（SC Env×SC Store）→ P（T（SC Env× SC Store））的语义为：W<$SC Pg<$（R0）= lfp <$λX.（R0）{ρ0→ ... ρn→ρn+1|ρn+1∈（SC环境×SC商店）{ρ0→ ... ρn} ∈X <$ρn→ ρn+1}进程声明（PRSCPr）和SystemC模块构造函数（PCtrSC Ctr）的语义定义在[6]中给出。与[7]中OO对象的语义定义相反，SystemC方法可以 被由默认上下文或SystemC模拟器通过进程的敏感性列表激活。 的语义的完整定义SystemC模块对象（OSC模块对象）通过定义转换A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）3943n=0例∅J函数nextsc（σ）=next（σ）nextsig（σ），包括两个部分C++ re-在SystemC中，可以找到一些特殊的函数[6]。定理2.10设F =λT。S v，sl0ln−1ln...σσ|sc00→ →n→l0ln−1{σ...σ ∈T，next（σ）3 <$σJ，lJ <$}0→ →nscn则OSC<$o sc<$）（vsc，ssc）=<$ωFscn（n）证据[ 1 ] 中 的 定 点 定 理 是 直接证明的。Q定义2.11（SystemC模块语义： MSCmsc））设msc=m DMem，Ports，Chan，Mth，SC Ctr是SystemC模块，则其语义MSCmsc）∈ P（T（T））为：MSCm sc={OSCosc（vsc，ssc）|o sc是m sc的instance，v sc ∈Din，s sc ∈SC Store}定理2.12（fixpoint中的SystemC模块语义）设l0ln−1lJJGsc <$S <$= λT。{S 0 v，s v| v，s <$∈ S}<${σ0→. → σn→ σ|l0ln−1{σ...σ ∈T，next（σ）3 <$σJ，lJ <$}0→ →nscn则MSC<$msc<$（vsc，ssc）= lfp<$Gsc <$Din×Store证据虽然SystemC模型在C++之上提供了一些额外的功能，但该定理的证明与定理的证明类似3.2在[7]中。例如，考虑到MSC的定义并依次应用[6]中SystemC模块对象的定义，定理2.10和[1]中的定点定理，证明是简单的。QSystemC fixpoint语义的最后一步是关联模块语义到整个SystemC程序语义。因此，我们考虑在[ 7 ]中定义的函数abs tract（αt）的更新版本。对新功能进行了升级，使其支持SystemC仿真语义、仿真环境和仿真测试。 在[6]中可以找到α SC的简单定义。定理2.13（MSC的合理性）设MSC是一个全SystemC程序，且mSC∈ MSC. 然后R0∈ SC环境× SC存储。τ∈ T（SC环境× SC存储）。τ∈W<$SCPg<$（R0）：<$τJ∈MSC <$m SC<$. αSC（{τ}）={τJ}证据（ 草图）当 τ 包 含 一 个 物 体 时 ， 我们必须考虑这两种情况oSC，m个SC的实例化，以及当它不包括任何oSC时。 对于第二种情况，定理的证明是微不足道的，考虑到τ将是空的痕迹。 在第一种情况下，迹不是空的（设为τJJ）。以来44A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）39SystemC模块在仿真开始前在主程序sc main中初始化，存在初始环境、存储和变量它定义了初始迹σ0∈τJJ。τ jj中的其余迹线是在τ上应用α SC方法得到的σ SC的相互作用迹线。因此，τJJ∈MSC <$mSC<$。Q定理2.14（M SC模的完备性）设MSC是SystemC模.然后τ∈ T（τ）。τ∈MSC<$mSC<$：<$SC P ∈ <$L SC Pg <$。ρ0∈SC环境 ×SC商店。m SC的实例。存在τJ∈ T（SC环境× SC存储）.τJ∈W<$ρ0<$$>αSC<$（{τJ}）={τ}证据满足上述定理的SystemC程序可以通过在sc main函数中创建mSC的实例来构造，初始状态对应于模块的构造函数SC Ctr执行时的状态 SC的方法的执行对应于执行 方法线程（将其敏感性列表中的事件设置为活动），并且端口的改变对应于通过新值更新其内部信号因此，总是有可能同时构造SC P和ρ0。例如，存在涉及SystemC线程、时钟线程等的许多其他可能的构造。Q3AsmL不动点语义AsmL [8]是为ASM [3]开发的最新语言之一与C++或Java相比，它我们将限制本文中提出的AsmL语义的子集中使用的程序转换。3.1句法域定义3.1（AsmL类：AS C）一个AsmL类是一个集合AS DMem，AS Mth，AS Ctr，其中AS DMem是一组模块数据成员，AS Mth是一组方法（函数）定义，AS Ctr是模块构造函数。我们将在AsmL中使用的一个重要特性对应于方法的先决条件（在方法执行之前验证的布尔命题定义3.2（AsmL方法：AS Mth）AsmL方法是一个集合，其中AS M是一个A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）3945∅在该方法的核心中，AS Pre是一组前置条件，AS Pos是一组后置条件，AS Cst是一组约束。请注意，AS Pre、AS Pos和AS Cst共享相同的结构。它们在方法中通过为每个方法使用特定的关键字来区分（例如，先决条件）。定义3.3（AsmL程序：AS Pg）AsmL程序是一个集合，其中LAS C是一组AsmL类，INIT是程序中的主函数3.2不动点语义类似于SystemC的增量延迟（δd）的概念，AsmL考虑两个阶段：评估和更新。该程序将始终运行在eval- uate模式下有两种类型的更新，全部和部分（通常使用Step指令执行）。定义3.4（AsmL环境：AS Env）AsmL环境是一个修改过的面向对象环境AS Env= [Var → Addr，Addr]，其中Var是一组变量，AddrN是一组地址（两个地址存储v ∈ Var的当前值和新值）。定义3.5（AsmL商店：AS商店）AsmL存储是AS Store= [（Addr，Addr）-（Val，Val）]，其中Val是使得AS Env等于Val的值的集合。整个AsmL程序语义（WASPg语义）、方法语义（M AS Pg语义）、方法语义（M AS Pg语义）、方法语义（M AS Pg语义）和方法语义（MASP g 语义 ）。对象语义（OASoAS）通过定义一个在[5]中可以找到下一个转换函数（σ）。AsmL类构造函数可以根据[7]中的定义3.8定义。定义3.6（AsmL类语义：CAScas）设c as=dj as dj，as mth，as ctr是一个AsmL类，则它的语义CAScas）∈ P（T（））是：Casc as={OASoas（vas，sas）|o as是c as的instance，v as ∈Din，s as∈ SC Store}定理3.7（定点中的AsmL类语义）设l0ln−1lJJH表示为λ S λ = λT。 {S 0 v，s v| v，s <$∈ S}<${σ0→. → σn→ σ|l0ln−1{σ...σ ∈T，next（σ）3 <$σJ，lJ <$}0→ →n如n则CAScas（vas，sas）= lfpHasDin×Store46A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）39OOO证据 类似于定理2.12Q函数αAS是[7]中定义的函数绝对值（αA）的更新版本在[5]中给出了αAS的完整定义定理3.8（C AS的可靠性）设PAS是一个完整的SystemC程序，cSC∈ CSC. 然后R0∈ AS环境× AS存储。τ∈ T（AS环境× AS存储）。τ∈W<$ASPg<$（R0）：<$τJ∈CA S<$cAS<$. αAS（{τ}）={τJ}证据 类似于定理2.13。Q定理3.9（C AS的完备性）设CAS是SystemC模. 然后τ∈T（τ）。τ∈CSC <$cSC<$：<$AS P ∈ <$L AS Pg<$。ρ0∈AS Env×AS商店。c AS的实例。存在τJ∈ T（ASEnv×ASStore）.τJ∈W<$ρ0<$$>αAS<$（{τJ}）={τ}证据与我们在定理2.14中提出的类似的构造方法，不同之处在于，我们在这里考虑AsmL方法及其先决条件，而不是考虑SystemC方法线程和敏感性列表。这里也存在许多可能的构造，例如涉及AsmL后置条件。Q4程序变换源SystemC程序和目标AsmL程序之间关于观测值αo的行为等效性是确保AsmL水平上任何验证结果的可靠性所必需的。我们的目标是定义在特定delta周期中活动的SystemC进程与允许在AsmL模型中执行的方法集之间的关系。因此，我们将通过AsmL程序中的方法（方法核心，先决条件）映射SystemC程序中的每个线程（方法，敏感性列表），以确保两个程序中的变量集在同一时间更新相同的值。SystemC observation函数需要通过检查更新阶段的结束来查看增量周期开始定义4.1（SystemC观测函数：αSC）设SC_Pg=SC_L_SC_Mod，SC_main_M为SystemC程序，观测函数αSC∈ P（SC_Env×SC_Store）→ P（T（SC_Env× SC_Store））为αSCSCPg（R0）=A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）3947MMOOOOMMOlfpλX.（R0）<${ρ <$0 →. 蓬|<$ρ <$i∈（SC Env× SC Store）<${ρi→.ρi}100米∈X{m scin MSC|o sc ∈MSC。o sc（ρi（））{}}=}在前面的定义中，αSC仅跟踪仿真循环的初始状态。例如，第三个条件确认在最后一个仿真周期中没有单个进程准备运行。类似地，我们为AsmL程序定义了一个观测函数αAS定义4.2（AsmL观察函数：αAS）作为设AS Pg=A_LAS C，INIT_L为AsmL程序，观测函数α∈ P（AS Env×AS Store）→ P（T（AS Env× AS Store））是αASβAS Pgβ（R0）=lfpλX.（R0）<${ρ <$0 →. 蓬|<$ρ <$i∈（SC Env×AS Store）<${ρi→.ρi}100米∈X{m，如CAS中|o为∈CAS。o as（ρi（））/={}}=}接下来，我们定义两个观测值之间的等价性概念。虽然SystemC和AsmL具有不同的环境和存储结构，但可以确保它们包含相同的信息。定义4.3（相对于 αo：αo）设SC Pg为SystemC程序，Vsc为其变量集，AS Pg为AsmL程序，Dout为其输出变量集prog scoprog asifSC Pg的初始状态的集合。 AS的初始状态集Pg.0 0<$ρ<$∈{ρ<$0→ ...→ρ<$n}∈αSC<$SC Pg<$（RSC）.O0<$ρ<$∈{ρ<$0→ ...→ρ<$n}∈αA S<$ASPg<$（RA S）|O0vsc ∈ V sc。V是这样的，如果vsc∈SCSig则n（ρ（vsc）=（vl 1，vl 2））<$（ρ（vas）=（vl 1，vl 2））如果vsc∈ASDMm则n（ρ（vsc）=vl 1）<$（ρ（vas）=（vl 1，vl 1））观察函数确保AsmL程序模拟评估和更新阶段（ρ集的长度n第一个if条件负责SystemC信号，而第二个条件涉及基本的C++变量。定理4.4（变换的AsmL程序w.r.t. αSC）令SC Pg是一个完整的SystemC程序，SC Din是一组输入，SC Dout是一组输出。O48A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）39OO推杆然后ASPg，一个AsmL程序，这样SC Pg就可以代替AS Pg证据（略图）证明是通过构造AsmL程序完成的。例如，对于每个SystemC模块，我们都可以选择一个具有相同数据成员和方法的AsmL类。我们将AsmL方法的前置条件AS Ctr设置为SystemC程序进程的灵敏度列表SC SL中存在的事件状态的结合。构造中的棘手点是何时在AsmL程序中进行更新。我们有两种可能：（1）C++变量更新：每当指令中涉及C++变量时，可以使用AsmL中的绑定器的概念来应用部分更新;以及（2）SystemC信号：当所有方法先决条件为假时，所有信号都被更新。一旦定义了AsmL类的集合，定理3.9保证了AsmL程序的存在。Q定理4.5（变换的合理性）设SC Pg是一个完整的SystemC程序，AS Pg是一个完整的AsmL程序. 然后SCPgαo ASPg：Vsc，ρs|ρ∈αSC<$SCPg<$.SCPg Prop（Vsc，ρ）：ASPgProp（Vas，ρ）|ρ∈αA S<$ASPg<$.其中Prop是程序的属性，Vsc是SystemC程序的一组变量，Vas是AsmL程序中相应的变量。证据从定义4.3中等价关系的构造中，证明是直接的。Q5结论在本文中，我们介绍了SystemC库的定点语义，特别是我们证明是可靠和完整的SystemC模块的语义。SystemC程序的跟踪语义。我们还提供了一个子集的AsmL的语义，我们证明了一个AsmL类w.r.t.的可靠性和完整性。AsmL程序的跟踪语义。然后，我们证明了存在的，对于每一个SystemC程序，一个AsmL程序具有类似的行为w.r.t.一个观察函数，我们设置它来考虑系统在SystemC模拟器更新阶段之后的轨迹。我们使用SystemC到AsmL的转换来降低SystemC模型的复杂性，并使其能够进行形式化验证[4] 使用与AsmL和ASM语言一起使用的模型检查和定理证明方法A. Habibi，S.Tahar/Electronic Notes in Theoretical Computer Science 131（2005）3949引用[1] P. Cousot和R.库索程序分析框架的系统设计。在Symposium on Principles of ProgrammingLanguages，pages 269[2] P. Cousot和R.库索通过抽象解释的程序转换框架的系统设计。在Symposium on Principles ofProgramming Languages，第178- 190页[3] Y.古列维奇1993年：《大革命》。质量标准和验证方法，第9-36页。牛津大学出版社，1995年。[4] A. Habibi和S.塔哈尔设计用于验证SystemC事务级模型。在欧洲设计自动化和测试，慕尼黑，德国。[5] A. Habibi和S.塔哈尔AsmL定点语义。Concordia大学欧洲经委会系技术报告，2004年12月。[6] A. Habibi和S.塔哈尔SystemC定点语义。Concordia大学欧洲经委会系技术报告，2004年12月。[7] F.我的天AnalyyeStatiqueModulairdeLangagesa`2004年6月，法国巴黎理工学院[8] Microsoft Corp. AsmL for Microsoft .NET Framework，2004年。物件。博士论文，Ecole[9] W. Müller，J. Ruf和W。 玫瑰花。 系统C方法执行日志和A页。KluwerAcademic Pub.，2003年。[10] P. D. 苔藓指称语义学，理论计算机科学手册B卷，第11章，第575-631页Elsevier Science B.V.，1990年[11] 开放系统C倡议。 网址：http://www.systemc.org，2004年。[12] K. Oumalou，A.Habibi和S.塔哈尔 在SystemC中验证PCI总线的设计在2004年11月在芬兰举行的片上系统研讨会。[13] A.塞勒姆同步SystemC的形式语义。在欧洲设计、自动化和测试会议上，第376-381页