顯示具有 SVA 標籤的文章。 顯示所有文章
顯示具有 SVA 標籤的文章。 顯示所有文章

2011年11月5日 星期六

排名前十的验证忠告

排名前十的验证忠告

1.这是遗留下的代码,所以不用验证
-小心!你能 100%保证你面对的是经过硅验证的代码吗?你能保证没有在上次工作之后
没有任何人碰过这代码吗?

2.我可以在 5 分钟内就把补丁加上
-只要你能保证你的验证环境不像是一大堆补丁堆在一起形成的,这样做到也可以。但
是想一下从今天起用一周时间来修改和修正你的验证环境是一件容易的事吗?难道多用几
分钟时间来写一个更健壮的代码不是更好吗?

3.随心所欲地计划和开始测试
-这是大大地错了!即使你的工作是小菜一碟你也要提前做好计划。你会惊讶地发现可
以避免多少无谓的问题。铭记 5 个 P:合适的计划排除差的性能。(proper planning prevents
poor performance)

4.这工作很简单,不必作测试计划
-将测试计划当作你的工作合同。你加入其中的定义了你当前所要做的工作,如果工作
真的很简单,就用半页纸把测试计划写下来。

5.验证不是产品,所以不必遵循软件标准
-验证的确不是产品,但是你仍需处理数千行的代骊,所以你最好可以确保一定程度的
一致性,更不用说可能存在代码错误的可能了。

6.别花时间在写注释上
-还记得最近一次你花费半天时间在反向研究别人的代码上吗?那么对于你自己写的代
码呢?更好的做法是,在开始每个测试前,保证代码中有足够的注释解释程序步骤,并要保
证注释的更新。

7.我知道了!让我们从外部强制这个信号的值就 OK 了
-强制的信号值往往会在整个流程中被遗忘,并在最后阶段才被发现,这时通常只有一周就
tapout 了!所以要极端的小心。

8.必须在后台一直运行回归运行(regression running)
-单纯的回归运行不能完成所有工作。你必须有一个分析人员(Regression Sitter)来监
视和分析运行结果-否则就是在白白磨损服务器!

9.我们己经实现了 100%的覆盖率真,所以没有必要再运行更多的测试了!
-实际上并不是这样。你的覆盖率模型只能捕捉到你提前想到的东西。很明显随机测试
平台可以产生能揭示出 bug 的额外情景。所以不要在 100%时停止。相反,要在这时加强覆
盖率模型。

10.验证应该寻找 bugs-这是一个很普遍的对验证工作的误解。验证者应该将注意力放在建立一个构建得很好的,强健和完整的测试平台上。bugs 将会自己被检测出来。

2011年10月20日 星期四

Digital Circuit Functional Verification(二十)

 验证工具總結

1. 尽管 Lint 和其他静态代码检查工具可能报告很多的伪错,但它们对于某些错误仍然是最
有效的检测工具。

2. 仿真器的好坏取决于被仿真的模型。同时仿真器还提供了许多提高仿真性能的选项,可以
支持联合仿真或者混合语言仿真。

3. 基于断言的验证对任何验证方法都是强大的工具,通过它可以很快地发现问题的位置和
发生时间。(SVA)

4. 硬件验证语言由于其对验证任务和覆盖率驱动的随机验证的支持,它对提高设计效率很有
帮助。(UVM, systemverilog, systemC...)

5. 由代码和功能覆盖数据可以对设计质量进行量化的评估。但要注意的是:不必付出所有
代价去达到 100% 的覆盖率,即使达到了预期的覆盖率目标也不能说明设计工作已经完成。
(spec. -> functional items -> function coverage -> code coverage)

6. 源码控制系统和问题追踪系统可以管理代码并报告错误。(Project manager 要試著與member 討論可行的作法)

2011年10月19日 星期三

Digital Circuit Functional Verification(十九)

METRICS 指标

指标是最基本的管理工具
管理者都希望看到
指标和报告,因为他们没有时间亲自跟踪项目的进展情况,而是根据一
些重要的
指标来掌握当前的情况。


指标可以评估验证的效果
很多
指标都可以用来评估功能验证的状态、进度和效率,code coverage就是其中之一。


code coverage并非适合所有情况
代码覆盖测试的是源代码被验证的程度,一般它会随着时间的流逝和设计的进展不断增
加,最终趋向 100%。


