最早揭示有限状态机设计bug的代码开发阶段。
随着设计规模和复杂性的增加,设计验证的努力会更强大。需要花费大量的时间,彻底验证复杂的控制逻辑的设计,这是设计的关键和最重要的组件的功能。最常见的一种设计模式在控制逻辑设计有限状态机。他们可以在不同的风格设计,状态和输出逻辑编码,在复杂或简单的设计,维护和验证。使用“Design-for-Verification”是很重要的方法来开发有限状态机在一个简洁、稳定和容易证明的方式。
RTL代码产品毛羽是众所周知的方法确保设计符合业内的集合为硬件开发设计指南。此外,产品毛羽能够自动提取有限状态机结构设计规范和揭示了FSM的设计最早bug的代码开发阶段。
标准化FSM设计模式是RTL代码标准化的重要组成部分,广泛应用于许多芯片设计公司。线头工具正式验证代码遵守公司标准,避免设计评审和手工代码检查。线头工具检查各种FSM代码特性如:
线头工具自动识别FSM RTL代码和提取FSM结构,呈现在FSM图窗口。视觉设计师批准FSM设计意图回顾这些FSM图表。对于遗留代码,提取FSM图形作为设计规范,允许RTL代码的更好的理解和促进重用。下图演示了FSM图提取的线头工具:
FSM提取后,线头工具应用各种结构和功能检查,进一步验证FSM正确性和符合公司标准。例如,它是一个很好的实践,避免使用粉和混合FSM类型,喜欢摩尔FSM类型。摩尔FSM输出注册,因此他们不可能传播有限状态机FSM输入故障输出。摩尔FSM也可取从时间的角度来看,FSM输出时间路径包括输出解码逻辑。同时,这是一个很好的实践执行一个特定的状态编码类型,以更好地设计适合设计要求。例如,在一个炎热的编码与摩尔FSM高速设计类型是可取的,而灰色编码更好的低功耗应用程序,等等。
ASIC和FPGA合成工具需要synthesis-specific属性实现FSM根据设计意图。线头工具保证适当的synthesis-specific属性陪FSM的代码。
FSM提取后,线头工具功能验证所有的FSM激活做转换,使可能的FSM状态从一个状态转换到另一个。例如,一个过渡,例如:
如果(> 7)= StateA;
永远不会被执行,如果变量“a”定义宽度的3或更少。否则,FSM图提出了诸如non-activatable FSM转换为下图所示:
缺乏激活导致“正常”状态转换成为不可用或创建动态或静态的僵局。
FSM转换验证后,线头工具分析僵局,FSM结构冗余和遥不可及的状态。
死锁状态“冻结”的FSM没有输出转换到其他州。下面的例子显示了FSM的僵局“错误”状态:
在FSM结构提取,所有转换验证,线头工具检查没有死锁状态FSM描述。
而不是死锁状态,遥不可及的状态没有输入转换,使FSM要么不可能进入这些国家之一。在一些FSM的设计,只允许重置状态中遥不可及的情况下,它是设计运行时从未使用过以后。下面的例子显示了FSM和遥不可及的“就绪”状态:
除了静态僵局,动态活动锁也可能存在于有限状态机。动态活锁代表不是单一的状态,而是FSM的状态。一旦进入,FSM离不开这群,继续循环群之间的状态。下面的例子显示了FSM和动态活锁,代表的州(S2、S3、S4):
线头工具的使用是非常重要的发展的关键任务的设计。这些设计应该完美地工作在任何PVT (process-voltage-temperature)变化,抵抗过度辐射水平和老化。一个FSM安全特性是能够恢复状态机的一个安全的状态,如果状态寄存器就会败坏。线头工具提供这样的检查,确保总是有一个默认的FSM描述分支语句,和所有默认的执行分支语句导致安全状态(s)。
对安全性要求苛刻的设计必须完美。例如,RTCA / - 254,为机载电子硬件、设计保证指导定义组需要遵循的指导方针,以确保完美和飞机的安全运行。让有限状态机等的设计,完美的高重要性通常有限状态机控制逻辑设计的重要部分。线头工具有助于保证设计FSM的完美操作逻辑。设计师可能配置线头工具只允许一个完美类型的有限状态机,例如:
以下图片代表的结构完美FSM类型详细:
总之,线头工具能够验证僵局,洛夫洛克,可达性以及许多其他FSM-related问题最早设计阶段,节省检验时间和消除可能的功能和实现的缺陷。建议使用他们开发有限状态机在RTL代码直接静态验证所提供的线头工具。FSM提取线头工具提供的功能可以用于更好地理解遗产或第三方RTL代码。对高安全性的设计时,线头工具有助于确保FSM代码安全根据安全标准要求。如果你想尝试验证FSM-related问题,只是从我们请求一个免费评估ALINT-PRO。
|
|
|
|
|
|
|
|
|
|
留下一个回复