文章目录

一、断言简介
- 1.1.断言分类——立即断言/并发断言
- 1.2.断言的语法结构层次
二、并发断言序列sequence
- 2.1. 关键字(sequence、property)与操作符( |=>、|->)
- 2.2. sequence的重复操作符——连续[*n]、非连续[=n]、跟随[->n]
- 2.2. sequence序列采样函数——$ rose、$ fell、$ past、$ stable、$ sampled
- 2.3. sequence序列操作符——and、intersect、or、first_match、within、throughout、ended
三、并发断言属性property
- 3.1. assert、assume、cover
- 3.2. disable iff 与not用法
- 3.3. 多时钟属性
四、代码示例

一、断言简介

断言是对设计行为属性的描述。它使用描述性语言来描述了设计必须满足的属性。在仿真过程中，如果一个被描述的属性不是期望的那样，那么断言就将失败，或者在仿真过程中，出现了一个不该出现的属性，断言也将失败。
使用断言的原因：原有的Verilog语言是一种过程性设计语言，在硬件设计过程中不能很好的描述时序行为。而SVA是一种描述性语言，可以很好的描述和控制复杂设计的时序的相关问题，代码简洁，易于维护。基于断言的验证方法（ABV）是对验证的增补，通过白盒验证的方式可以获取设计的意图，提供设计的可观察性，有利于指导验证工作，加快验证进度，保证验证的完备性。除此之外，断言还可以对总线协议进行定义和验证（AHB/APB）等，相当于一个RTL代码的监视器。

1.1.断言分类——立即断言/并发断言

断言分为立即断言和并发断言。立即断言是非事件性的，断言属性类似if语句中的条件表达式，用于检查表达式的值是否为真，断言失败时必须采用相应的仿真行为，如下语法：

assert_info：assert(expression)$display("passed");       //expression为真时，执行语句else$display("failed");      //expression为假时，执行语句

相比于立即断言，并发断言更为常用，并发断言基于时钟周期，用于描述一个跨时钟周期的行为，并发断言使用关键字property…endproperty描述事件，如下：

property  p_shakehand;                 //当行为属性p_shakehand中的条件request为真时，结果序列必须为真，否者序列失败@(posedge  clk)                     //符号“|=>”左侧的为原因序列，右侧为结果序列request |=> acknowledge ##1 data_enable ##1 done;      //2. 当request为1时，启动线程序列检查
endproperty
apshakehand:assert property(p_shakehand);       //1. assert关键字启动断言检查

1.2.断言的语法结构层次

SVA语法主要分为五个结构层次：

最底层——布尔表达式；
第二层——序列（sequence），其中可包含一些操作符，如##时隙延迟、重复操作符、序列操作符等，序列是一个封装格式，可在不同地方使用；
第三层——属性（property），重要的封装方式，可封装sequence，内部可定义蕴涵操作符（|->，|=>）；
第四层——断言指示层，即采用assert对特定的属性或者序列做行为检查，或者采用cover做覆盖率统计；
第五层——断言的最后封装，这一层可以通过module、program、interface来进行封装。

二、并发断言序列sequence

并发断言基于时钟周期的，因而只有利用时钟周期采样的值才有效。下面以并发断言为主进行讲解。需要说明的是断言属性有七种，序列sequence只是其中之一（属性property包含有序列sequence、否定Negation、分离Disjunction、联合Conjunction、if…else…、implication、instantation）。

2.1. 关键字(sequence、property)与操作符( |=>、|->)

thread：线程是一组相关的事件序列（原因序列与结果序列），表示一种设计属性；
sequence：序列是描述一种信号时序关系的基本语句块；
property：属性用于封装各种sequence，可作为检查器、假设条件和覆盖率，对应关键字为assert、assume、cover；
|-> ：表示起因序列与结果序列处于同一个时钟周期；只有当起因序列为真时才进行结果序列的检查，避免虚假错误的产生。
|=> ：表示结果序列处于起因序列的下一个时钟周期；等效于##1。
断言的建立过程与格式：