并不是所有的项目都适合用代码覆盖率来评估。代码覆盖率对于独立的小的设计单元
是有效的
(例如,FPGA、ASIC 或可重复利用的元件),但却不适于由单独验证过的模块构成的大型设计项目。验证这些大型设计的目的是为了检查各个模块的接口是否正常工作,而不是验证每个模块的功能,因此没必要运行所有的语句。



测试用例的代码行数可以反映测试效率
执行验证过程所需的代码行数可以有效地反映执行该过程的代价,所以可以用它来比较新
的验证语言或方法的效率。如果新方法能减少需要编写的代码行数,那么它也可以降低验证过
程的花费。


代码行的比率可以反映设计的复杂性
被验证的设计的代码行数与测试用例的代码行数的比率可以反映设计的复杂程度,这个比
率还可用于预测某个新设计的复杂度和验证花费。



版本控制系统可以了解到随时间变化的源代码修改程度。在项目的初期,随着新功能的
不断加入和版本的变化,代码会以很快的速度变化。在验证的初期阶段,修复错误也会导致代

码的变化。而随着验证过程的进行,错误越来越少,代码的变化也不断减少。

 与品质相关的指标
品质是主观判断的,但可以通过测试指标来间接反映
与品质相关的
指标与功能验证的关系比其他指标与其的关系更加密切。虽然品质是主观
值,但它可以由与设计质量相关的
指标来反映,这就好比零售服务的质量可以由顾客投诉次数
和重复投诉的数量来反映。



功能覆盖(function coverage)可以反映测试用例的完整性
功能覆盖测试的是设计中观测到的输入、输出和内部信号的组合。对这些数据赋予不同的
权重,可以得到一个功能覆盖
指标,反映设计的功能被执行的程度。如果增加重要指标的权重,它还可以作为功能验证进展情况的一种度量。在项目的初始阶段,覆盖率以很快的速度朝着100% 的目标增长,随着项目的进行,由于存在一些难以达到的功能点,它的增长速度明显放慢。





最简单的指标就是已知问题的数目
最容易收集的数据就是未解决的问题的数量,在统计时可以把问题的重要程度作为权重。
在使用计算机化的问题追踪系统时,可以很容易地得到这个
指标以及它的趋势和变化速率,由
此可以判断问题是在不断增加还是在减少并趋向于零?



 解释指标
用什么来评估已经完成的工作
管理者在很大程度上依靠
指标来判断设计者的工作业绩(作为奖惩的依据),这导致所有
设计人员都十分关注
指标,也是为什么要慎重选择那些可以客观反映当前情况和所付出的努力
指标的原因。如果评估的是已发现和修改的错误数,你很快会看到这个数目在增加,但你会
看到代码的质量在提高吗?错误以前没有被报告吗?如果只要有效地发现并修改错误就能得到
管理者的肯定,这会不会导致设计者编写代码时过于马虎和草率呢?



2011年10月15日 星期六

Digital Circuit Functional Verification(十五)

斷言ASSERTIONS


Simulation Assertions 
簡單來說就是利用簡單的語義描述來驗證signals protocol
而這個驗證語法是基於一個或多個clock來確認signals之間的關係

断言被分为两大类:一类是由设计者定义,另一类由验证工程师定义。
● 由设计者定义的设计断言(Implementation Assertion)
    通常寫成embedded Mode,而嵌入到RTL中,因為Assertion 不會被合成
● 由验证工程师定义的规范断言(Specification Assertion)
   通常會使用blockbox方式來驗證design,常放在design的外部

由於assertion只能指出錯誤,但不能指出少驗了那些項目
因此必須搭配code coverage相關的方法來使用


Formal Assertion Proving
Formal tools called model checker or assertion provers can mathe-
matically  prove that,  given an  RTL design  and  some  assumptions
about the relationships of the input signals, an assertion will always
hold  true.  If a counter  example  is  found,  the  formal  tool  will  pro-
vide  details  on  the  sequence  of events  that leads  to  the  assertion
violation. It is then up to you to decide if this sequence of events is
possible, given additional knowledge about the environment of the
design.

 形式验证领域将这些输入断言称为约束(constraint),这里作者使用术语“假设”(assumption)将其与随机发生
的约束区分开来,后者是一种随机的概念。

這個驗證觀念在2008之後似乎不再有人再提了,

