Equivalence Checking

아래 그림이 Synopsis사의 formality 설명 문서에 나온 순서도인데,

1) HDL로 작성한 RTL을 synthesize하면 1차 netlist가 나옴.

2) 1)에서 나온 netlist로 PnR을 진행하면 Final netlist가 나옴.

3) Synthesizer가 뱉어낸 netlist와 PnR이 완료된 Final netlist를 비교하여 각 net이 동일하게 생성되었는지,

즉 Verilog로 서술했던 functionality와 netlist로 구현된 design이 정확히 같은 동작을 하는지 확인함.