포멀(Formal) 방식으로 확인한 C++ 설계와 RTL 설계의 동등성

타이밍이 없는 C++로 기술된 설계를 상위 수준 합성(HLS) 플로우를 통해 적용할 때, 설계자는 생성된, 타이밍이 있는 RTL이 원본 상위 수준으로 기술된 설계와 기능적으로 동등한지 의문을 가지게 됩니다. 미세 조정을 하거나 RTL을 전력에 맞춰 최적화할 때면 이러한 변경 사항이 더 이상 원래 사양에 부합하지 않는 것이 아닌가 우려되는 것이 당연합니다. 물론 테스트벤치를 만들어 플로우의 모든 단계마다 검증을 할 수도 있지만, 시간이 너무 오래 걸리기 때문에 생산 일정을 완전히 망쳐버릴 수 있습니다. 설계자에게 진정으로 필요한 것은 테스트벤치와 시뮬레이션 없이도 설계 동등성을 신속하게 판단할 좋은 방법입니다. 그리고 여기에 가장 적합한 해결책이 바로 포멀(Formal), 순차적 로직 동등성 검사법인 SLEC HLS입니다. 이 백서를 통해 왜 SLEC HLS가 Catapult 검증 플로우의 필수적인 부분인지에 대하여 알아보고 그 동작 원리는 무엇이며, 왜 이 제품이 시장에서 유일한 툴인지 확인해 보시기 바랍니다.