异步逻辑的形式验证！！！

abao123

如题：
在一个模块中有如下代码
wire clk_a ;
reg flag_a ;
assign clk_a = flag_a && sclk ;
always@(posedge clk_a)
begin
   ......
   data_a <= data ;
   .....
end
always@(posedge pclk)
begin
   .....
   data_b <= data_a ;
   .....
end
sclk和pclk为异步时钟,flag_a是一个使能信号，它控制clk_a.
门级网表的仿真正确，但是网表和rtl做形式验证且始终不能通过。
请问下在这种情况下需要做如何处理????

abao123

自己顶一下！！

navylin1

are you sure this will work on real silicon? donot you need synchronizer for clock domain crossing?

abao123

回复 3# navylin1


    没有明白什么意思？？能讲的清楚一点吗？
能用中文更好，谢谢！！！

overdriver

类似svf这种东西你加了么？

abao123

回复 5# overdriver

加了，谢谢
问题已解决！！