asynchronous reset mechanism of D flip-flop in yosys

[Bassman59]

Hey Guys,

Unless you or I could show that yosys-smtbmc does not follow IEEE verilog standard on what is supposed to happen when both the clock edge rises and the asynchronous reset is deasserted at the same time ,
yosys developers will just ignore my questions.

Maybe you can show them your example and ask them to explain why its result differs from what the industry-standard tool gives you?

They only follow standard specifications instead of follow blindly what results the other tools are giving.

Do you get it ?

Please correct me if wrong.

Why do you assume that ModelSim is not following standard specifications? Especially given that ModelSim has been around, well, forever.

Why do you assume that what yosys-smtbmt is doing is correct?

Note: yosys-smtbmc is formal verification tool

You should have said that you were using yosys-smtbmc in your very first post, as the rest of us were wondering why you were doing verification with a synthesis tool.

I just spent a few minutes looking at yosys-smtbmc. I found a paper. I even found one of your posts on Reddit. I don't understand what his verification mechanisms (assert, assume, etc) are doing under the hood.

Anyway, looking at Wolf's paper and your FORMAL code, I suspect that there's a race condition. I admit that I don't know anything about SystemVerilog Assertions, so I can't say whether you are using them correctly.

[NorthGuy]

Unless you or I could show that yosys-smtbmc does not follow IEEE verilog standard on what is supposed to happen when both the clock edge rises and the asynchronous reset is deasserted at the same time ,
yosys developers will just ignore my questions.

This has nothing to do with Verilog. The schematics they produced is correct. So, you can rule out everything which is related to Verilog. It's the later steps where the problem occur.

There's no race condition here. The reset_sync is generated by the clock edge. In simulation, it is assumed to reach the destination by the next clock edge. In real life, where there's a clock skew, the clock at the receiving flop may be too late, so that it arrives after the reset_syn has gone low. But the behavioural simulation is not concerned with timing - it is run as if there's no clock skew and all the setup and hold requirements are met. This applies to about any signal in your design. reset_sync is not special.

[Bassman59]

Unless you or I could show that yosys-smtbmc does not follow IEEE verilog standard on what is supposed to happen when both the clock edge rises and the asynchronous reset is deasserted at the same time ,
yosys developers will just ignore my questions.

This has nothing to do with Verilog. The schematics they produced is correct. So, you can rule out everything which is related to Verilog. It's the later steps where the problem occur.

There's no race condition here. The reset_sync is generated by the clock edge. In simulation, it is assumed to reach the destination by the next clock edge. In real life, where there's a clock skew, the clock at the receiving flop may be too late, so that it arrives after the reset_syn has gone low. But the behavioural simulation is not concerned with timing - it is run as if there's no clock skew and all the setup and hold requirements are met. This applies to about any signal in your design. reset_sync is not special.

My comment about race conditions concerns what the yosys FORMAL stuff does, not what Verilog itself will do (as shown by my test bench).