#mermaid-svg-H3SxEVKIaB6uuF3R .label{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);fill:#333;color:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .label text{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .node rect,#mermaid-svg-H3SxEVKIaB6uuF3R .node circle,#mermaid-svg-H3SxEVKIaB6uuF3R .node ellipse,#mermaid-svg-H3SxEVKIaB6uuF3R .node polygon,#mermaid-svg-H3SxEVKIaB6uuF3R .node path{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-H3SxEVKIaB6uuF3R .node .label{text-align:center;fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .node.clickable{cursor:pointer}#mermaid-svg-H3SxEVKIaB6uuF3R .arrowheadPath{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .edgePath .path{stroke:#333;stroke-width:1.5px}#mermaid-svg-H3SxEVKIaB6uuF3R .flowchart-link{stroke:#333;fill:none}#mermaid-svg-H3SxEVKIaB6uuF3R .edgeLabel{background-color:#e8e8e8;text-align:center}#mermaid-svg-H3SxEVKIaB6uuF3R .edgeLabel rect{opacity:0.9}#mermaid-svg-H3SxEVKIaB6uuF3R .edgeLabel span{color:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .cluster rect{fill:#ffffde;stroke:#aa3;stroke-width:1px}#mermaid-svg-H3SxEVKIaB6uuF3R .cluster text{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R div.mermaidTooltip{position:absolute;text-align:center;max-width:200px;padding:2px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:12px;background:#ffffde;border:1px solid #aa3;border-radius:2px;pointer-events:none;z-index:100}#mermaid-svg-H3SxEVKIaB6uuF3R .actor{stroke:#ccf;fill:#ECECFF}#mermaid-svg-H3SxEVKIaB6uuF3R text.actor>tspan{fill:#000;stroke:none}#mermaid-svg-H3SxEVKIaB6uuF3R .actor-line{stroke:grey}#mermaid-svg-H3SxEVKIaB6uuF3R .messageLine0{stroke-width:1.5;stroke-dasharray:none;stroke:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .messageLine1{stroke-width:1.5;stroke-dasharray:2, 2;stroke:#333}#mermaid-svg-H3SxEVKIaB6uuF3R #arrowhead path{fill:#333;stroke:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .sequenceNumber{fill:#fff}#mermaid-svg-H3SxEVKIaB6uuF3R #sequencenumber{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R #crosshead path{fill:#333;stroke:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .messageText{fill:#333;stroke:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .labelBox{stroke:#ccf;fill:#ECECFF}#mermaid-svg-H3SxEVKIaB6uuF3R .labelText,#mermaid-svg-H3SxEVKIaB6uuF3R .labelText>tspan{fill:#000;stroke:none}#mermaid-svg-H3SxEVKIaB6uuF3R .loopText,#mermaid-svg-H3SxEVKIaB6uuF3R .loopText>tspan{fill:#000;stroke:none}#mermaid-svg-H3SxEVKIaB6uuF3R .loopLine{stroke-width:2px;stroke-dasharray:2, 2;stroke:#ccf;fill:#ccf}#mermaid-svg-H3SxEVKIaB6uuF3R .note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-H3SxEVKIaB6uuF3R .noteText,#mermaid-svg-H3SxEVKIaB6uuF3R .noteText>tspan{fill:#000;stroke:none}#mermaid-svg-H3SxEVKIaB6uuF3R .activation0{fill:#f4f4f4;stroke:#666}#mermaid-svg-H3SxEVKIaB6uuF3R .activation1{fill:#f4f4f4;stroke:#666}#mermaid-svg-H3SxEVKIaB6uuF3R .activation2{fill:#f4f4f4;stroke:#666}#mermaid-svg-H3SxEVKIaB6uuF3R .mermaid-main-font{font-family:"trebuchet ms", verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .section{stroke:none;opacity:0.2}#mermaid-svg-H3SxEVKIaB6uuF3R .section0{fill:rgba(102,102,255,0.49)}#mermaid-svg-H3SxEVKIaB6uuF3R .section2{fill:#fff400}#mermaid-svg-H3SxEVKIaB6uuF3R .section1,#mermaid-svg-H3SxEVKIaB6uuF3R .section3{fill:#fff;opacity:0.2}#mermaid-svg-H3SxEVKIaB6uuF3R .sectionTitle0{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .sectionTitle1{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .sectionTitle2{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .sectionTitle3{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .sectionTitle{text-anchor:start;font-size:11px;text-height:14px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .grid .tick{stroke:#d3d3d3;opacity:0.8;shape-rendering:crispEdges}#mermaid-svg-H3SxEVKIaB6uuF3R .grid .tick text{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .grid path{stroke-width:0}#mermaid-svg-H3SxEVKIaB6uuF3R .today{fill:none;stroke:red;stroke-width:2px}#mermaid-svg-H3SxEVKIaB6uuF3R .task{stroke-width:2}#mermaid-svg-H3SxEVKIaB6uuF3R .taskText{text-anchor:middle;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .taskText:not([font-size]){font-size:11px}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutsideRight{fill:#000;text-anchor:start;font-size:11px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutsideLeft{fill:#000;text-anchor:end;font-size:11px}#mermaid-svg-H3SxEVKIaB6uuF3R .task.clickable{cursor:pointer}#mermaid-svg-H3SxEVKIaB6uuF3R .taskText.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutsideLeft.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutsideRight.clickable{cursor:pointer;fill:#003163 !important;font-weight:bold}#mermaid-svg-H3SxEVKIaB6uuF3R .taskText0,#mermaid-svg-H3SxEVKIaB6uuF3R .taskText1,#mermaid-svg-H3SxEVKIaB6uuF3R .taskText2,#mermaid-svg-H3SxEVKIaB6uuF3R .taskText3{fill:#fff}#mermaid-svg-H3SxEVKIaB6uuF3R .task0,#mermaid-svg-H3SxEVKIaB6uuF3R .task1,#mermaid-svg-H3SxEVKIaB6uuF3R .task2,#mermaid-svg-H3SxEVKIaB6uuF3R .task3{fill:#8a90dd;stroke:#534fbc}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutside0,#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutside2{fill:#000}#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutside1,#mermaid-svg-H3SxEVKIaB6uuF3R .taskTextOutside3{fill:#000}#mermaid-svg-H3SxEVKIaB6uuF3R .active0,#mermaid-svg-H3SxEVKIaB6uuF3R .active1,#mermaid-svg-H3SxEVKIaB6uuF3R .active2,#mermaid-svg-H3SxEVKIaB6uuF3R .active3{fill:#bfc7ff;stroke:#534fbc}#mermaid-svg-H3SxEVKIaB6uuF3R .activeText0,#mermaid-svg-H3SxEVKIaB6uuF3R .activeText1,#mermaid-svg-H3SxEVKIaB6uuF3R .activeText2,#mermaid-svg-H3SxEVKIaB6uuF3R .activeText3{fill:#000 !important}#mermaid-svg-H3SxEVKIaB6uuF3R .done0,#mermaid-svg-H3SxEVKIaB6uuF3R .done1,#mermaid-svg-H3SxEVKIaB6uuF3R .done2,#mermaid-svg-H3SxEVKIaB6uuF3R .done3{stroke:grey;fill:#d3d3d3;stroke-width:2}#mermaid-svg-H3SxEVKIaB6uuF3R .doneText0,#mermaid-svg-H3SxEVKIaB6uuF3R .doneText1,#mermaid-svg-H3SxEVKIaB6uuF3R .doneText2,#mermaid-svg-H3SxEVKIaB6uuF3R .doneText3{fill:#000 !important}#mermaid-svg-H3SxEVKIaB6uuF3R .crit0,#mermaid-svg-H3SxEVKIaB6uuF3R .crit1,#mermaid-svg-H3SxEVKIaB6uuF3R .crit2,#mermaid-svg-H3SxEVKIaB6uuF3R .crit3{stroke:#f88;fill:red;stroke-width:2}#mermaid-svg-H3SxEVKIaB6uuF3R .activeCrit0,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCrit1,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCrit2,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCrit3{stroke:#f88;fill:#bfc7ff;stroke-width:2}#mermaid-svg-H3SxEVKIaB6uuF3R .doneCrit0,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCrit1,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCrit2,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCrit3{stroke:#f88;fill:#d3d3d3;stroke-width:2;cursor:pointer;shape-rendering:crispEdges}#mermaid-svg-H3SxEVKIaB6uuF3R .milestone{transform:rotate(45deg) scale(0.8, 0.8)}#mermaid-svg-H3SxEVKIaB6uuF3R .milestoneText{font-style:italic}#mermaid-svg-H3SxEVKIaB6uuF3R .doneCritText0,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCritText1,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCritText2,#mermaid-svg-H3SxEVKIaB6uuF3R .doneCritText3{fill:#000 !important}#mermaid-svg-H3SxEVKIaB6uuF3R .activeCritText0,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCritText1,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCritText2,#mermaid-svg-H3SxEVKIaB6uuF3R .activeCritText3{fill:#000 !important}#mermaid-svg-H3SxEVKIaB6uuF3R .titleText{text-anchor:middle;font-size:18px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R g.classGroup text{fill:#9370db;stroke:none;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family);font-size:10px}#mermaid-svg-H3SxEVKIaB6uuF3R g.classGroup text .title{font-weight:bolder}#mermaid-svg-H3SxEVKIaB6uuF3R g.clickable{cursor:pointer}#mermaid-svg-H3SxEVKIaB6uuF3R g.classGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-H3SxEVKIaB6uuF3R g.classGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R .classLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.5}#mermaid-svg-H3SxEVKIaB6uuF3R .classLabel .label{fill:#9370db;font-size:10px}#mermaid-svg-H3SxEVKIaB6uuF3R .relation{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-H3SxEVKIaB6uuF3R .dashed-line{stroke-dasharray:3}#mermaid-svg-H3SxEVKIaB6uuF3R #compositionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #compositionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #aggregationStart{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #aggregationEnd{fill:#ECECFF;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #dependencyStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #dependencyEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #extensionStart{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R #extensionEnd{fill:#9370db;stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R .commit-id,#mermaid-svg-H3SxEVKIaB6uuF3R .commit-msg,#mermaid-svg-H3SxEVKIaB6uuF3R .branch-label{fill:lightgrey;color:lightgrey;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .pieTitleText{text-anchor:middle;font-size:25px;fill:#000;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .slice{font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R g.stateGroup text{fill:#9370db;stroke:none;font-size:10px;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R g.stateGroup text{fill:#9370db;fill:#333;stroke:none;font-size:10px}#mermaid-svg-H3SxEVKIaB6uuF3R g.statediagram-cluster .cluster-label text{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R g.stateGroup .state-title{font-weight:bolder;fill:#000}#mermaid-svg-H3SxEVKIaB6uuF3R g.stateGroup rect{fill:#ECECFF;stroke:#9370db}#mermaid-svg-H3SxEVKIaB6uuF3R g.stateGroup line{stroke:#9370db;stroke-width:1}#mermaid-svg-H3SxEVKIaB6uuF3R .transition{stroke:#9370db;stroke-width:1;fill:none}#mermaid-svg-H3SxEVKIaB6uuF3R .stateGroup .composit{fill:white;border-bottom:1px}#mermaid-svg-H3SxEVKIaB6uuF3R .stateGroup .alt-composit{fill:#e0e0e0;border-bottom:1px}#mermaid-svg-H3SxEVKIaB6uuF3R .state-note{stroke:#aa3;fill:#fff5ad}#mermaid-svg-H3SxEVKIaB6uuF3R .state-note text{fill:black;stroke:none;font-size:10px}#mermaid-svg-H3SxEVKIaB6uuF3R .stateLabel .box{stroke:none;stroke-width:0;fill:#ECECFF;opacity:0.7}#mermaid-svg-H3SxEVKIaB6uuF3R .edgeLabel text{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .stateLabel text{fill:#000;font-size:10px;font-weight:bold;font-family:'trebuchet ms', verdana, arial;font-family:var(--mermaid-font-family)}#mermaid-svg-H3SxEVKIaB6uuF3R .node circle.state-start{fill:black;stroke:black}#mermaid-svg-H3SxEVKIaB6uuF3R .node circle.state-end{fill:black;stroke:white;stroke-width:1.5}#mermaid-svg-H3SxEVKIaB6uuF3R #statediagram-barbEnd{fill:#9370db}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-cluster rect{fill:#ECECFF;stroke:#9370db;stroke-width:1px}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-cluster rect.outer{rx:5px;ry:5px}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-state .divider{stroke:#9370db}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-state .title-state{rx:5px;ry:5px}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-cluster.statediagram-cluster .inner{fill:white}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-cluster.statediagram-cluster-alt .inner{fill:#e0e0e0}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-cluster .inner{rx:0;ry:0}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-state rect.basic{rx:5px;ry:5px}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-state rect.divider{stroke-dasharray:10,10;fill:#efefef}#mermaid-svg-H3SxEVKIaB6uuF3R .note-edge{stroke-dasharray:5}#mermaid-svg-H3SxEVKIaB6uuF3R .statediagram-note rect{fill:#fff5ad;stroke:#aa3;stroke-width:1px;rx:0;ry:0}:root{--mermaid-font-family: '"trebuchet ms", verdana, arial';--mermaid-font-family: "Comic Sans MS", "Comic Sans", cursive}#mermaid-svg-H3SxEVKIaB6uuF3R .error-icon{fill:#522}#mermaid-svg-H3SxEVKIaB6uuF3R .error-text{fill:#522;stroke:#522}#mermaid-svg-H3SxEVKIaB6uuF3R .edge-thickness-normal{stroke-width:2px}#mermaid-svg-H3SxEVKIaB6uuF3R .edge-thickness-thick{stroke-width:3.5px}#mermaid-svg-H3SxEVKIaB6uuF3R .edge-pattern-solid{stroke-dasharray:0}#mermaid-svg-H3SxEVKIaB6uuF3R .edge-pattern-dashed{stroke-dasharray:3}#mermaid-svg-H3SxEVKIaB6uuF3R .edge-pattern-dotted{stroke-dasharray:2}#mermaid-svg-H3SxEVKIaB6uuF3R .marker{fill:#333}#mermaid-svg-H3SxEVKIaB6uuF3R .marker.cross{stroke:#333}:root { --mermaid-font-family: "trebuchet ms", verdana, arial;}#mermaid-svg-H3SxEVKIaB6uuF3R {color: rgba(0, 0, 0, 0.75);font: ;}

