Formal Verification of High-Level Design Based on Control/Data SeEparation

摘要

組込みシステムやシステムLSIなどの規模増大に伴い，より抽象度の高い高位設計から設計を始めること が多くなっている．高位設計の正しさは主にシミュレーションによって検証されるが，テストパターン の漏れがあると設計誤りを検出できないため，網羅的な検証を行う形式的検証の重要性が高まっている ．しかし，形式的検証では一般に計算量が設計規模に対して指数的に増加するため，検証可能規模が小 さいという問題がある．