現在的觀念應該是
Formal verification就用formal tools(LEC, formality)之類來作靜態驗證
Assertion就用SVA, PSL, OVL之類來作動態驗證

另一種原因可能是OVM/UVM的出現,而random input及constraints在其中的使用

2011年7月8日 星期五

SVA 再了解(十)

bind的使用

先看一下bind的語法

先寫一個給bind用的module
module mutex_chk(a, b, elk);
input logic a, b, elk;

property p_mutex;
©(posedge elk) not (a && b);
endproperty

a_mutex: assert property{p_mutex);
endmodule

假如有一個design如下
module t o p {. . ) ;
inline ul (elk, a, b, inl, in2, outl);
inline u2 (elk, c, d, in3, in4, out2);
endmodule

我們可以在design上加入下面的bind作check
bind top.ul mutex_ehk il(a, b, elk);
bind top.u2 mutex_ehk i2(c, d, elk);

2011年7月7日 星期四

SVA 再了解(九)

SVA for Data Integrity in Asynchronous FIFO

int wcnt, rcnt;
always @(posedge wclk) if (write) wcnt = wcnt + 1;
always @(posedge rclk) if (read) rcnt = rcnt + 1;
property p_data_integrity;
int cnt;
logic data;
@(posedge wclk)
(write, cnt=wcnt, data=wdata) |=>
@(posedge rclk)
first_match(##[0:$] (read & (rcnt==cnt))) //$盡量不要用,會拖慢模擬速度
##0 (rdata==data);
endproperty

assert property (p_data_integrity);

2011年7月4日 星期一

Design and Verification Team Considerations

Designers should embed their assertions in the design near the RTL that’s
being tested.
– Easy to capture assumptions, expectations, and identify corner cases as the code is
written
Makes good documentation
Interface assertions should be in a verification component for reuse.
– The verification components can be instantiated in the test bench, or in an external
file.
Verification engineers should use external files for their assertions.
– Avoids conflicts with the designer
– Easily separated
Place coverage points in an external file or within an `ifdef directive.
– This allows the user to avoid the performance impact when coverage is not used.

SVA 再了解(八)

將SVA嵌入到Verilog design裡的一個例子



2011年7月3日 星期日

SVA 再了解(七)

$onehot() 與$onehot0()的例子

property OH;
@(posedge CLK)
($onehot(GRANT_VEC));
endproperty

property OH_ZERO;
@(posedge CLK)
($onehot0(GRANT_VEC));
endproperty

SVA 再了解(六)

一個檢查pipe的SVA例子

DATA_PIPELINE: assert property (
@(posedge clk) disable iff(!rst_n)
$rose(valid) |-> (##5 pipe_ready ##1 pipe3_data==$past(port_data, 2)
);

2011年7月2日 星期六

SVA 再了解(五)
























實際上,我們trace這個REQ的$rose,它的trigger 點是在CLK的edge上
,然後對REQ的上一個cycle到這個cycle的變化為rising時,視之為條件成立

SVA 再了解(四)

SVA 提供了 3 个内嵌函数,用于检查信号的边沿变化。

$rose(布尔表达式或信号名) 一個bit
当信号/表达式的最低位由 0 或 x 变为 1 时返回真值。

$fell(布尔表达式或信号名) 一個bit
当信号/表达式的最低位由 1 变为 0 或 x 时返回真值。

$stable(布尔表达式或信号名) 一個bit
当信号/表达式的最低位不发生变化时返回真值。

2011年7月1日 星期五

SVA 再了解(三)

使用序列的重复操作符进行检查

序列的重复操作符分为 3 类:连续重复,跳转重复和非连续重复。
“[*m]”为连续重复操作符。“a[*3]”表示 a 被连续重复 3 次,“a[*1:3]”表示 a 被
连续重复 1~3 次。连续重复的相邻两次重复之间只有一个时钟间隔。
連續訊號

“[->m]”为跳转重复操作符。“a[->3]”表示 a 被跳转重复 3 次,“a[->1:3]”表示 a
被跳转重复 1~3 次。跳转重复的每一次重复之前可以有任意个时钟周期的间隔。
像pulse或連續訊號

“[=m]”为非连续重复操作符。“a[=3]”表示 a 被非连续重复 3 次,“a[=1:3]”表示 a
被非连续重复 1~3 次。非连续重复的每一次重复之前可以有任意个时钟周期的间隔,最后一
次重复之后可以有任意个时钟周期的间隔。
像pulse一樣的,全部都是斷續的

property cons_rep_p;
@(posedge sclk) $rose(a) |-> ##1 b[*3] ##1 c;
endproperty

property goto_rep_p;
@(posedge sclk) $rose(a) |-> ##1 b[->3] ##1 c;
endproperty

property non_cons_rep_p;
@(posedge sclk) $rose(a) |-> ##1 b[=3] ##1 c;
endproperty

SVA 再了解(二)

|=>與 |->的不同

|=>
非交叠蕴含操作符“|=>”表示:如果先行算子匹配,后序算子在下一个时钟周期开始计算。
The operator |=> means “then at the next clock
cycle”, and it is called non-overlapping suffix implication.

|->
交叠蕴含操作符“|->”表示如果先行算子匹配,后序算子在同一个时钟周期开始计算。
(operator |->, called overlapping suffix implication

2011年5月6日 星期五

SVA 再了解(一)

這是一個簡單的 SVA測試例
關於sequence 及property的用法

module test;

reg clk, rst_n;

wire ph1, ph2, ph3;

reg [1:0] ph_fsm;

reg vsync, vsync_d, vsync_start;

reg [9:0] ph1_cnt, ph2_cnt, ph3_cnt;

reg [7:0] phase_loop_cnt;
wire phase_loop_end;

parameter ph1_value =10;
parameter ph2_value =15;
parameter ph3_value =35;

always #5 clk = ~clk;

initial begin
clk =0;
vsync = 0;
rst_n =1;
#100;
rst_n =0;
#100;
rst_n =1;

@(posedge phase_loop_end)
vsync =1;

@(posedge phase_loop_end)
vsync =0;

end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph_fsm <=0;
else begin
if (ph_fsm ==0)
ph_fsm = 1;
else if (ph_fsm == 1 && ph1_cnt == ph1_value)
ph_fsm =2;
else if (ph_fsm == 2 && ph2_cnt == ph2_value)
ph_fsm =3;
else if (ph_fsm == 3 && ph3_cnt == ph3_value)
ph_fsm =1;
else
ph_fsm = ph_fsm;

end
end

assign phase_loop_end = (ph_fsm ==3 && ph3_cnt==ph3_value);

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph1_cnt <= 1'b0;
else if(ph_fsm == 2'b01)
ph1_cnt ++;
else
ph1_cnt <= 1'b0;
end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph2_cnt <= 1'b0;
else if(ph_fsm == 2'b10)
ph2_cnt ++;
else
ph2_cnt <= 1'b0;
end

always @(posedge clk or negedge rst_n) begin
if (~rst_n)
ph3_cnt <= 1'b0;
else if(ph_fsm == 2'b11)
ph3_cnt ++;
else
ph3_cnt <= 1'b0;
end

assign ph1 = (ph_fsm == 2'b01);
assign ph2 = (ph_fsm == 2'b10);
assign ph3 = (ph_fsm == 2'b11);

initial begin
$fsdbDumpfile("./test.fsdb");
$fsdbDumpvars(0, test);
$fsdbDumpSVA(0, test);
end

initial begin
#1ms;
$finish;
end

sequence s_ph12_chk_seq;
@(posedge clk) ph1 [->ph1_value] ##1 ph2;
endsequence

sequence s_ph23_chk_seq;
@(posedge clk) ph2 [->ph2_value] ##1 ph3;
endsequence

sequence s_ph31_chk_seq;
@(posedge clk) ph3 [->ph3_value] ##1 ph1;
endsequence

property p_ph1231_chk1;
@(posedge clk) $rose(ph1) |-> ##ph1_value $rose(ph2) |-> ##ph2_value
$rose(ph3) |-> ##ph3_value ph1;
endproperty

property p_ph1231_chk2;
@(posedge clk) s_ph12_chk_seq |-> s_ph23_chk_seq |-> s_ph31_chk_seq;
endproperty

ph1231_chk_sva1: assert property (p_ph1231_chk1)
else begin
$display("\n Fail in ph1231 sva1\n");
#1000;
$finish;
end

ph1231_chk_sva2: assert property (p_ph1231_chk2)
else begin
$display("\n Fail in ph1231 sva2\n");
#1000;
$finish;
end

endmodule