Hardware/ASIC/SoC/NoC2009.11.06 15:35
Formal verification 기술들은 Timing 그리고 물리적인 영향과 같은 기술적 고려사항 없이 수학적인 방법을 사용하여 설계의 유효성을 검증한다. 그리고 참조하는 설계와 대조하여 비교함으로써 설계의 논리적인 기능을 검사한다.
많은 EDA tool vendor들은 formal verification tool들을 개발해 왔으며, Synopsys는 "Formality"라 부르는 formal verification tool을 시장에 소개했다.
Formal method와 dynamic simulation의 주요한 차이는 다음과 같다. Formal method는 두 설계의 구조와 기능이 논리적으로 동등한지를 검증함으로써 설계를 검증하지만, Dynamic simulation method는 오직 설계의 확실한 경로들에 대해서만 감지하고 다른 곳에서 발생하는 문제를 찾지 못한다. 게다가 formal method는 dynamic simulation method와 비교하여 무시해도 좋을 만큼의 시간을 소비한다.
설계 순서에서 Formal verification의 목적은 RTL과 RTL, RTL code와 gate-level netlist 또는 gate-level과 gate-level netlists사이를 비교하여 확인하기 위한 것이다.
RTL과 RTL 검증은 오래된 기능적으로 오류가 없는 RTL과 비교하여 새로운 RTL을 확인하기 위해서 사용된다. 이것은 일반적으로 추가적인 기능들을 수용하기 위해서 자주 바뀌는 주제의 설계를 위해 수행된다. 새로운 기능들을 RTL source에 추가할 때, 이전에 오류없이 설계된 RTL의 기능적으로 올바른 특성을 파괴하는 위험이 있다. 이것을 예방하기 위해서 Formal verification은 원래의 기능의 유효성을 검사하기 위해서 원래의 RTL과 새로운 RTL 사이에서 수행된다.
RTL과 gate-level 검증은 Logic이 DC(Design Compiler)에 의해서 정확하게 합성되었는지를 확인하기 위해서 사용된다. RTL을 기능적으로 정확하다는 것을 동적으로 시물레이션하기 때문에, RTL과  scan이 추가된 gate-level netlist 사이의 formal verification은 gate-level이 같은 기능이라는 것을 보장한다. 이 예에서 만약 우리가 gate-level을 검증하기 위해서 dynamic simulation 방법을 사용한다면, 이것은 설계 검증을 위해서 설계의 크기에 따라서 몇일 또는 몇주의 오랜 시간을 소비한다. 이와 비교하여 formal verification 방법은 비슷한 검증을 수행하기 위해서 몇시간을 소비할 것이다.
마지막 부분은 gate-level netlist와 gate-level netlist를 비교하여 검증하는 것을 수반한다. 이것은 또한 검증 절차를 위해서 중요한 단계이다.

Reference
[1]Advanced ASIC Chip Synthesis using synopsys Design Compiler, Physical Compiler and PrimeTime 2E
Posted by Act of God