采用通用核查指令降低Verilog设计中命题的复杂性

采用通用核查指令降低Verilog设计中命题的复杂性

     对于集成电路设计工程师来说，把设计要点用命题注释可以提高程序的可读性，但是这会引出在综合过程中如何利用命题，并防止对命题综合从而影响逻辑输出的问题。本文比较了在Verilog 或 VHDL语言程序中不同的命题方法进行硬件设计验证的优点和缺点，所提出的白盒验证工具能够降低命题的复杂性。
    
     命题方法在软件设计中已经应用了很长时间，并已成为许多软件研发团队使用的主流方法，然而，在硬件描述语言Verilog 或 VHDL中采用命题来进行硬件设计也不过最近才开始普及。虽然VHDL具备固有的命题结构，但是Verilog却没有。因此采用Verilog语言的设计及验证工程师要采用不同的命题方法。本文对几种不同的命题方法进行了研究，阐述了它们各自的优缺点。
    
    命题的作用
    
     一般来说，命题是描述一个特定的设计应该实现何种功能或不应该实现何种功能的语句。这样的一个描述可以在所有的时间或环境下为真，或者在设计中的特定行为下有条件地部分为真。命题也可称为“设计意图的表述”或“设计工程师的假设”，因为它们对设计的重要特性进行归档。最具有价值的命题不仅仅是文档，它们被动地观察设计并核查设计的行为是否与设计工程师的期望或假设一致。
    
     作为命题的一个简单例程，我们可以观察采用One-Hot编码的状态机。在Verilog语言中没有任何特殊的编码方案来识别状态寄存器，若一个设计错误导致寄存器违反了One-Hot规则，则没有内在的机制来核查及报告这种违规。在这种情况下，采用命题是最适宜的。命题可描述寄存器的行为：它可以是被设计成、打算设计成或者被假设具有One-Hot编码的多种行为。这个命题既可是个注释并仅进行纯粹的信息描述，也可以是一个主动的命令,对One-Hot规则进行连续地核查。
    
    命题的例程包括：
    
     1、一个Verilog实例描述是并行的，两个项目永远不会同时为真；
     2、一个状态机不会进行非法行为转换；
     3、存储器要从经过初始化的地址读取信息；
     4、接口上的两个信号要遵循请求-确认握手协议。
    
     在所有的这些例程中，设计工程师企图匹配命题定义的行为来实现逻辑，但有时设计工程师会出错，而命题在这时则提供了一种交叉核查的方法；当设计工程师设计出来的行为与命题规定的行为不符时，命题就会发出报警。若在Verilog仿真时出现违反命题的情况，人们就非常希望能核查并报告这种违反命题的情况。
    
     除了仿真之外，命题也是形式或半形式验证工具要达到的验证目标。这些工具构造基于形式的数学模型，并采用推理技术来证明或反证设计工程师所期望达到的电路行为的特性。
    
     若验证工具发现了一种可以违反电路特性的方法，那么也就发现了电路设计中的某种缺陷。如果验证工具能够证明无法违反电路属性，那么就得到了有价值的验证信息。
    
     形式或半形式验证工具能够证明两个Verilog例程项目不能同时评估，或没有办法让状态机进行非法行为转换。工程师非常希望形式验证工具的目标特性与仿真中使用的命题相匹配。这使命题具体化并在利用形式验证方法之前的仿真过程中排除故障。进一步来说，如果仿真测试套件中包含某种违反命题的测试，则表明存在设计缺陷，要在进行形式的分析前改正这种缺陷。
    
     设计中的命题是“白盒”验证的一个极好的实例，因为它们能够将设计所期望的的内部行为具体化而不仅仅定义从设计输入到输出的端到端行为。在许多场合，包括上述几个实例，命题直接映射到内部设计结构，如状态机和存储器。
    
     除了核查表示设计缺陷的问题之外，对电路内部结构的命题提高了整个设计的可观测性和设计行为的能见度。对于一个大型设计的输出，人们不容易核查到深藏在电路设计内部的设计缺陷的作用，并且诊断及改正这种缺陷也非常耗时。最好在缺陷源头或接近源头处核查到缺陷，这些地方往往就是内部设计结构命题所报告的设计违规之处。
    [page]
    基本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”语句表示的特性。
    [page]
    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语言或其它的测试平台语言来写命题程序，通过P