ImpulseC/CoDeveloperを使ってみる (5)

今日も『【実践】C言語による組込みプログラミングスタートブック』を続行中です。
C言語の記述でのクロックの分周と、アップダウンカウンタへの変更まで行いました。
明日5章の残り（ロードつきカウンタ、ロードつき10進アップダウンカウンタ）を確認し、
来週24時間時計の動作を確認すれば一通りこの本は終了です。

ところで、ImpulseCの記述では、シミュレーション用の記述と動作合成用の記述を
分けるのにIMPULESE_C_SYNTHESISというマクロを使用しています。
たとえば、
    #ifndef IMPULSE_C_SYNTHESIS
        // シミュレーション用の記述  --- (1)
    #else
        // 動作合成用（ハードウェア）記述  --- (2)
    #endif
のようになります。

シミュレーションでは(1)の記述を使用して機能確認を行い、動作合成をしてHDLに
するときには(2)を使うのですが、(1)と(2)が等価であることはどうやって確認して
いるのでしょうか？

HDLで設計する場合は、シミュレーションと論理合成とで同じHDLを使用しますし、
Formal Verificationを使用してRTLとゲートレベルの等価性もチェックできます。
動作合成を行うときの等価性チェックをどのように行っているのか、気になります。