首页> 外国专利> ABSTRACTION DEVICE AND VERIFICATION DEVICE OF CIRCUIT DESCRIPTION, ABSTRACTION PROGRAM AND VERIFICATION PROGRAM OF THE CIRCUIT DESCRIPTION, AND ABSTRACTION METHOD AND VERIFICATION METHOD OF THE CIRCUIT DESCRIPTION

ABSTRACTION DEVICE AND VERIFICATION DEVICE OF CIRCUIT DESCRIPTION, ABSTRACTION PROGRAM AND VERIFICATION PROGRAM OF THE CIRCUIT DESCRIPTION, AND ABSTRACTION METHOD AND VERIFICATION METHOD OF THE CIRCUIT DESCRIPTION

机译:电路描述的抽象装置和验证装置,电路描述的抽象程序和验证程序,以及电路描述的抽象方法和验证方法

摘要

PROBLEM TO BE SOLVED: To provide an abstraction device and a verification device of circuit description, an abstraction program and a verification program of the circuit description, and an abstraction method and a verification method of the circuit description, allowing facilitation of verification of the circuit description converted into a formal specification, wherein description contents of a computer program can be verified by formal technique.;SOLUTION: The abstraction device determines whether each calculation processing unit included in a logic model shown by specification data 24 of the circuit description is a non-verifiable calculation processing unit not allowing the verification by the formal technique within a preset threshold time. When decision results are affirmative decision, a list of verifiable calculation processing units allowing the verification by the formal technique within the threshold time is output to an output device 13 in a selectable state based on input operation from an input device 12. Inside the logic model, the calculation processing unit decided that it is the unverifiable calculation processing unit is replaced with the calculation processing unit selected from the list of the verifiable calculation processing units.;COPYRIGHT: (C)2010,JPO&INPIT
机译:解决的问题:提供电路描述的抽象装置和验证装置,电路描述的抽象程序和验证程序,以及电路描述的抽象方法和验证方法,以便于电路的验证描述转换成正式规范,其中计算机程序的描述内容可以通过正式技术进行验证。解决方案:抽象设备确定电路描述的规范数据24所示的逻辑模型中包括的每个计算处理单元是否为非-可验证的计算处理单元不允许在预设的阈值时间内通过形式技术进行验证。当判定结果为肯定判定时,基于来自输入装置12的输入操作,以可选择的状态将允许在阈值时间内通过形式技术进行验证的可验证计算处理单元的列表输出至输出装置13。 ,计算处理单元确定它是不可验证的计算处理单元,替换为从可验证的计算处理单元列表中选择的计算处理单元。;版权:(C)2010,JPO&INPIT

著录项

  • 公开/公告号JP2010079433A

    专利类型

  • 公开/公告日2010-04-08

    原文格式PDF

  • 申请/专利权人 AISIN AW CO LTD;

    申请/专利号JP20080244629

  • 发明设计人 KUBO TAKAYUKI;

    申请日2008-09-24

  • 分类号G06F17/50;

  • 国家 JP

  • 入库时间 2022-08-21 19:01:21

相似文献

  • 专利
  • 外文文献
  • 中文文献
获取专利

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号