Special consideration of x-bits by celledges data

[povik]

Feature Description

Yosys has a facility for "cell edges data" (see celledges.h) which describe which output bits of a cell can be influenced with which input bits.

test_cell -edges can verify this data against a SAT solver. Say we have an input bit X and output bit Y of some cell. For each pair of X and Y, we ask the solver: Can you find a value for all the cell inputs other than X, such that the value of Y is different when X=0 and X=1?

Cells can output x-bits even with defined inputs, and so far the cell edges test considers x-bits equal to zero when it queries the SAT solver, and the rules for generating the cell edges data are written with this in mind (e.g. for $shiftx in #3972) But depending on the use case, this may not be exactly what we want.

I can picture two approaches to x-bits desirable in different use cases:

• We consider x-bit distinct from both 1 and 0: This makes sense e.g. if we are tracking information leakage, since we don't konw what the actual value in place of the x-bit will be in the synthesized circuit, so potentially there's an information leak if the bit flips between x-state and 1, or x-state and 0.

• We consider x-bit not distinct from neither 1 or 0: So in the test we will ask the SAT solver to find a way to flip the Y output between 1 and 0. If the flip is between 1 and x, or 0 and x, we don't count that as grounds for an edge. This may be useful where we want the least amount of edges only constrained by synthesis semantics, e.g. in a hypothetical optimisation pass.