上广电为连续数据输入假设/断言

我是一个基于断言的验证新手试图了解它应该如何正确完成。我发现了很多关于systemverilog +断言的结构和技术细节的信息，但是我仍然没有找到一些关于真实世界中事情真正完成的“食谱”材料。上广电为连续数据输入假设/断言

的问题和制约因素：

设计具有数据输入总线与数据，有效和ID输入

Ñ
一个数据 “包” 是3个样品

后总会有来自频道的数据n + 1
- 频道ID将包装后的最大ID已发送
可以有数据字节之间蜱任何数量clk的
下面是与信道ID的简单，希望正确的时序图：

那么，你如何用最少的代码做ammount的呢？不错，干净。以前我构建了虚拟verilog模块来驱动数据。但肯定可以使用一些假设财产只是限制渠道ID，但其他方面留下空闲的手为正式工具试图制动我的设计？

对于初学者简单模板可以是：

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

我想问题是，假定/像上面断言倾向于触发每一个数据样本，并创建在时间上重叠的并行线程。

来源

2016-07-22 jarno

@MthetheTTaylor OP正在谈论形式验证。形式验证中的术语是，你对你的输入刺激进行假设，并且这些限制了它的合法状态空间。 –

@Tudor哦 - 就这样。我错过了。 –

您提供的示例不重叠。在具有相同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-22 13:21:35

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

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

如果您不提供任何假设，那么工具可以驱动任何随机数据并评估断言，在这种情况下，您可能会得到虚假篡改。这种情况被称为“约束下”。

同样，如果你提供了太多的假设，那么你可能会错过一些合法的输入组合。这种情况被称为“Over Constraint”。

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

对于你的情况，你的假设可能会有点像这样：

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);

在正式验证方法更详细的信息，请访问我的博客上说：What is Formal Verification? [1/2] & What is Formal Verification? [2/2]

来源

2016-07-22 17:26:06

你的命题限制了输入，所以如果有3个数据字节具有相同的ID，那么下一个ID将是前一个+1？但是它是否仍然让这个工具能够使用非连续的ID？我的意思是，对我来说，似乎上述假设并不真的禁止这样做。我不在工作的计算机上，所以我不能尝试。 – jarno

我认为它会引导工具生成连续的ID。但无论如何，为了检查确切的实现，我们需要通过工具本身运行它 –

我将定义三个sequence检测下一个有效的相同的ID（same_id）;在下一个有效的（change_id）上检测到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-27 02:08:29 AldoT

上广电为连续数据输入假设/断言

回答

相关问题