采用通用核查指令降低Verilog设计中命题的复杂性
命题的作用
一般来说，命题是描述一个特定的设计应该实现何种功能或不应该实现何种功能的语句。这样的一个描述可以在所有的时间或环境下为真，或者在设计中的特定行为下有条件地部分为真。命题也可称为“设计意图的表述”或“设计工程师的假设”，因为它们对设计的重要特性进行归档。最具有价值的命题不仅仅是文档，它们被动地观察设计并核查设计的行为是否与设计工程师的期望或假设一致。
作为命题的一个简单例程，我们可以观察采用One-Hot编码的状态机。在Verilog语言中没有任何特殊的编码方案来识别状态寄存器，若一个设计错误导致寄存器违反了One-Hot规则，则没有内在的机制来核查及报告这种违规。在这种情况下，采用命题是最适宜的。命题可描述寄存器的行为：它可以是被设计成、打算设计成或者被假设具有One-Hot编码的多种行为。这个命题既可是个注释并仅进行纯粹的信息描述，也可以是一个主动的命令,对One-Hot规则进行连续地核查。
命题的例程包括：
一个Verilog实例描述是并行的，两个项目永远不会同时为真；
一个状态机不会进行非法行为转换；
存储器要从经过初始化的地址读取信息；
接口上的两个信号要遵循请求-确认握手协议。
在所有的这些例程中，设计工程师企图匹配命题定义的行为来实现逻辑，但有时设计工程师会出错，而命题在这时则提供了一种交叉核查的方法；当设计工程师设计出来的行为与命题规定的行为不符时，命题就会发出报警。若在Verilog仿真时出现违反命题的情况，人们就非常希望能核查并报告这种违反命题的情况。
除了仿真之外，命题也是形式或半形式验证工具要达到的验证目标。这些工具构造基于形式的数学模型，并采用推理技术来证明或反证设计工程师所期望达到的电路行为的特性。
若验证工具发现了一种可以违反电路特性的方法，那么也就发现了电路设计中的某种缺陷。如果验证工具能够证明无法违反电路属性，那么就得到了有价值的验证信息。
形式或半形式验证工具能够证明两个Verilog例程项目不能同时评估，或没有办法让状态机进行非法行为转换。工程师非常希望形式验证工具的目标特性与仿真中使用的命题相匹配。这使命题具体化并在利用形式验证方法之前的仿真过程中排除故障。进一步来说，如果仿真测试套件中包含某种违反命题的测试，则表明存在设计缺陷，要在进行形式的分析前改正这种缺陷。
设计中的命题是“白盒”验证的一个极好的实例，因为它们能够将设计所期望的的内部行为具体化而不仅仅定义从设计输入到输出的端到端行为。在许多场合，包括上述几个实例，命题直接映射到内部设计结构，如状态机和存储器。
除了核查表示设计缺陷的问题之外，对电路内部结构的命题提高了整个设计的可观测性和设计行为的能见度。对于一个大型设计的输出，人们不容易核查到深藏在电路设计内部的设计缺陷的作用，并且诊断及改正这种缺陷也非常耗时。最好在缺陷源头或接近源头处核查到缺陷，这些地方往往就是内部设计结构命题所报告的设计违规之处。
基本Verilog命题
在Verilog设计中给定一个命题的最基本方法是加入一条注释。例如考虑前面讨论过的One-Hot状态寄存器。下列的代码表示，在代码文件中增加一段注释以表明总是采取One-Hot编码方式：
=============
reg [3:0] state_var；
// This state register should always be one_hot；
=============
对于设计工程师来说，将设计的要点在文件中进行注释是必不可少的，不管注释是否按可执行的命题形式编写。一个注释形式的命题记录了设计工程师的假设，并使另一工程师容易理解设计工程师的意图。
当然，注释的不利点也在于它仅仅是一个注释，在仿真过程中不能自动进行核查。因此，设计工程师有时采用特定的Verilog代码来核查设计假设并用Verilog “$display”语句来报告所有违规的设计。通常，设计工程师希望这个代码在仿真过程中被激活，但实际上不综合到逻辑关系中。有些设计工程师忽略了这个问题，他们指望逻辑综合工具来删除不影响任何模块输出的逻辑。
还有一些设计工程师认为，这种方法风险性太大，转而在命题核查代码附近采用“synthesis off/on”附注或某些其它形式的条件编译来确保命题核查代码不被综合。附注或许是必需的，它能使其它的RTL分析工具(如代码覆盖工具)也能够忽略核查逻辑。
下面是Verilog代码中用One-Hot命题来核查逻辑的一个例程。即使这样一个简单的命题也会引出若干问题：
============================
reg [3:0] state_var；
.
//synopsys translate_offinteger idx, ones_found；
always @(state_var)
begin
ones_found = 0；
for (idx = 0； idx 4 ； idx = idx + 1)
if (state_var[idx] === 1'b1)
ones_found = ones_found + 1；
if (ones_found != 1)
$display(one_hot violation at %d,$time)；
end
//synopsys translate_on
==============================
工程师在这个模块中增加了两个新变量(ones_found和idx)来支持核查逻辑。核查与设计紧密链接。
在本例中，若设计工程师要将“state_var”寄存器改名，那么核查逻辑也要做若干相应的变化。对更加复杂的命题核查而言，这种由RTL代码变化引起的波动效应的后果很严重，因为这种命题核查需要有几十甚至上百行Verilog代码。
这个简单的例程忽略了许多细节。例如，它核查的仅仅是1'b1位，而不管其它位是1'b0、未知的1'bx还是三态的1'bz。若设计工程师要报告“state_var”值(4'b0x10)的违规情况，那就需要更多的核查逻辑。在复位脉冲附近，需要特别处理，因为“state_var”值为4'b0000时就会超出复位范围，这时只有在第一个时钟后开始调出One-Hot值。频繁出现的情况是，看上去一个简单的命题核查实际上需要占用设计工程师的大量时间。
采用行间Verilog核查逻辑不需要验证复用。设计工程师可以结束在编程时进行大规模程序代码模块的剪切和粘贴以完成在不同地方进行的相似核查的编码。设计假设中的一个变更会导致多处代码也进行相应的变更。从仿真转移到形式或半形式验证时，这种方法就不需验证复用。通常，形式验证工具不能验证混在可综合或不可综合Verilog代码中的仅用“$display”语句表示的特性。
Verilog命题库
最明显的给定Verilog命题的方法是采用通用命题核查库，如最近引入的开放式验证库(OVL)。链接到特定设计结构的命题通常可以用在RTL代码的多处。每当可以采用相同的命题核查时，允许以复用方式调用这些以Verilog模块形式出现的通用命题。前述的一些复杂问题(如复位附近的特别处理)，一旦是库中模块，便能够解决，并且无论在何处引用，模块均会发生作用。
进一步而言，设计工程师可以不必花费很多精力来调整某种类型的RTL变更。当变量名称改变时，设计工程师只要更改在引用模块时使用的变量而不用在命题核查代码中进行多项更改。相对于采用行间Verilog核查逻辑来给定命题的方法来说，新方法的优点显著。
OVL定义了Verilog“监测器”模块库，它可在设计所用RTL代码表示命题的适当地方引用。当进行仿真并报告违规时，OVL监测程序执行命题核查。OVL的始创还表现在用形式验证工具可以在模块库内方便地设计一个命题。
下面是一个调用OVL模块核查状态寄存器的One-Hot编码例程。在核查逻辑附近，监测器模块包含有“systhesis translate off/on”附注，设计工程师不需要为了确保核查逻辑不被综合而采用特别的架构：
=========================
reg [3:0] state_var；
.
assert_one_hot #(0,4) oh1 (.clk(clock),.reset_n(rst_n),
.test_expr(state_var))；
============================
与显式Verilog代码相比，采用命题核查库的优点是显而易见的，但这种方法有其自身内在的局限性。例如，命题的风格使命题不能放在RTL代码的上下段之间。考虑到仅当某些条件为真的前提下命题有效(这种有效性需要核查)的情况，若命题条件已经在RTL代码中表达(如用Verilog if语句进行陈述)，在具体化核查程序时非常重要一点就是利用这些命题条件。
上下条件语句可以存在适用于行间Verilog核查逻辑之中，其中的不同命题核查可以根据周围的RTL代码执行。
不同的核查可放置在if和else子句之间，仅当相应的if或else条件为真时激活。上下条件语句之间的命题不能采用OVL之类的命题库来表达。Verilog的句法规则不允许在RTL的任意点上调用模块。这通常意味着设计逻辑必须被复制成为核查逻辑的一部分以构建适用的条件。
调用Verilog模块进行命题核查的另一个局限性在于，这种方法缺乏自变量句法的灵活性。虽然Verilog参数有一定的灵活性(例如变量宽度),但调用Verilog模块时不允许简单指定任选自变量的变量数(这种自变量具有缺省的自变量值)。通常来说，在调用的每个Verilog命题库元素中，每一个自变量必须被明确地指定。
命题库并不一定用Verilog语言写成。有些人用C语言或其它的测试平台语言来写命题程序，通过PLI接口将命题程序与Verilog程序相连。采用PLI调用允许比用Verilog模块调用有更灵活的句法。不足之处是PLI自身是一种低效的接口，因而采用这种类型的命题核查通常会增加一些不堪承受的仿真开销。
核查器指令
在Verilog中，给定命题核查的最灵活方法是使用注释指令句法从一个命题核查库中调用相应元素。采用注释意味着不用“synthesis off/on”附注或其它的特别处理就能使命题对逻辑综合或其它的工具透明。自由的Verilog模块调用句法允许采用上下条件命题，命题的自变量数目也具有高度灵活性。
更重要的是，一个智能核查器生成工具组合了核查器指令和RTL设计中的信息来产生核查码，这种核查码针对特定的设计度身定制。下面给出的代码是一个One-Hot命题的例程。任何相关的时钟、复位甚至要核查的变量均能够从处于指令同一行的寄存器说明来推断。一个核查器生成工具能够读取包含有这种指令的RTL文件，然后构建适用于对“state_var”进行One-Hot核查的程序，“state_var”将在仿真时工作并报告任何可能的违规设计。
==========================
reg [3:0] state_var； //assertion one_hot
reg [5:0] state_var； //assertion one_hot
reg [3:0] renamed_state_var； //assertion one_hot
==========================
这段程序表明了采用命题库的另一优点。精选的指令名称有助于设计程序自行对文件进行归档。对于必须阅读和理解RTL代码的工程师来说，采用一个名为One_Hot的命题较之行间Verilog代码更易理解。
组合了智能核查器生成工具的核查器指令方法具有强大的功能，它允许核查器程序适应RTL代码中可能产生的变更。上面显示的所有三个指令是相互等效的，然而，由于待核查的状态寄存器的名称和宽度可从RTL中推断，核查器生成工具会产生不同的核查程序。因此，在RTL中进行的一般性更改不需对核查指令作任何的调整。
由于具备上述的优点，在研制白盒验证套件时选择了核查器指令方法。核查器指令使设计工程师在编写Verilog RTL代码时能非常方便地给定命题。0-In公司的通用指令参考了0-In CheckerWare库，它们包括：
Verilog核查器的数据路径元素。例如验证数据在电缆传输时没有发生数据丢失，或在FIFO或存储器中没有发生数据错误；
Verilog 核查器的控制结构。例如验证仲裁方案是否正确，或状态机工作是否正常；
Verilog核查器的接口。例如验证信号间的多周期时序关系或核查三态总线是否始终处于被驱动状态。
在CheckerWare库中有五十多个项目的核查器，单个接口核查器被组合来构成CheckerWare监测程序，此监测程序核查复杂总线的完整协议规则。CheckerWare监测程序可以进行标准接口的正确性核查，所涉及的标准接口包括PCI、PCI-X、UTOPIA、SDRAM及ARM微处理器所用的AMBA总线。
核查指令可以用RTL代码或独立的Verilog文件直接调用。核查工具是一个智能核查生成工具，它可从指令周围的RTL上下条件推断出尽可能多的信息。若将指令放置在RTL的最佳位置，核查程序就会自动前后调节并在文件自行调用时增加指令值。
下面的例程说明了如何应用0-In核查指令来自动完成不同的核查，这种核查依据寄存器的配置行为(递增或递减)来进行：
==========================
reg [7:0] cnt；
.
if (monotonic_direction === 1'b1) cnt = cnt + 8'h01； //0in overflow
else
cnt = cnt - 8'h01； //0in underflow
==========================
利用0-In核查器，可从Verilog RTL推断的信息数量非常巨大。例如，CheckerWare库包括了“data_used”核查，这种核查揭示的是装入源寄存器的数据在重写之前至少被一个目标寄存器使用。当0-In核查器读取如下所示的简单指令后，就可推断出所有的目标寄存器及所有相关的选择条件、加载启动和可以防止源数据到达目标寄存器的时钟门。所产生的Verilog核查综合考虑了所有这些条件，因此指令会自动适应RTL的逻辑变化。0-In核查器也会自动将核查与设计等级相匹配，以使同一指令既能在模块级也能在系统级的仿真中使用。
====================
reg [7:0] pipe_stage_3； // 0in data_used
====================
所有CheckerWare核查器和监测程序可以跟踪结构覆盖范围内的信息，也能够提供在仿真中表现出的设计结构运用好坏情况的反馈信息。例如，FIFO核查器主张FIFO既不在其空时接受读操作也不在其满时接受写操作。不管仿真测试是否曾经充满FIFO或在至少增加了一个输入项后全部耗尽，结构覆盖分析均会提供报告。如果这两种情况均没有发生，那么FIFO并没有通过仿真来达到足够的核查。当验证工程师在指导测试研发时，这些结构覆盖“孔”被证明非常有价值。
最后，所有的0-In指令产生的核查器不仅用于仿真，也用于0-In Search半形式验证工具。传统的形式工具如模型核查器也能容易实现0-In核查器。这样相同的0-In核查指令可以提供用于仿真的命题、形式及半形式验证并支持文件自动调用的RTL代码。
虽然Verilog本身不支持命题，但抓住设计意图和设计工程师的假设的意义是人所共知的。由于降低了给定命题的复杂程度，所有工程师都愿意采用这种经证明有效的白盒验证工具。目前，在Verilog设计中采用不同的方法表示命题核查。这些方法中最具灵活性的是通用核查指令，它可以接入具有最小规范说明、适应性强、内容丰富的命题核查库。
作者：Ramesh Sathianathan
设计验证经理
0-In设计自动化公司
Tom Anderson
应用工程副总裁
0-In设计自动化公司
评论