What can cause a signal to have an X value?

[gussmith23]

Hi all! I'm curious about these lines of the btor backend:

yosys/backends/btor/btor.cc

Lines 971 to 973 in 83c9261

	for (auto bit : sig)
	if (bit == State::Sx)
	goto has_undef_bits;

My module has signals with bits equal to State::Sx...but I can't figure out why the bits are X. That I know of, there are a few ways that signals can get an X value:

• Being set to X, explicitly
• An uninitialized register (maybe? I'm actually not sure on this one, but I think it's the case)

Knowing that these things can cause signals to be X, I've (1) removed all of the instances of X literals from my program and (2) made sure all of the registers are initialized. Despite that, I'm still triggering the above lines of code.

So my question is: what are all of the ways in which a signal can get the value X?

This question may be specific to the BTOR backend -- I'm not sure. My goal is to eliminate the "unnamed" inputs that the BTOR backend generates for X and Z signals.