search

ghdl / ghdl-yosys-plugin

VHDL synthesis (based on ghdl)
GNU General Public License v3.0
295 stars 32 forks source link

GHDL+YOSYS formal verification, using Xilinx primitives #194

Open Marceloqa opened 6 months ago

Marceloqa commented 6 months ago

I've been using the workflow described in this link https://vhdlwhiz.com/formal-verification-in-vhdl-using-psl/#yosys-et-al It has afforded me great success, and i've taken my first steps with formal verification with PSL and GHDL.

However, I wish to now do some formal verification with modules that instantiate Xilinx primitives (.e.g IBUFDS from 'unisim') library. Is this even possible? Since these libraries provided by Xilinx (in location /opt/Xilinx/Vivado/2022.2/data/vhdl/src/) are most likely non-synthesizeable, i worry that there is no way to achieve what i want, since 'ghdl-yosys-plugin' involves synthesis prior to formal verification using other tools.

Does anyone have any experience/insight into this? What alternatives exist for formal verification with Xilinx primitives?

tgingold commented 6 months ago

In general you don't want to do that. Ideally, you design a core, which doesn't use Xilinx primitives and you do formal verification on that core. Finally, you have a testbench for the full design including the primitives. That's certainly possible for primitives liks IBUFxx or OBUFxx. For very complex primitives (GT, PCI) you probably need to abstract them.

aniketabhiraj2004 commented 1 week ago

Is thier is a way to run unisim?