What is Z-to-X conversion? Issue while trying to run assertions with Z values

Hi!

I’m a newbie to the world of FPV and I’m starting to test my first design, which consists of an SPI receiver. But I’m having a problem with one of the outputs in my design.

By protocol the SPI should have an output bus (SDO) to send serial data to the Controller, however, in my design this output is split into two outputs: sdo_t and sdo_o, since the intention is to connect a tri-state buffer to the output, the behavior should be something like this:

tb_sdo = sdo_t ? 1'bz : sdo_o;

Where tb_sdo would be the output of the buffer, I defined this TB signal to work with it while doing my verification process, but I encountered multiple CEX that doesn’t make sense to me, to illustrate this, I created the following cover:

cover property( ... (1'b1 |-> ##1 tb_sdo === 1'bz && $past(tb_sdo) === 1'b1));

This cover is basically to detect a transition from 1 to Hi-Z, which is a 100% possible scenario but when my cover converges the waveform shows that tb_sdo remains in Hi-Z all the time, there’s no transition at all, but it detects it as if there had been one:

I created other covers and noticed that the ones to detect a transition Z-to-0 or Z-to-1 are unreachable even though they are possible scenarios too! I have seen them in other waveforms.

The root problem seems to the following, but it doesn’t specify the signal causing the problem:

ZTOX - unconstrained inputs from Z-to-X conversions
[ 1] fv_spi_receiver_i.past_value_117

But I tried to find any information about what Z-to-X conversion means and I couldn’t find anything.

I hope this is not a tool-specific issue, but a lack of tri-state values knowledge from my side, thank you so much for your help in advance!!