TXP语言：一种用于硬件系统验证的新型时态属性规范语言

网址：http://www.elsevie r. n l/l oc ate/en tcs/vol um e55. ht ml 13页Dynamic Assertions UsingTXPSurrendraDudani1Jo~aoGeada1GrzegorzJakacki1丹尼尔·维纳1摘要本文提出了一种新的时态属性规范语言TXP。该语言旨在支持在仿真运行时对时态属性的动态监视，并为形式化属性检查提供输入规范。对于硬件系统的设计验证，硬件描述语言（HDL）提供了建模能力，但对于逻辑关系涉及多周期约束的复杂断言的简洁规范，HDL是不够的。 TXP是一种声明性语言，它基于值和事件序列上的正则表达式提供了一组丰富的运算符。它的主要特性是允许多周期行为、过去或未来的时移操作、条件匹配、序列重复和序列限制。序列可以用逻辑连接词（如“and”和“or”）构造，以组成更复杂的断言。 一个TXP引擎已经开发出来，以监测的性质在运行时。1引言Synopsys公司开发了一种新的时态属性描述语言TXP2.使用这种语言，用户可以编写断言来验证硬件系统的性能在仿真过程中在运行时，或提供这些断言正式或半正式的验证工具进行静态检查。许多基于时序逻辑的规范语言[1，2]已经被提出用于形式化方法，如模型检查和定理证明，但它们被硬件设计者采用的速度很慢。TXP是以硬件设计为主要应用程序开发的，它通过提供使用硬件设计人员熟悉的概念的构造来解决可用性问题。TXP语言提供了一种方法来准确和有效地描述跨越多个周期和被测设计模块的控制行为。对于硬件开发人员来说，与时序和顺序相关的功能问题很难检测到，而且对x来说代价最高1 Synopsys公司2 TXP是OpenVera的一部分，并已由Synopsys公司作为Vera开源计划的一部分提供。c 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2延迟和成本超支。常用的HDL（如Verilog [4]和VHDL [5]）被设计为在寄存器传输级（RTL）（即单周期转换）上对硬件进行显然，这样的执行模型不足以简明地指定多周期函数。有人可能会说HDL是设计语言，而不是规范语言，因此需要一种新的规范方法，特别是考虑到设计规模和复杂性的增加。使用一种规范化的方法来简单直观地表达被测设计的输入/输出行为、总线协议和其他复杂关系，可以开发一种非常有效的动态监控系统，以在验证过程中检测故障行为。TXP语言是一种声明性语言，其语义基于正则表达式[3]。已经有一些建议扩展时态逻辑[6]以提供正则表达式的表达能力。TXP建立在这些概念的基础上，为硬件设计人员提供了直观的语法基于正则表达式的语言的决定有两个方面：第一，正则表达式不能很好地与硬件设计者所理解的排序操作相结合;第二，正则语言可以很容易地转换为一个nite状态模型，可以由形式化方法用来执行形式化的属性检查。也有一些历史的工作时间逻辑指定的属性的软件系统。在[7]中描述的Bandera项目已经开发了一个用于JAVA语言的系统，其中可以指定常见的时态属性。这些属性在代码中是位置相关的，当程序执行到达一个控制点时显示红色TXP规格允许用户表达以下测序特征：用于指定一个事件跟随另一个事件的基本序列构造过去或未来的序列使用逻辑连接词（and，or，inv）的复合序列序列的重复在序列期间保持的条件时间有界序列用户指定的时钟或模拟时间作为采样时间单位在第二节中，我们描述了TXP的理论基础和定义语言的形式语义结构。第3节显示了运行时验证环境，并解释了仿真模型。在第四节中，我们描述了语言的特点和一些例子来说明语言结构的使用。最后，第5节总结了当前的工作，并概述了未来的工作。32理论基础这一部分描述了TXP语义发展的理论基础。第2.1节描述了在标准正则表达式上定义的运算符。第2.2节进一步构造了运算符的否定的定义。每个TXP构造的语义稍后根据本节中描述的定义来定义。2.1正则表达式的定义我们处理时间序列（t序列）的字母表的估值。估价是对设计在特定时刻的状态的完整描述对于序列代数的标准签名，我们添加一个运算符[。 新代数VTSeq的载体是Val？Nat其中Val是设计估值的集合，Nat是自然数的集合。在t序列（v; n; m）中，n和m表示t序列的“虚拟开始”和“虚拟结束”相对于v的开始的位置“=（“; 0; 0）（u;n0;n00）[=（u;n0;n0）的解释0 00 0 00（u; n ;n） （v; m ;m）定义为（w;n0+i;m0 0 +j）如果w是最短序列，则满足（1）u是w在位置i的子序列，（2）v是w在位置j的子序列，（3）n00+i=m0+j.如果不存在suchi，j，w，则不进行级联。注意，连接的解释是一个部分函数。 形式为（v; 0; jvj）的t-序列称为非扩张的。注意，所有非扩展t-序列的子代数同构于序列的标准代数。时态正则语言（t-languages）的代数VTReg是建立在t-序列的代数之上的。 对于正则语言代数的标准签名，我们添加运算符[，\， rst、cst和neg。载波是t-序列代数的载波的幂集解释定义为U[=fu[：u2U gU\V=（（U？）\V）[（U\（V？））我们说，t语言U是非扩张的，i U中的所有序列都是非扩张的。注意，所有非扩展t-语言的子代数与正则语言的标准代数同构其余的操作仅为非扩展参数定义。让我们假设NExtend，其中NExtend表示所有非扩展t序列的集合另外40？我们将写hei来表示所有t序列（[v]; 0; 1）的集合，使得Verilog表达式e在赋值v中求值为真rst U=fu2U：8u0 2N扩展：u0 6=“）（uu0）2=UgU=fu0 2N扩展：9u00 2N扩展：u=u0u00gU=fu0 2N扩展：u0 2=Ugneg U=rst（U）\U2.2显式失效在本节中，我们将展示如何在具有显式失败的赋值上构造时态正则表达式的代数VTFReg。其载波的元素被定义为对，为了方便起见，我们将其写为比率：U（U; U）=U0其中，\numerator”表示断言成功，而\denomi- nator”表示失败。该代数的签名和运算根据VTReg中的运算定义如下：UVU0V0U[VU0V0U V=U0[（U V0）U[ V=U0\V0U V\U0V0“U\V=U0[V0“= ;为 ;;=;什么？hei= e对于e 2 V exp：e你你？=U0;UVW（U V）[（（negU）W）如果U0下第0页其他W0 =（U V0）[（（negU）W0）UU0inv=U0UU VV\U？5使进入U0V0=V0[（（U？U0）\V）如果U和U0 仅包含（[v]; 0; 1）形式的序列;否则不包含UrstU0首次使用= 第一个U06设计源TXP源Verilog编译器公司简介仿真模型PLITXP发动机透镜U[n：：m]U0UU\[n：：m]=U0\[n：：m];如果U\[n：：m]6=;[n：：m]len[n：：m]U0 =（U0 \[n：：m]）[m如果U\=;以代数载体VTFReg作为形式化的语义域TXP语义的定义。3运行时环境虽然TXP可以支持任何HDL，我们将描述Verilog HDL的运行时环境。Verilog是一种事件驱动的语言，许多硬件设计人员使用它来模拟他们的系统，以便使用仿真进行设计和验证。为了模拟设计，用户编写Verilog描述和编译来生成用于模拟的模型为了编写使用来自仿真的运行时信息的应用程序代码，Verilog提供了一个称为编程语言接口（PLI）的软件接口。Fig. 1. TXP运行环境如图1所示，TXP规范是单独编译的，并提供给TXP监控引擎。TXP运行时引擎使用编程语言接口（PLI）3与Verilog仿真交互，主要是为了获得设计变量信息，例如值，并在值更改时获得通知。当模拟运行时，TXP监视并跟踪TXP le中描述的断言的状态。 当检测到断言失败时，报告提供调试信息，该调试信息报告断言的开始时间和检测到失败的时间。4语言基础本节解释了该语言的基础知识。该描述包括时序模型、序列匹配、断言、时移操作以及3 虽然原型实现使用PLI接口，但有更有效的方式与模拟器交互，如VPI和直接内核接口。7序列的构建4.1定时模型和事件TXP中采用的时序模型基于时钟周期（cycle），并使用时钟周期的广义概念。时钟滴答是一个原子时刻，意味着时钟滴答中没有持续时间。表达式中的变量在时钟滴答时的值是在该时刻精确采样的。采样值是时钟周期内变量的唯一有效值。时钟的定义由用户明确指定，并且可以从一个表达式到另一个表达式而变化。此外，用户可以选择使用模拟时间作为表示异步事件的时钟。时间表达式总是与时钟定义联系在一起。表达式中涉及的变量值仅在时钟刻度处采样。这些值用于评估事件或逻辑子表达式，这些事件或逻辑子表达式是确定与时间表达式的匹配所必需时钟滴答处的事件被定义为表达式的值相对于该表达式在前一时钟滴答处的值例如，当一个信号的值从低变高（上升沿）时，它被认为是一个事件。如果事件发生，则事件的计算结果为true，如果事件未发生，则为false。4.2匹配A序列由时间表达式描述的序列由检查点组成，从评估时间的开始到结束在时间上分散。检查点是对逻辑表达式或事件的评估，导致真/假值。通常，序列被写为一系列检查点，其中检查点后面跟着下一个检查点。为了确定序列的匹配，在适当的时间评估检查点以满足表达式。如果所有的检查点都满足，则称发生序列匹配。在每个时钟周期都尝试断言，以查看它是否被违反。 测试在时钟节拍的断言中，独立于在先前时钟节拍的任何尝试，执行对表达式的新的求值尝试。每次尝试的结果也分别报告。当表达式计算分支以计算构造所隐含的所有替代序列时，会出现更复杂的情况。在这种情况下，每个序列的匹配都是相互独立的。表达式可能导致多个匹配或匹配失败。 如果这样的时间表达式是更大表达式的子表达式，则结果匹配用于确定封闭表达式的匹配。8实施例4.1e1 #[1.. 3]（ack==0）该语句表示在时钟节拍1、2或3发生事件e1之后，信号ack必须为低。为了确定这三种情况中的每一种的匹配，开始三个单独的评估。这三个序列是：e1 #1（ack==0）e1 #2（ack==0）e1 #3（ack==0）4.3断言断言，也称为检查器，表示为检查或禁止子句。断言定义了系统的一个属性，它被监视以向用户提供功能验证能力。 断言被写为时态表达式，并且可以表达系统的值和事件之间的复杂时序和函数关系。如果关联的时态表达式至少有一个与该尝试匹配，则check子句导致该尝试成功否则，check子句将失败。一般来说，检查子句指定的期望是时间表达式对所有尝试都为真另一方面，禁止子句导致尝试成功如果相关联的时间表达式没有匹配，则执行该操作。否则，禁止条款失效。与检查子句相反，禁止子句被指定为确保某个条件永远不会发生。声明检查或禁止，使用标识符来命名断言，使用时钟来指定采样值/事件的时钟刻度，以及使用时间表达式来指定监视的关系。时钟事件规格检查名称：临时表达式;禁止名称：临时表达式;G时钟决定值和事件的采样时间在模拟过程中，每当事件规范描述的事件发生时，就会出现时钟事件规格可以是上升沿、下降沿、沿（下降或上升）或模拟时钟本身。实施例4.2时钟摆边检查规则1：if（pipelined）stage1#1stage 2#1stage 3;禁止规则2：if（pipelined）命令行instr#2命令行获取;G9？4.4时移操作形式语义[n.. m]A]]=[n：：m][[A]]，对于1nm[n.. m]A]]=/[m：：n][[A]]对于nm0[n.. m]A]]=（/[0：：n][[0：：m]）[[A]]，对于n0m[[#nA]]=[[#[n.. n]A]]，如果n>0[[A #n B]] = [[A]] [[#（n 1）B]][[A->> B]] = [[A]][[B]]时间以时钟滴答延迟的形式表示，并使用#符号指定。e1#t e2意味着e1应该发生，之后是（t 1）时钟滴答，之后是e2。换句话说，e1必须出现，然后在t时钟节拍4上出现e2。这个基本的时间符号用于表示表达式之间的时间关系，并为序列提供构建块。规范的示例是：序列之间的延迟、预期序列发生时的特定时钟滴答、预期序列完成的时间段以及序列发生的可能性。时间可以用多种方式表示，例如#t，表示t个时钟滴答，#[t1：：t2]，表示t1和t2之间的可变时间延迟，以及#[1.. simend]，表示最终在模拟结束之前。（简短的─切割符号->>可用于表示相同）实施例4.3考虑三个表达，分别表示正向转移、负向转移和可能性。txpexpr1=te1#2te2;对于expr1，预期te2在te1之后2个时钟周期出现txp expr 2= te1 # -1 te2;对于expr2，预期te2在te1之前出现1个时钟节拍txpexpr3=te1-> >te2;对于expr3，预期te2在te1之后但在模拟结束之前的某个时间发生4.5复合序列形式语义[[A或B]]=[[A]][[[B]][[A]]=[[A]]\[[B]][[inv A]]= inv [[A]]提供了三个运算符来构造序列：and、or和inv。4 TXP允许时移为负。然而，在本文中，我们将不详细的形式语义的这个功能。10[当两个操作数表达式都预期成功时，使用二元运算符和时间表达式和时间表达式和的两个操作数是时态表达式。与操作的匹配要求是两个操作数表达式必须匹配。当其中一个操作数表达式匹配时，它等待另一个匹配。复合表达式的结束时间是完成最后一个操作数的操作数表达式的结束时间。实施例4.4假设ve1、ve2、ve3、ve4和ve5是逻辑Verilog表达式，则第二个操作数更长，因此结束时间是从当前时间开始的4个时钟节拍(ve1#2 ve2）和（ve3 #2 ve4 #2 ve5）当两个操作数序列中至少有一个预期成功时，使用运算符或时间expr或时间expr或运算的匹配要求是两个操作数表达式中至少有一个成功。匹配的结束时间是匹配的任何时态表达式的结束时间。为了获得匹配的逆，使用inv运算符反转时间表达式运算符inv补5个匹配项。每个成功的匹配都转换为失败的匹配，反之亦然。通常，当用户对检测表达式的失败感兴趣当匹配成功表达式的所有可能性都用尽时，就会发生失败4.6条件匹配形式语义[[if AnextBnextelseC]]=if[[A]]next[[B]]else[[C]][[if AthenBelseC]]=if[[A]][next[[B]]else[[C][[if AnextB]]=if[[A]]next[[B]]else“[[ifAthenB]]=if[[A]]next[[B]]else“这些结构允许用户基于满足某些标准来监测序列。最常见的用法是将先决条件附加到序列，并在两个备选项之间选择序列，其中选择是基于条件的成功。提供了两种子句5 有一些例外，当inv可以同时导致匹配和失败时。 注意第2.1节中11如果第二，则继续如果第二，则seq1，否则seq2rst子句用于对时态表达式进行预处理（这里提供的功能与时态语言中如果condition cond失败，则跳过seq进行监视。注意，cond和seq都可以是时态表达式。当cond的监视与seq、seq1或seq2的监视重叠时，这些子句工作良好。实施例4.5考虑从主设备到目标设备的数据传输的总线操作。当总线进入数据传输阶段时，可以发生多个数据阶段以传输数据块。在数据传输阶段期间，数据阶段在任何时钟上升沿完成，在该时钟上升沿上irdy被解除断言并且trdy或stop被解除断言。注意，这里的被解除断言的信号意味着低的值，并且negedge意味着从高到低值的转变。 数据阶段的结束可以表示为clockposedgemixedftxpdataend=if（dataphase）then（（negedgeirdy&&（negedgetrdy|| return（）;G另一个变化是在条件和序列之间的连接效应。这些结构提供为如果第二个下一个序列如果第二个下一个序列1接第二个序列2与前面的子句不同，cond和seq、seq1或seq2之间没有重叠。在条件cond成功时，对时间表达式seq的监视在下一个时钟节拍处开始，即，在COND的结束和SEQ的开始之间存在一个时钟节拍差。请注意，如果cond产生多个序列，则考虑最早的匹配。4.7序列重复形式语义代表;代表;代表m]A]]=[[A]][n：：m]，0nm代表;代表;代表]A]]=[[A]]n[[A]]？对于0n和non extended[[A]]存在连续地重复监视时间表达的情况。在这种情况下，监视被执行指定的次数，并且每次都期望成功地从评估时间表达中产生。换句话说，重复与相同时间表达式的指定次数的级联相同。Repetition用repetition参数表示，该参数指定需要监视表达式的次数。此参数可以是一个数字或一个值范围重复顺序12seq#1 seq#1 seq：n可以是任何非零正整数常数，并且seq可以是时间表达式。上面的表达式在语义上等同于下面的表达式，|nt{imzes}实例4.6平行样本3（ev1 #1 ev2）说“序列（ev1 #1 ev2）必须连续出现三次相当于写（ev1 #1 ev2）#1（ev1 #1ev2）#1（ev1 #1 ev2）实施例4.7突发模式下的总线读取事务预期在8个数据阶段中读取数据。每个数据阶段跟随下一个，其中当信号irdy和trdy同时被解除断言时，数据阶段被称为发生。clockposedgemusclefcheckburstrule：if（negedge burst mode）then #2 rep 8（negedge trdy）（negedge irdy）;G断言突发规则表示“当检测到突发模式的下降沿时，两个时钟滴答之后，数据传输开始（trdy和irdy都被解除断言）并持续8次”。4.8序列形式语义[[istrue vinA]]=istruehviin[[A]][n. m]inA]]=len[n：：m][[A]][[len ninA]]=[[len[n.. n]inA]]事件序列常常在对正确行为的某些约束的假设下发生。例如，在处理事务时，逻辑条件必须为真。或者，事务必须在给定的时间段内完成，而不管在要处理的事务中发出什么命令变体。同样经常地，在处理事务时禁止某些事件的发生。这些情况可以直接使用以下两个结构表示：在时态表达式中创建逻辑表达式逻辑EXPR是一种逻辑表达式，其在时间EXPR的监视期间的每个时钟节拍处必须导致为真。如果temporal expr在时间t1开始并在时间t2结束，则逻辑expr必须从时间t1到t2保持为真。时间表达式中镜头时间移位测试时间移位指定时间表达式的持续时间的长度。时移规格的所有变化都是允许的。如果为时间移位指定单个数字，则它表示固定的持续时间。如果时间移位指定了一个数字范围，那么时间表达式可以在任何时候终止13在由最小和最大数量确定的时间段实施例4.8时钟脉冲检查突发规则1：if（negedge burst mode）thenistrue（！burstmode）in（#1 rep 8（negedge trdy&&negedgeirdy））;G在上面的表达式中，信号突发模式的值需要为低，并且在表达式（#1 rep 8（trdy==0）&&（irdy==0））期间的每个时钟节拍处检查。clock posedgemusclefcheck burstrule 3：if（negedge burst mode）thenlen #[9..11]在（#[1..4] rep 8（negedge trdynegedgeirdy））;&&G在上面的表达式中，整个重复序列的总持续时间必须不小于9个时钟节拍且大于11个时钟节拍。此限制由len #[9.. 11]在表达上。5结论我们提出了一种新的语言，用于指定对硬件设计人员有用的属性我们认为，在验证硬件设计时，排序操作是最常见的考虑因素。TXP非常适合这样的应用程序，因为它提供了一种方便的语法来编写PCI和Inniband等通用协议。基于正则表达式语义的TXP已实现在仿真运行时监视时态表达式。TXP也正在试验驱动一个正式的属性检查器。由于我们的TXP断言模型是基于nite状态自动机，一个interset-ing调查领域是行使TXP断言的自动刺激生成。我们的工作将继续检查硬件设计验证的各个方面，并调查该语言的未来扩展引用[1] T.克罗普夫正式硬件验证简介。Springer-Verlag，1999年[2] E. Clarke，O.Grumberg和D.佩尔德。模型检验，MIT出版社，1999年[3] 霍 普 克 罗 夫 特 和 厄 尔 曼 。 自 动 机 理 论 、 语 言 与 计 算 导 论 ， AddisonWesley，1979年[4] 基于Verilog硬件描述语言的IEEE标准硬件描述语言，IEEE计算机协会，IEEE Std 1364-1995，纽约，1996年14[5] 基于VHDL硬件描述语言的IEEE标准硬件描述语言，IEEE计算机协会，IEEE Std 1076-1993，纽约，1996年[6] H.平石基于“无”正则型逻辑模型检验算法的时序机设计验证，CMU-CS-88-1953，麦基-梅隆大学，1988年[7] J. Corbett，M. Dwyer，J. Hatterfly，Robby.动态软件可检查属性的语言框架，SPIN 软件模型检查研讨会论文集，计算机科学讲义，Springer-Verlog，2009年8月。2000