UPPAAL中的模型检查同步电路答案

【问题标题】：Model checking synchronous circuit in UPPAALUPPAAL中的模型检查同步电路
【发布时间】：2017-01-17 06:02:48
【问题描述】：

我正在使用 UPPAAL 模型检查器在门级对同步电路进行建模，我对如何对时钟进行建模有些困惑，我的目标是验证设置时间和保持时间没有被违反。我发现一些模型在 appal 模型检查器中将时钟作为测试向量，例如 t=10 相当于上升沿，而 t=20 是下降沿，这使它看起来更像一个测试向量。任何人都可以提出一个关于如何在 UPAAL 中模拟同步电路的基本示例吗？

谢谢

【问题讨论】：

您需要熟悉定时自动机，请查看 Uppaal 教程。如果您可以提供时序图，那么将其建模为具有一些时钟保护和不变量的状态机是非常简单的。
感谢 @mariusm 的回答，我查看了 UPPAAL，不确定时序图如何提供帮助，我实际上正在努力在门级建模 D 触发器，并验证设置时间和保持时间，但是在为时钟建模时，我很困惑如何将其建模为自动机，因为到目前为止我发现的最好的事情是将时钟作为测试向量，例如 8 个状态例如模型对应于 8 个上升沿，这更有可能是一个测试向量，我不知道我如何才能获得时钟空间，所以我可以在每个上升沿验证 D 触发器的行为。
我不明白“测试向量”部分。至于同步时钟，您需要建模一个进程，该进程在（广播）通道rise 和fall 上以给定的时间（由使用clock 变量的守卫和不变量建模）发出，然后其他连接的组件将监听到这些频道并相应地更新它们的状态。

标签： synchronous digital circuit model-checking uppaal

【解决方案1】：

在声明中这样写：

clock t;
broadcast chan rise, fall;

那么 Uppaal 中的同步时钟将如下所示：

那么其他连接的组件应该使用rise? 和fall? 作为边缘同步来监听。

【讨论】：

感谢 mariusm 的解释，我真正感到困惑的部分是我的 D 触发器输入，我有一个 D 触发器行为的模型，但我不知道如何对 D 触发器输入进行建模，或者我将其建模为每次在 0 和 1 之间切换的 2 个状态自动机（考虑到延迟），或者我将其作为第一个“0_logique”状态将保持 X 时间然后下一个“ 1_logique" 状态将保持 X 时间，特别是我需要输入以尊重时钟的设置时间和保持时间。
@HachaniAhmed，你很可能需要更多的中间状态。从两个位置开始，然后在输入建模需要发生的情况时为每个事件添加边。继续添加边，直到所有位置都可以随时处理任何输入。在中间状态可能需要一些等待时间（用不变量和守卫模拟等待）——这有点乏味，但这是正常的，因为实际的电子设备也是非瞬时的，需要一些时间来改变状态。