断言可以启用工程师设计正确的IP施工吗?
光阴似箭,OneSpin的传统节日难题已经达到第三年。2016年12月,OneSpin挑战工程师解决爱因斯坦的谜语使用断言和正式的验证工具。2017年12月,是模型的挑战最难的数独世界上使用断言和找到解决办法和正式的工具。此外,参与者必须证明解决方案是独一无二的,不可能与仿真。
对于我们的三周年,我们决定改变策略。2018 - 19 OneSpin假日难题挑战工程师设计一个计算的数字电路斐波纳契数。
查看最新OneSpin假日拼图,斐波那契计算器,点击这里。
我们计划授予三个奖项:
验证工程师知道有时功能需求没有实现在RTL代码以最直接的方式。虽然这可能会导致挫折和生成大量的功能性角情况下无法预见,往往是有原因的。设计师有很多目标和功能正确性显然是至关重要的,它不是唯一的一个。
旋回性能、时间、面积和功耗指标也很重要。找到正确的平衡需要创造力和实现的选择可能是更复杂的比一个期望或希望。最完美的例子是处理器。实现一个设计符合给定的指令集架构(ISA)相对比较容易。
一旦所有的其他目标发挥作用,事情就复杂了。设计师需要包括复杂的逻辑功能,如分支预测,投机获取、管道(多个超标量体系结构的微体系结构)和无序的执行。你见过多少不同吗RISC-V开源内核是可用的吗?
斐波那契计算器挑战迫使参与者关注电路复杂性和表演,而不是功能的正确性。然而,有一个清晰的要求表示SystemVerilog启用断言验证工程师,不断检查设计优化,包括旨在提高旋回性能变化,没有引入bug。
我们收到了来自世界各地的许多解决方案,从所有的人。虽然大多数提交正确的看着首先检查,一些显示错误断言检查时使用一个正式的工具。我的猜测是,这些参与者并没有获得一个正式的工具和依赖于模拟检查他们的设计,因此缺少一些角落的病例。
其他解决方案几乎是正确的,但未能满足断言集后重置。在我的职业生涯中,我使用了所有主要商用正式工具和知道一些可能包括default-implicit假设重置,可能掩盖真正的RTL的问题。
我的建议是仔细阅读工具的文档,即使是简单的设计只有一个重置,并使一些基本实验准确了解该工具处理SystemVerilog断言禁用条件和重置。
总的来说,这个练习告诉我们,可能有巨大的好处至少在形式化一些功能需求的前期和使用一个正式的工具来检查设计的成熟。所需的时间来验证优化并检查他们彻底可以削减,使快速迭代,可以节省几个月的努力。
几年前,我报告经验将这种方法应用到工业设计。
这里是获奖者:
今年的奖是一个Fortnum & Mason豪华阻碍,当然包括蜂蜜,或同等价值的凭证。
我们已经忙着找新想法在接下来的假期难题。发送你的建议(电子邮件保护)。
感谢所有的参与者。请继续关注今年晚些时候未来OneSpin假日难题!
|
|
|
|
|
|
|
|
|
|
留下一个回复