出题办法在软件规划中现已运用了很长时刻，并已成为许多软件研制团队运用的干流办法，但是，在硬件描绘言语Verilog 或 VHDL中选用出题来进行硬件规划也不过最近才开端遍及。尽管VHDL具有固有的出题结构，但是Verilog却没有。因而选用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规划主动化公司
