验证高层综合操作流图等价性的一种有效形式方法

摘要：

根据当前高层综合系统不跨越控制边界进行代码移动的特点,提出了临界路径的概念,将行为规范与RTL实现的操作流图分解成模型检查工具可以接受的验证目标.为了便于自动验证高层综合过程,给出了验证自动机模型.实验结果表明,应用该方法,可简化状态空间,得到更高的验证效率,并保证规范与RTL实现的一致性.

关键词：高层综合、模型检查、临界路径、操作流图

所属期刊栏目：15

分类号：TP3;TN4

资助基金：国家高技术研究发展计划863计划2002AA1Z1190

在线出版日期：2005-03-31（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：7-11