形式验证技术出现在上升。似乎它已经存在永远,但现在发现进入比以往更加流动。

这是因为用户没有正式的技术。

正式的问题是它很难。从历史上看,投资正式被投资最佳匹配一个或两个博士帮忙。或者通过雇佣一些专家顾问帮助解决问题。我们已经开始摆脱这些束缚是通过应用程序。公司做正式的技术意识到他们必须目标具体问题,然后埋葬下面的正式部分用户界面和流程更自然的问题得到解决。

真正的意图已经做了一段时间,例如。你clock-domain穿越(CDC)解决方案。你有产品毛羽RTL的工具。您可以验证约束。等等。从底层一步删除正式技术使生活更容易为用户;正式的供应商负责映射的技术问题。

但是这里有一个很重要的问题:它的历史上只有正式工具供应商建立了这些应用程序,使用自己的正式技术。

假设你是一个系统房屋建筑一些专门的盒子。也许电子鼠捕手。(当然,连接到互联网,这样老鼠可以上传数据分析计算。)有许多传感器和电路控制当老鼠活板门关闭和打开。你想确保门是坚如磐石的逻辑控制,没有意外事件可能无意中打开门,释放一只老鼠,它不应该。

非常适合正式的工作。(我认为。跟我在这里工作。)但是,正如一个小角色在专业市场(从来没有过称之为一个利基当投资者),你的选择是什么?你可以投资工具和一个博士学位,但这可能会在你的预算。问题是,你不太可能能够说服一些正式的公司开发一个捕鼠器应用的市场,可能是一个公司。和一个小。

这种类型的机会OneSpin决定将值得一说。他们正在做它…它叫什么?开发工具包,也许…叫做发射台,它提供了非正式的公司来开发应用程序,使用正式的技术。第一个人:Agnisys,注册验证程序,龟岛的逻辑安全验证的应用程序。

设备本身由资源和一个API,这样开发人员可以构建用户界面和设计基础的方式正式技术杠杆。当应用程序出售,OneSpin的正式技术,包括螺栓,以及执照费OneSpin适用(除了价格应用程序提供商费用)。但是,如果买方已经OneSpin的工具,应用程序可以被放置在这些现有的工具,并没有额外的许可费用(但可能应用价格仍然适用)。显然这里的一些OneSpin增殖潜力。巧合吗?我不认为…

正式的游戏

然而,可能有滥用的可能性。假设一个完整的套件正式工具成本$ 30 k。(我不知道实际的定价——我用数字OneSpin旋转的讨论,其中包括一个假想的例子。)假设一个应用程序设计为k捕鼠器验证售价仅为10美元。然后假设你注意,应用程序通过将某些属性添加到RTL专门为捕鼠器验证,注释,这样应用程序可以识别哪些属性来验证。

好吧,这不是火箭科学意识到你可以完全的游戏系统。如果你有其他不相关的属性,需要验证一个更昂贵的通用的正式的工具,你可以手动捕鼠夹注释添加到你的所有属性来愚弄捕鼠器的应用验证,不仅捕鼠器的。你伪造的工具,这样你有30 k美元从$ 10 k的工具的价值。

我打电话这个“使命黑客。“很不错的骗局,不是吗?好了,不要太激动。他们已经到它。他们这些属性添加特定应用程序吗?是的,他们是加密的。所以你聪明的小计划不会工作。他们使用标准SystemVerilog加密、对称密钥交换(私人)安排OneSpin和应用程序之间的制造商。

虽然发射台与OneSpin的正式技术,它不是锁。作为一个应用程序制造商,你可以决定别人的正式的技术目标。但是,要做到这一点,有两个重要的事情需要做。

首先,您需要安排一个密钥交换和其他正式技术供应商。只要的平方,那么这将工作,因为加密标准。重申方式不同,加密不锁工具进入OneSpin因为它不是专有加密。它只是阻止黑客的任务。

先生们,选择你的引擎

你要做的第二件事是让您的其他正式供应商engine-picking引擎。原来这不是微不足道的。

你看,很容易认为正式的技术是这个庞大的野兽。喜欢点缀你的设计,然后你喂野兽的设计。它咬你的设计,给出一个答案。

嗯,显然这不是那么简单。正式的技术是关于跑步的证明。你想证明这个事实还是事实——通常是一系列的他们。所以设计成证明丁(甚至可以是抽象和运送云为解决)。但是我们大多数人不太明显的是有不同的引擎可以运行这些证明,和每个引擎擅长一种特殊的证据。

OneSpin给引擎的一些示例。两个熟悉的声音:坐(可满足性)和BDD(二元决策图)。还有BMC和克雷格(不管他是谁)和PDR然后神秘的“别人的东西。”+专有的引擎。

这不是应用程序开发人员可能会知道这引擎使用。所以OneSpin已经建立了一个引擎选择抽象问题。他们确实提供了一些灵活性,你如何解决这个,然而。这engine-picking业务并不都是事先准备好的。你可以设置它:

• 力一个明确的决定(发动机或发动机B);
• 设置首选项:首先试一试,如果不工作(过了一段时间),然后尝试B(然后C…);
• 按顺序运行A和B(和其他人)看到这提出了最好的答案。一个更好的版本,这是A和B并联运行,首先要了解哪个答案是收敛的。

(图片由OneSpin)

OneSpin说这花了不少令人挠头。所以任何其他公司,想抓住发射台需要为自己的工具解决这个问题。这绝对是可行的,并使用发射台OneSpin特意让人,不锁的人,但它确实需要努力实现适应不同的工具。

一般的好消息(正式)是,如果应用程序制造商选择这个发射台的东西,它可以把正式的解决更大范围的问题。软件制造商只需要专家在自己的领域,不是正式的技术。这有可能成为一个巨大的推动者。

更多信息:

OneSpin发射台

• 
• 
• 
• 
•