基于断⾔的可验证性RTL设计
基于断⾔的可验证性RTL设计
断⾔(声明，asrtion)并不是⼀个新的概念，在软件设计中，断⾔早已得到了⼴泛的应⽤，它可以帮助软件⼯程师在软件开发及测试过程中更早更快的发现、定位出软件中存在的错误。例如在JAVA中定义了⼀种断⾔的语法：asrt
Expression1:Expression2，当程序运⾏到这个断⾔，如果Expression1的值为假，则程序会报错，并根据Expression2给出相应的错误信息。许多JAVA⼯程师都认为断⾔是最快也是最有效的测试⽅法。现在同样的概念越来越多被引⼊到硬件及SOC设计中。
断⾔是⼀种⽩盒验证技术，所谓的“基于断⾔的可验证性RTL设计”是指设计师可以利⽤完整的断⾔验证(ABV)⽅法在开发RTL 时编写断⾔，⼀旦设计错误发⽣，断⾔能⽴即探测到，⽆需等待错误结果传递到设计边界，这省去了查找和定位错误的好多时间，提⾼了被验证芯⽚的可观察性和可控制性。当致命错误发⽣后，断⾔可以终⽌错误、节省模拟时间。
有四种定义断⾔的⽅式：开发验证库定义宣称性断⾔，Verilog断⾔构造定义过程性断⾔，还可⽤形式特征语⾔或伪注释指⽰定义，具体描述可以参阅附录⼀《数字芯⽚设计的断⾔验证》。
本⽂将介绍如何⽤ModelSim进⾏OVL宣称性断⾔设计验证。OVL是基于Verilog的开放源码的断⾔监督元件库，以相同⽅式在RTL中定义静态和动态断⾔；提供统⼀的消息
报告机制；易于定制；提供⼀致安全级别，发⽣严重错误时可以停⽌模拟。由于源码开放，能够根据应⽤进⾏定义，因此OVL 很吸引⼈。OVL使⽤断⾔模块库，因此在设计中必须实例化断⾔。⽬前它还⽆法定义过程性断⾔。
把ovl⽬录下的50个.v⽂件、7个.h⽂件和1个vlog95⽬录拷贝到ModelSim项⽬⽬录下，这些是Accellera组织于2008年最新发布的适⽤于Verilog仿真器的Open Verification Library V2.0 (OVL)，可以从⽹站
/doc/97822e156c175f0e7cd13716.html 下载最近的版本进⾏更新。现以断⾔语句ovl_always为例进⾏使⽤说明。
坚持才能成功Syntax
ovl_always #(verity_level, property_level, msg, coverage_level, clock_edge, ret_polarity, gating
_type)
instance_name(clock, ret, enable, test_expr, fire);
Description
The ovl_always asrtion checker checks the single-bit expression test_expr at each active edge of clock. If test_expr is not TRUE, an always check violation occurs.
Parameters
verity_level: verity of the failure, default is `OVL_ERROR
`OVL_FATAL 显⽰FATAL信息OVL_FATAL:…并经过⼀定时间后停⽌模拟
// ovl runtime after fatal error
`define OVL_RUNTIME_AFTER_FATAL 100
`OVL_ERROR 显⽰ERROR信息OVL_ERROR:…
`OVL_WARNING 显⽰WARNING信息OVL_WARNING:…
`OVL_INFO 显⽰INFO信息OVL_INFO:…
property_level: A checker’s “property type” determine whether to u the asrtion as an asrt property or an assume property (a property that a formal verification tool us to determine legal stimulus). The property type also lects whether to asrt/assume X/Z value checks or not. Default is `OVL_ASSERT
`OVL_ASSERT Asrt asrtion check and X/Z check properties.
check and X/Z check properties.
asrtion
`OVL_ASSUME Assume
`OVL_IGNORE Ignore asrtion check and X/Z check properties.
`OVL_ASSERT_2STATE Asrt asrtion check properties. Ignore X/Z check
properties.
`OVL_ASSUME_2STATE Assume asrtion check properties. Ignore X/Z check
properties.
msg: The default value of `OVL_MSG_DEFAULT is “VIOLATION”. Changing this define provides a default message printed when a checker asrtion is violated.
coverage_level: A checker’s “coverage level” determines the cover point information
reported by the individual checker. This parameter can be any logical bitwi-OR of the defined cover point type values, for example `OVL_COVER_BASIC | `OVL_COVER_CONER
`OVL_COVER_NONE Disable coverage reporting.
`OVL_COVER_SANTITY Report SANITY cover points.
`OVL_COVER_BASIC Report BASIC cover points.
`OVL_COVER_CONER Report CONER cover points.
`OVL_COVER_STATISTIC Report STATISTIC cover points.
`OVL_COVER_ALL Report information for all cover points.
clock_edge:
`OVL_NOEDGE
`OVL_POSEDGE Rising edges are active clock edges.
`OVL_NEGEDGE Falling edges are active clock edges.
`OVL_ANYEDGE Both rising and falling edges are active clock edges.
ret_polarity:
`OVL_ACTIVE_LOW Ret is active when FALSE.
`OVL_ACTIVE_HIGH Ret is active when TRUE.
gating_type: A checker’s “gating type” lects the signal gated by the enable input.
`OVL_GATE_NONE Checker ignores the enable input.
`OVL_GATE_CLOCK Checker paus when enable is FALSE. The checker treats the
current cycle as a NOP. Checks, counters and internal values
梦幻西游合宠攻略remain unchanged.
`OVL_GATE_RESET Checker rets when enable is FALSE.
output fire[2:0]: Asrtion failure when fire[0] is TRUE. X/Z check failure when fire[1] is TRUE. Cover event when fire[2] is TRUE.
Example
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// tb_asrt_always.v
module tb_asrt_always();
reg ret_n, clk;
reg[7:0] count;
常见的写作手法
wire clr;
wire[2:0] fire;
always @(podge clk)
count <= (~ret_n || clr) ? 8'b0 : (count + 8'd1);
assign clr = (count >= 8'd143) ? 1'b1 : 1'b0;
`ifdef OVL_ASSERT_ON
ovl_always #(
`OVL_ERROR,
`OVL_ASSERT,
"ERROR: count > 15",
`OVL_COVER_CORNER,walk是什么意思
`OVL_POSEDGE,
`OVL_ACTIVE_LOW,
`OVL_GATE_CLOCK)
chk_cnt(
clk,
ret_n,
1'b1,
count <= 8'd15,
fire);
`endif
initial begin
clk = 0;
ret_n = 0;
电子商务报告
#7 ret_n = 1;
end
always begin
#5 clk = ~clk;
end
always @(podge clk)
$monitor("At time %t, count = %d", $time, count);人物作文500字
endmodule
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
家公往事
/
///////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// # Copyright 1991-2007 Mentor Graphics Corporation
#
# All Rights Rerved.
#
# THIS WORK CONTAINS TRADE SECRET AND PROPRIETARY INFORMATION
# WHICH IS THE PROPERTY OF MENTOR GRAPHICS CORPORATION
# OR ITS LICENSORS AND IS SUBJECT TO LICENSE TERMS.
# U this run.do file to run this example.
# Either bring up ModelSim and type the following at the "ModelSim>" prompt:
# do run.do
# or, to run from a shell, type the following at the shell prompt:
# vsim -do run.do -c
# (omit the "-c" to e the GUI while running from the shell)
onbreak {resume}
# create library
if [file exists work] {
vdel -all
}工程地质条件
vlib work
# compile Verilog/VHDL source files
vlog +define+OVL_ASSERT_ON ovl_always.v tb_asrt_always.v
# open debugging windows
quietly view *
# start and run simulation
vsim tb_asrt_always
run 200 ns
//////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
在ModelSim Transcript窗⼝运⾏命令：
ModelSim>do run.do
结果显⽰为：
# ** Warning: (vdel-134) Unable to remove locked optimized design "_opt". Locker is grwu@PKU-3053CC107BA. # ** Warning: (vlib-34) Library already exists at "work".
# Model Technology ModelSim SE vlog 6.3d Compiler 2007.11 Nov 26 2007
# -- Compiling module ovl_always
# -- Compiling module tb_asrt_always
#
# Top level modules:
# tb_asrt_always
# vsim tb_asrt_always
# ** Note: (vsim-3813) Design is being optimized due to
# Loading work.tb_asrt_always(fast)
# Updating
# At time 5, count = 0
# At time 15, count = 1
# At time 25, count = 2
# At time 35, count = 3
# At time 45, count = 4
# At time 55, count = 5
# At time 65, count = 6
# At time 75, count = 7
# At time 85, count = 8
# At time 95, count = 9
# At time 105, count = 10
# At time 115, count = 11
# At time 125, count = 12
