用以产生组成验证用自动假定值之方法、系统与电脑程式产品

摘要

本文揭露用于计算一精确最小自动机以作为假定－保证论证内的一中间声明之方法、系统及电脑程式产品。在一实施例中，该计算一精确最小自动机藉由使用一取样方法及一布耳可满足性而被执行。本文所描述的方法可被用作形式验证的一工具之部分。

主权项

一种用于产生一电子电路设计之组成验证的自动化假定值之电脑实施方法，包含以下步骤：使用一处理器进行以下动作：识别该电子电路设计的一第一集合及一第二集合之行为；至少部分地基于该第一集合及该第二集合之行为，迭代地计算一最小不完整确定性有限自动机(IDFA)；藉由自该最小IDFA归纳而决定一确定性有限自动机(DFA)，其中该DFA系藉由执行一学习程序以自该IDFA收集资讯而决定；以及将该DFA储存在一实体电脑可读媒体上或将该DFA显示在一显示装置上。