基于形式验证的多周期路径检测技术

来源 :计算机测量与控制 | 被引量 : 0次 | 上传用户:xyjslzy
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
多周期路径是将复杂电路运算拆分在多个时钟周期完成,从而提高电路总体运行频率的一种方法;在设计和验证中,多周期路径约束错误会导致设计迭代反复和验证误报;文章对多周期路径的产生机理和设计验证中常见的问题进行分类分析,提出一种用静态时序分析和形式验证结合来查找设计中的多周期路径的方法,首先通过静态时序分析,查找出时序违例的路径,针对这些路径,插入设计的检测电路,检测电路主要通过检测目的触发器采样控制信号有效时间,来判断该路径是否为多周期路径;采用基于断言的形式验证,用自动化的手段检测多周期路径;实践结果表明,该方法针对两种时钟下的多周期路径,能够100%准确地检测出违例的多周期路径,避免多周期路径错误约束,省略人工分析和动态仿真确认多周期路径环节.
其他文献
针对减压渣油储罐机械清洗中存在的问题,提出有效的改进措施.改进后水洗工期缩短39%,罐内废渣量减少97%,人员进罐施工作业时间降低93.7%;同时,在安全管理难度、罐内作业时间、环保压力及施工成本等方面都有大幅降低.
四川省自贡市沿滩区位于国家长江上中游柑桔产业带,是四川省柑桔重点县之一.沿滩区柑桔种植历史悠久,目前柑桔是当地优势农业产业,但在品种选择、建园水平、管理技术、品牌打造、商品化处理等方面,仍有潜力可挖.
传统卷烟市场日趋萎缩,加热不燃烧的新型烟草制品代表未来烟草制造技术的发展方向.加热卷烟的雾化烟丝由多种配方薄片烟丝构成,对香气携带能力差,需提高加香比例;且加热型卷烟制品口味更丰富,传统加香机进行加香时无法保证各个口味间不串味,影响烟草产品质量.在传统加香机的基础上进行升级改造,研制一种防外溢加香机,以满足加热型卷烟制品不同口味的生产需求.
通过对深度学习和矩阵分解技术进行结合,设计一个深度神经网络对用户和物品进行特征提取,形成用户隐向量和物品隐向量的方法,计算这两个隐向量的内积得到用户对物品的评分预测.为提高推荐精度,提出使用显式数据和隐式数据并设计新的损失函数能够同时计算这两类数据损失的方法.在两个公开数据集上的实验结果表明,该方法比基线模型在HR和NDCG推荐指标上有较大提升.
针对滑油中磨粒形状复杂且尺寸大小不一,传统滑油磨粒检测方法存在时效性差、检测尺度小、精度低、非铁磁性磨粒不能检测等缺点;设计了一种基于深度学习的航空发动机滑油磨粒检测方法;基于连续流微流控芯片的滑油图像采样方法,构建滑油图像采样系统;设计图像增强方法,进行图像数据增强消融试验研究,针对YOLOv3模型和Faster RCNN模型进行精度测试,结果表明消融试验后的YOLOv3模型检测能力明显优于Faster RCNN模型;为减少消融后YOLOv3模型的误检率,提出SER算法以优化该模型的推理置信度阈值;研究
氡是紧随吸烟之后的第二大致肺癌环境因素。近年来,随着氡与肺癌流行病学调查研究的不断深入及其方法学的进一步完善,相关危险度模型的研究也取得了一些新的进展。本文对迄今为止多个国际学术组织或团队给出的氡致肺癌超额相对危险度模型进行综述,简要介绍所建立模型的背景及其考虑的主要因素;结合我国不同年代的室内氡浓度水平进行了氡致肺癌危险度的试算,并为准确开展我国室内氡致肺癌风险评估研究提出了参考建议。“,”Radon is the second largest environmental factor inducing
在运载火箭的海上测控任务中,目标特性分析是最重要的工作之一;通常采用人工预先识别任务弧段中火箭遥测天线方向图的增益变化,并手动计算地面测控站接收信号AGC情况;针对上述方法效率低、过程繁琐、人为错误无法避免等问题,讨论了基于STK软件进行运载火箭测控链路电平仿真分析的方法,重点分析如何利用火箭实测天线方向图生成STK格式的天线电磁场辐射图;通过某次运载火箭飞行任务的仿真分析和实际跟踪结果比较,证明该仿真分析方法能够满足任务需求,仿真结果可以作为运载火箭目标特性分析的参考.
生物医学文本蕴含着丰富的探索价值,其为生物医学工作者进行研究提供了宝贵的领域知识.充分且高效地利用海量的生物医学文献,并从中发现重要的隐藏信息、获取专业领域知识,对生物医学研究具有重要的意义.生物医学实体链接是对生物医学文本中的命名实体进行识别,并将表示该实体的某些字符串映射到生物医学领域知识库中对应概念.生物医学实体链接任务通常面临两个主要的挑战:(1)自然语言描述的歧义性.(2)自然语言文本与生物医学知识库的异构性.传统的方法基于特征选择或规则发现,依赖于手动选择特征或定义规则,处理分阶段模型中也可能
功率开关器件是逆变器的核心部件,但其易发生开路故障,故对其进行故障诊断方法研究很有必要;针对中点钳位型(NPC)三电平逆变器功率开关管器件的开路故障,提出一种基于总体经验模态分解(EEMD)模糊熵和粒子群算法(PSO)优化的核函数极限学习机(KELM)的故障诊断方法;首先采样功率开关器件的桥臂输出端的三相电压作为故障信号以区分各种故障类型,然后利用EEMD模糊熵提取故障特征向量,最后将其划分为训练集和测试集送入PSO-KELM中,识别故障类型并输出诊断结果;经Matlab平台仿真实验得到该方法的故障诊断率
现场可编程门阵列(FPGA)内部资源众多,其中互连资源出现故障的概率远远高于片内其他资源,而在以往许多互连测试研究中,所生成的测试配置存在无法覆盖反馈桥接故障的难题,所以较难有测试配置实现故障列表的100%覆盖;因此通过约束桥接故障只发生在单个查找表(LUT)内的信号线上,并结合单项函数,对反馈桥接故障模型进行优化改进,从根本上解决难题;然后对优化后的反馈桥接故障设置相应的约束条件,再使用布尔可满足性理论(SAT)生成满足约束条件的测试配置;采用优化后的故障模型对ISCAS\'89基准电路进行了测试配