有多少方式解决问题吗?
它已成为一个历史悠久的传统OneSpin构成一个假日难题的挑战,工程师无处不在。去年,我们要求你解决著名爱因斯坦的谜语使用断言和正式的工具:这是一个巨大的成功。2017 - 18假期,我们问你来解决最难的数独在世界上,并证明解决方案是独一无二的。我们很高兴,更加热情的工程师们分享他们的专业知识和提交大量的整洁和快速的解决方案。
检查OneSpin假期拼图,点击这里。
今年我们计划奖三个奖项:
如果你不喜欢阿斯泰里克斯从法国,广受欢迎的漫画系列,这些名字是受三次著名的不屈不挠的高卢人的冒险。在我们稍微扭曲的解释,从和他的朋友们使用一个正式的药水,给他们一个超人的力量抵抗占领一群卑鄙的bug。
解决难题是有趣的,你可能会想,确保你享受比赛是我们的首要任务。它也提高我们的逻辑思维能力,能够审查一系列高质量的解决同样的问题是一种罕见的,极其宝贵的学习机会,尤其是当一个人有事先走的难题。
使用RTL代码编写数独和断言不是一个经验丰富的工程师非常具有挑战性的任务,但它仍然需要大量的思考和决策。就我和我确信我不是唯一一个双重检查,解决方案是正确的。我经历了几个迭代,试图想出更多的可重用和可读的代码。
OneSpin 360 DV-Verify屏幕截图显示了解决数独的挑战。
除了具体目标你可以,编码风格是受建立最佳实践和个人喜好的影响。首先选择的是语言。提交大部分来自欧洲和北美,超过80%使用SystemVerilog RTL代码和断言。我们还收到了提交使用硬件描述语言(VHDL),和一些使用PSL或ITL断言。ITL代表间隔语言和OneSpin专有的断言语言。
另一个选择有显著影响编码风格是辅助建模解决方案实现的RTL代码,和编码是多少直接断言和假设。一些工程师更愿意编写简单的属性和转变成造型RTL复杂性。
我们2017 - 18假日难题问工程师证明给定的数独游戏只有一个解决方案。值得注意的是,虽然模拟器与约束求解器可以用来找到一个有效的解决方案,只有一个正式的工具可以快速、轻松地证明解决方案是独一无二的。正式的工具本质上是彻底的,他们对模拟器的关键区别。
必须证明解决方案的独特性也给予我们机会去观察不同的编码选择。你们中的一些人选择了一种组合的方法,基于实例化的核心解算器两次,证明实例都产生相同的解决方案。其他人去顺序的方法,基于证明一个解算器总是随着时间的推移产生相同的解决方案。
一些参与者在运行时的挑战,给这个目标最高优先级。编码选择在运行时产生巨大影响:一些解决方案需要超过10秒的CPU时间,而其他人,包括魔毯,用不到0.1秒。
这里是获奖者:
我们还决定增加一个额外的奖:
你好,很高兴你今年所做的另一个难题。去年很有趣和教育。我的解决方案需要3.5秒证明独特性,所以我怀疑这将是最快的,这不是特别值得一读的,所以我相信它会不了奖,但我真的想支持参与。欢呼,安东尼
所有四个赢家将获得一个亚马逊回声+和可以用它来实现声控数独。
明年,我们有新的想法,不仅对谜题还对挑战的格式。如果你有反馈或建议分享,请电子邮件我们(电子邮件保护)。我们希望接到你的电话。
感谢所有的参与者。请继续关注今年晚些时候在接下来OneSpin节日难题!
|
|
|
|
|
|
|
|
|
|
留下一个回复