2

我是一个基于断言的验证新手，试图了解它应该如何正确完成。我已经找到了很多关于 systemverilog + 断言的结构和技术细节的信息，但我仍然没有找到某种关于在现实世界中如何真正完成事情的“食谱”材料。

问题和限制：

  • 设计有一个带有数据、有效和id输入的数据输入总线
  • 一个数据“包”是3个样本
  • 在通道n之后，总会有来自通道n+1的数据
    • 频道 ID 将在最大 ID 发送后回绕
  • 数据字节之间可以有任意数量的 clk 滴答声

  • 下面是带有通道 ID 的简单且希望正确的时序图：

    在此处输入图像描述

那么如何用最少的代码做到这一点呢？干净整洁。以前我已经构建了虚拟 verilog 模块来驱动数据。但是可以肯定的是，可以只使用一些假设属性来限制通道 ID，否则可以腾出手来让正式工具尝试破坏我的设计？

初学者的简单模板可以是：

data_in : assume property (
  <data with some ID>[=3]
  |=>
  <data with the next id after any clk tick>
);

我想问题是像上面这样的假设/断言往往会在每个数据样本上触发并创建时间重叠的并行线程。

4

4 回答 4

2

相信您在谈论形式验证方法。

对于形式验证，您不需要构建任何模块来驱动激励。但相反，刺激将由工具本身驱动，您可以使用假设属性引导工具生成合法刺激。

如果您不提供任何假设，则工具可以驱动任何随机数据并评估断言，在这种情况下，您可能会得到错误的证伪。这种情况称为“受约束”。

同样，如果您提供太多假设，那么您可能会错过一些合法的输入组合。这种情况称为“过度约束”。

因此，提供准确的假设非常重要。

对于您的情况，您的假设可能看起来像这样：

property channel_change;
  // To check the next consecutive ID, after data transfer
  @(posedge clk)
  (id) throughout (valid [=3]) |=> valid && (id == $past(id) + 1)
endproperty

assume property (channel_change);

有关形式验证方法的更多详细信息，请访问我的博客：什么是形式验证？[1/2] &什么是形式验证？[2/2]

于 2016-07-22T17:26:06.437 回答
1

我将定义三个sequence来检测下一个有效 ( ) 上的相同 id same_id；检测id下一个有效 ( change_id) 的变化；并检测有效数据包 ( packet_id)。然后我可以在四个内监控一个属性valid，只有三种可能的情况：即

case1: (id, id,   id,   id+1) OR 
case2: (id, id+1, id+1, id+1) OR
case3: (id, id,   id+1, id+1)

请在下面查看我的代码。我没有测试过，这只是我的想法。希望它会奏效。好消息是property只会持续 4 个时钟滴答，并且在每个时钟滴答中，只有一个线程。所以我们可以避免线程爆炸。

// To detect same id within two non-consecutive valid,
// (a,a)
sequence same_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence


// To detect valid packet
// (a,a,a)
sequence packet_id;
  int prev_id;
  @(posedge clk)
  same_id, prev_id=id ##1 valid[=1] ##0 id==prev_id;
endsequence   

// To detect any change of ID
// any (a,b)
sequence change_id;
  int prev_id;
  @(posedge clk)
  valid, prev_id=id ##1 valid[=1] ##0 id==prev_id+1;
endsequence

// Put all together, in any four non-consecutive valid, there are only three cases: a,b,b,b OR b,b,b,c OR a,a,b,b
property next_id;
  int prev_id;
  @(posedge clk)
  (change_id ##0 packet_id) or         // a,b,b,b
  (packet_id ##0 change_id) or         // b,b,b,c
  (same_id ##0 change_id ##0 same_id); // a,a,b,b
endproperty
于 2016-07-27T02:08:29.323 回答
1

您提供的示例不重叠。在三个具有相同 ID 的样本之后，一旦另一个具有下一个 ID 的数据样本到来，结果将匹配并且整个属性将保持。

无论如何，有重叠的尝试是生活中的事实。工具总是在每个时钟周期评估（断言或假定）属性，以确定是否可能匹配。如果它确定是，则开始新的尝试；如果没有，它会继续前进。没有办法说“当它已经被尝试时不要尝试考虑这个断言”，因为你永远不知道尝试是否会在匹配中结束。

当看像你画的那个波浪时，很明显你不需要在三个样本中评估属性，但这仅仅是因为你可以看到整个画面。这类似于能够预见未来的工具。

继续讨论您的具体问题，但是，您的约束并不能说明全部内容。它只是说明一旦有 3 个具有相同 ID 的样本出现，下一个样本的 ID 应该递增。这里没有说样品必须以 3 个一包的形式提供。您需要以下内容：

assume property (
  sample_with_some_id_came |->
    came_out_of_reset_and_no_samples_were_sent.triggered or
      one_or_two_samples_with_same_id_sent_after_reset.triggered or
      three_samples_with_the_previous_id_sent.triggered
);

我也不确定您的假设是否会导致某种“无休止”的行为，因为您说在 3 个具有相同 ID 的样本之后必须始终有下一个样本。

于 2016-07-22T13:21:35.840 回答
0 
assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> (valid[->1] ##0 id == $past(id,,valid))[*2] ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));

分解它：蕴含的前因要么有效发生了两次，并且当前 id，在有效完成两次变高的时间步长（[->] 而不是 [=]），与最后一次有效变高的 id 不同：

((valid[->2] ##0 id != $past(id,,valid))

或有效在 rst 之后立即变高：

($fell(rst) ##0 valid[->1])

暗示的结果（在先行匹配后开始一个时钟 |=> ）从两个匹配的 valid 变高和 id == 前一个 id 开始（当 valid 为高时）。这必须匹配两次 [*]。

(valid[->1] ##0 id == $past(id,,valid))[*2]

并以下一个周期结束，valid 在某个时刻变高，当它变高时，id 必须等于前一个 id（当 valid 为高时）+1。

##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1))

这个假设允许 id 在有效低时改变 - 但仍然要求 id 在 3 个有效高周期内相同。

如果您希望 id 在整个有效时间内保持稳定，您可以使用以下命令：

assume property (@ (posedge clk) disable iff (rst) ((valid[->2] ##0 id != $past(id,,valid)) or ($fell(rst) ##0 valid[->1])) |=> ($stable(id) throughout valid[->2]) ##1 valid[->1] ##0 (id == $past(id,,valid) + 2'd1));
于 2019-11-14T19:09:24.533 回答