GHDL+YOSYS formal verification, using Xilinx primitives

[Marceloqa]

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?