시스템 반도체의 현실적인 연역적 검증

Practical Deductive Verification of Logic Chips

높은 검증 능력과 검증 용이성을 가진 시스템 반도체의 연역적 검증 프레임워크인 VeriFlow를 개발한다. 문제: 높은 검증 능력이란 안전성(safety), 진행 보장(liveness), 보안 등 하드웨어에 요구되는 다양한 명세를 전부 검증할 수 있음을 의미하고, 높은 검증 용이성이란 검증에 들어가는 시간과 인력을 포함한 비용이 적다는 뜻이다. 일반적으로 이 두가지는 검증에 투자할 수 있는…