1. 编写序列sequence

2. 编写属性property

3. 编写断言assert或覆盖cover语句

sequence s1;       //sequence主要描述信号与信号之间的时序关系a ##1 b ##1 c;    //a为高，下一拍b为高，在下一拍c为高
endsequenceproperty p1;       //property主要将各种sequence进行封装s1;
endpropertya1:assert property(@(posedge clk) a |-> p1 );    //关键字assert启动断言， |-> :表示起因序列和结果序列在同一个周期

2.2. sequence的重复操作符——连续[*n]、非连续[=n]、跟随[->n]

重复操作符（连续）—— [*n]、 [*min：max] ，用法示例如下：

示例1：       a ##1 b[*3] ##1 c     等价于    a ##1 b ##1 b ##1 b ##1 c
示例2：       a ##1 b[*3：4] ##1 c     等价于    a ##1 b ##1 b ##1 b ##1 c 或者 a ##1 b ##1 b ##1 b ##1 b ##1 c

重复操作符1（非连续） —— [=n]、 [=min：max]，示例如下

示例1：  a ##1 b[=2] ##1 c     含义：第一拍a为1，最后一排c为1，a与c之间b为1要出现2次，非连续出现。
示例1：  a ##1 b[=2：5] ##1 c     含义：第一拍a为1，最后一拍c为1，a与c之间b为1最少出现2次，最多出现5次，非连续出现。

