异步电路的形式验证

Formality is used to verify synchronous designs。Therefore your design should not contain asynchronous state-holding loops implemented as combinational logi。

这句话是formality user guide中的一句话，想问下为什么异步电路是难于进行等价性验证的，应该采用什么样的手段来确保异步电路部分的RTL和网表的等价。
希望有大侠能给解释下（若能提下异步电路会对等价性产生什么影响更好了）

采用仿真的手段很难发现CDC的问题。RTL仿真时间太短，也就是说出现DCD概率非常小。采用形式验证工具能否发现这方面的问题

异步电路 就用动态仿真来看看啊， sta，fm不行的，