系统与设计
的意见

解决使用形式验证爱因斯坦的谜题

一个经典的逻辑谜题度假。

受欢迎程度

注意所有Sherlockians半导体行业!OneSpin解决挑战你在爱因斯坦的谜题智力测验和度过假期令人费解,使用你选择的形式验证软件的品牌。

三个遥控飞行的无人机将被授予三个最快解决方案执行正确的谜语OneSpin DV-Verify正式的验证软件。OneSpin将公布结果,促进他们在3月份DVCon。

爱因斯坦的谜题

据称爱因斯坦发明了谜语在1800年代末和表明,只有2%的世界人口可以解决它。虽然没有证据声称他是作家,它赢得了逻辑难题绰号“爱因斯坦的谜题。“当然,爱因斯坦没有获得正式的验证或脑力在我们的行业。无论如何,逻辑和演绎如福尔摩斯会采取和形式验证是所有你需要的解决方案。小学,我亲爱的难题。

这是谜语:五个房子在一个街道在五个不同的颜色。在每个房子住有不同国籍的人。这五个主人喝某种类型的饮料,烟一定品牌的雪茄,保持一定的宠物。没有主人有相同的宠物,支付相同的宠物,抽烟草的同一品牌或喝饮料。

问题是:谁拥有鱼?

一些额外的线索来帮助解决谜题:

  • 英国人住在红色的房子里
  • 瑞典人养的宠物狗一样
  • 丹麦人喝茶
  • 左边的绿房子是白宫
  • 绿色房子的主人喝咖啡
  • 抽烟的人蓓尔美尔街提出了鸟
  • 黄房子的主人抽登喜路香烟
  • 住在中间房子的人喝牛奶
  • 挪威人住在第一个房子
  • 抽烟的人混合住旁边的人一直猫
  • 旁边的人让马住抽烟的人登喜路香烟
  • 业主谁抽烟BlueMaster喝啤酒
  • 德国抽香烟王子
  • 挪威人住在蓝房子旁边
  • 吸烟的人有邻居饮料混合水

作为一个难题,你应该拿出一组属性在你最喜欢的形式验证工具或写出解决方案,应该工作。可以解决这个谜团的使用一个简单的Verilog或VHDL的形式验证模型和一些属性。

OneSpin将运行解决方案在DV-Verify奖无人机的三个玩家最快的解决方案。所有的提交必须周一收到,1月16日。应该发邮件提交:(电子邮件保护)

不要这样一个虚构的侦探福尔摩斯和华生医生或者坐在场边。相反,穿上你的猎鹿帽帽和亲手解决谜题。海泡石烟斗可选的。



留下一个回复


(注意:这个名字会显示公开)

Baidu