重复操作符2（非连续） —— [->n]、 [->min：max]，示例如下

示例1：a ##1 b[->2] ##1 c  含义：第一拍a为1，最后一排c为1，且*倒数第二拍b也为1*，a与c之间b为1要出现2次，非连续出现。
示例1：a ##1 b[->2：5] ##1 c  含义：第一拍a为1，最后一拍c为1，*倒数第二拍b也为1，a与c之间b为1最少出现2次，最多出现5次，非连续出现。

2.2. sequence序列采样函数——$ rose、$ fell、$ past、$ stable、$ sampled

$ rose：判断上升沿。如果表达式的值跳变为1，$rose函数返回真，否则返回假
$ fell：判断下降沿。如果表达式的值跳变为0，$fell函数返回真，否则返回假
$ past：返回当前时钟周期之前的一个时钟周期的表达式的采样值
$ stable：判断信号的稳定不变，如果表达式的值保持稳定不变，$ stable函数返回真，否则返回假
$ sampled：在时钟事件的最后时刻采样表达式的值

`define  data_end_exp  (data_phase && ((irdy==0)&&($fell(trdy)||$fell(stop))))         //声明宏定义
property  data_end_rule;@(posedge  mclk)`data_end_exp |-> ##[1:2] $rose(frame) ##1 $rose(irdy);
endproperty

