Title:
A formal verification device and a program
Document Type and Number:
Japanese Patent JP6199813
Kind Code:
B2
Abstract:
PROBLEM TO BE SOLVED: To suppress occurence of a pseudo error at the time of formal verification.SOLUTION: A formal verification device (100) comprises an input restriction storage unit (112), an assertion storage unit (114), a logic circuit storage unit (116) and a formal verification unit (122). The input restriction storage unit (112) stores input restriction. The assertion storage unit (114) stores assertion. The logic circuit storage unit (116) stores a logic circuit. The formal verification unit (122) executes formal verification on the basis of the input restriction, the assertion and the logic circuit. The input restriction storage unit (112) stores, as the input restriction, an input condition of dynamic verification or an output result of dynamic verification.
Inventors:
Fujita Nobuto
Application Number:
JP2014127986A
Publication Date:
September 20, 2017
Filing Date:
June 23, 2014
Export Citation:
Assignee:
Kyocera Document Solutions Co., Ltd.
International Classes:
G06F17/50
Domestic Patent References:
| JP2000305977A | ||||
| JP2006053813A | ||||
| JP11328251A |
Foreign References:
| US20120198399 | ||||
| US8316332 |
Other References:
垣内洋介 外3名,モニタベース形式検証のための入力制約を考慮したモニタ回路生成手法,電子情報通信学会論文誌D,社団法人電子情報通信学会,2006年 4月 1日,Vol. J89-D, No. 4,pp. 674 - 682
松本剛史 外4名,反例を利用した網羅性の高いプロパティ集合生成手法,情報処理学会研究報告,社団法人情報処理学会,2008年11月10日,Vol. 2008, No. 111,pp. 115 - 120
松本剛史 外4名,反例を利用した網羅性の高いプロパティ集合生成手法,情報処理学会研究報告,社団法人情報処理学会,2008年11月10日,Vol. 2008, No. 111,pp. 115 - 120
Attorney, Agent or Firm:
Hiroyuki Maei