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

An Efficient Method for Verifying the Equivalence of Operating Graph During High Level Synthesis

作　　者：王彬[1] 林争辉[1] 

机构地区：[1]上海交通大学电子工程系，上海200030

出　　处：《高技术通讯》2005年第1期7-11,共5页Chinese High Technology Letters

基　　金：国家高技术研究发展计划(863计划)

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

关 键 词：形式方法 自动验证 模型检查 RTL 图分解 代码 自动机模型 高层综合 移动 状态空间 

分 类 号：TN911.72[电子电信—通信与信息系统] TP311[电子电信—信息与通信工程]