2.3. sequence序列操作符——and、intersect、or、first_match、within、throughout、ended

and操作符：表示两个序列是匹配的，具有相同的起点，但是他们的结束时间不一致，由长序列的结束点为准。
intersect交互操作符：用于描述两个序列匹配，长度一样，且结束时间必须一致。相当于and操作符的一个特例。
or操作符：用于描述两个序列至少有一个是匹配的，即至少有个序列为真，则操作为真。
first_match操作符：如果有多个匹配序列时，first_match操作符只返回第一个操作序列
throughout跨越序列：在假设条件为真时，一个序列才会发生正确的行为

sequence burst_rule1;@(posedge mclk)$fell(burst_mode) ##0(!burst_mode) throughout (##2 ((trdy==0)&&(irdy==0)) [*7]);
endsequence

ended关键字：可以测试任意序列是否到达结束点。用法：“序列名.ended”

三、并发断言属性property

3.1. assert、assume、cover

assert关键字：属性检查，相当于检查器
assume关键字：将属性当做假设条件，仿真时，验证环境必须满足属性要求，否者必须报错
cover关键字：收集设计行为的覆盖率。

功能覆盖率分为面向数据覆盖率和面向控制的覆盖率，面向数据覆盖率可以通过编写覆盖组covergroup收集覆盖率，而面向控制的覆盖率用于检查行为序列，通过SVA编写行为序列，使用关键字cover收集覆盖率。

