Issues with formal verification using yosys

[AnishMall]

I am trying to synthesize a FIR filter using yosys with the NanGate 15nm library file. After synthesis I want to run formal verification to check for equivalence since I have a doubt regarding the correctness of the synthesis itself. I have tried using both EQY and SBY but am getting different errors in both. In EQY, the process gets stuck in the combine phase into what I assume is an infinite loop. Using SBY gives me an error "base: ERROR: Module \BUF_X1' referenced in module \FIR_filter_firBlock_left_MultiplyBlock' in cell `_1356_' is not part of the design." I am attaching my EQY and SBY scripts that I have been using. I could not find any documentation regarding how to perform the verification if one has used a custom library file for synthesis so I am not sure if these scripts are correct. Would be grateful to receive any kind of help with this.

[KrystalDelusion]

Your SBY script appears to have the functional_verilog_NanGate5nm.v file in the gold with FIR_filter.v while the EQY script has it in the gate with synth_firfilter2.v.

[AnishMall]

which of the two is correct? I have been trying different things since I could not find any documentation for this kind of formal verification. I also think my errors might be due to other reasons, since neither worked really

[KrystalDelusion]

I don't know that either of them are correct. I was initially going to respond that I don't think SBY supports verifying post-synthesis results against a pre-synthesis reference when I noticed that they were different.

Is FIR_filter.v the original source while synth_firfilter.v is the synthesis output? How are you generating synth_firfilter.v?

[AnishMall]

yes, I am generating synth_firfilter.v using yosys with the following synthesis script

I also made changes to my sby script. This is working for simple designs like an adder module but not for the FIR filter design.

[KrystalDelusion]

Asynchronous logic (like an $adff) is problematic for the sat solvers Yosys/SBY use. You would typically call async2sync after prep to convert the asynchronous cells to synchronous ones with extra logic to emulate the asynchronous behaviour. FWIW, if you're running sat I don't think you need SBY at all; you can just run that in Yosys directly, and if you've already proved equivalence with sat I don't think SBY is adding anything.