【摘 要】
：
利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将
【基金项目】
：
本课题得到国家自然科学基金（60403048,60573173）资助.
论文部分内容阅读
利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.
其他文献
根据发电企业生产管理特点，设计了一套完整的生产实时监管系统。系统集成了生产过程实时监控、运行重要事件自动监视和报警、性能计算与经济分析、重要指标在线对比分析、综合
3月22日-23日，中电装备公司2012年信息化工作会议在北京顺利召开。国家电网公司信息通信部吴杏平副主任、装备公司副总经理、党组成员巩学海等同志亲临会议现场，公司信息化工作
国家电网公司信息化SG186工程项目通过国家级评审——总体达到国内领先和国际先进水平2010年2月25日．国资委在京组织召开国家电网公司信息化SG186工程项目评审会。评审委员会
基于比较的诊断是多计算机故障诊断的一种实用方法.M（o）bius立方体是超立方体结构的一种变形,具有并行处理所需的某些性质.文章在MM＊比较模型下研究了M（o）bius立方体的诊断问题.利
4月20日，甘肃省电力公司为积极推进信息系统运行方式管理工作，加强运行总结分析和需求预测，在公司范围内首次开展网络与信息系统运行方式的编写工作。
SoPC(片上可编程系统,System on a Programmable Chip)在嵌入式系统中有着广泛的应用,通常用FPGA(现场可编程门阵列,Field Programmable Gate Array)实现.一类嵌入式处理器,
2009年4月18—19日，由中国地理学会主办，教育部人文社科重点研究基地河南大学黄河文明与可持续发展研究中心、河南大学环境与规划学院承办的‘‘全球金融危机背景下的中国城市
本文在追溯中国资源型城市发展历史背景的基础上，选取1952、1984、1990和2004年四个时段我国届存的资源型城市，从城市数量、类别和空间格局的变化，比较系统地揭示了我国资源型城
学界坊下戏言凡举“名士”善长脾气，吴传钧先生在我们心目中犹如智者弥勒。2008年4月2H在学界蜂拥北京纪念吴传钧先生90华诞之际，《人文地理》编辑部特制《学科泰斗》四字的古
结合昆明供电局的现状,应用项目管理的方法,探索出一条适合企业实际的信息系统项目管理新路。运用项目人力资源管理、项目进度控制和项目质量管理等手段,顺利完成了企业信息