3.2. disable iff 与not用法

disable iff(expression)：当expression为真时，关闭property的序列检查，否则进行检查
not：表示not后的序列不能出现

property  abc(a, b ,c);     //参数化disable iff(a==1)    //当a为1时，关闭属性检查not @clk (b ##1 c);   //not后的序列不能出现
endproperty
env_property：assert property(abc(rst, in, out)) pass_statement; else fail_statement;
//statement语句是可选的，当属性为真，执行pass_statement，否则执行fail_statement

3.3. 多时钟属性

|-> ：表示起因序列与结果序列起始点处于同一个时钟周期；

@(posedge clk0) s0 |-> @(posedge clk1) s1        //语法序列不合法，存在不同的时钟
@(posedge clk0) s0 |-> @(posedge clk0) s1        //正确

|=> ：表示结果序列处于起因序列的下一个时钟周期；

@(posedge clk0) sig0 |=> @(posedge clk1) sig1     //操作符"|=>"用于同步clk0与clk1的上升沿

四、代码示例

module sequence_demo();bit rst_n;bit clk;reg a,b,c;event e1;initial beginforever #10 clk = ~clk;
endinitial beginrst_n = 1;#5;rst_n = 0;     //复位处理#5;rst_n = 1;     //撤销复位->e1;
endinitial begin$vcdpluson();     //该系统函数是为了使代码运行完毕之后，生成相应的波形文件@e1;a <= 0;b <= 0;c <= 0;repeat(3)begin@(posedge clk);a <= 1;@(posedge clk);a <= 0;b <= 1;@(posedge clk);a <= 0;b <= 0;c <= 1;@(posedge clk);c <= 0;end@(posedge clk);               @(posedge clk);@(posedge clk);
endsequence s1;       //sequence主要描述信号与信号之间的时序关系a ##1 b ##1 c;    //a为高，下一拍b为高，在下一拍c为高
endsequenceproperty p1;       //property主要将各种sequence进行封装s1;
endpropertya1:assert property(@(posedge clk) a |-> p1 );    //启动断言， |-> :表示起因序列和结果序列在同一个周期endmodule

启动脚本编译后：使用Makefile实例三，略微修改all选项即可。

SVA——断言属性之序列（sequence与property的用法）相关推荐

SVA 断言翻译笔记 16.13多时钟序列语法（九）
16.13 Multiclock support(多时钟支持) 目录 16.13 Multiclock support(多时钟支持) 1.多时钟序列 2.多时钟属性 3.时钟流 4.例子 5.在多时钟 ...
SVA 断言 note
断言概念一般,断言是基于时序逻辑的,单纯进行组合逻辑的断言很少见,因为太费内存(时序逻辑是每个时钟周期判断一次,而组合逻辑却是每个时钟周期内判断多次,内存吃不消). 因此,写断言的一般规则是: ti ...
mysql添加序列触发器_Oracle中使用触发器(trigger)和序列(sequence)模拟实现自增列实例...
问题:在SQL Server数据库中,有自增列这个字段属性,使用起来也是很方便的.而在Oracle中却没有这个功能,该如何实现呢? 答:在Oracle中虽然没有自增列的说法,但却可以通过触发器(tri ...
属性项目的定义（property）［ZT］
原文地址:属性项目的定义(property) @property (copy, nonatomic) NSString *title; 什么是assign,copy,retain之间的区别? assi ...
Oracle数据库中序列(SEQUENCE)的用法详解
http://database.51cto.com/art/201108/280742.htm 在Oracle数据库中,什么是序列呢?它的用途是什么?序列(SEQUENCE)其实是序列号生成器,可以为 ...
oracle初始化序列值,如何修改序列(Sequence)的初始值(START WITH)
Oracle 序列(Sequence)主要用于生成流水号,Oracle EBS系统中是经常用到的.但是,有时需要修改序列初始值(START WITH)时,好多人凭感觉认为:Alter Sequence ...
手机怎么安装py thon_Python属性装饰器– Python @property
手机怎么安装py thon Hello friends, today we will learn about Python property decorator. In our previous tu ...
序列(SEQUENCE)、同义词(SYNONYM)
--============================================= --SQL基础--> 序列(SEQUENCE).同义词(SYNONYM) --========== ...
Oracle sql创建序列sequence
知道的创建表序列的用途是当建立表的时候,Oracle不像Mysql一样会有自动主键增长AUTO_INCREMENT,所有如果需要主键自动增长的效果,Oracle提供了序列sequence方式. 创建序 ...

SVA——断言属性之序列（sequence与property的用法）