why the results I get with Yosys’s eval -set-undef -table L command differ from those produced by ABC’s write_pla

[yujning]

module TOP (
output [8:0] D,
input [0:0] S,
input [0:0] L
);

wire A;   
wire B; 
wire [8:0] y;
wire n15, n16, n17, n18, n19, n20, n21, n22, n23, n24, 
    n25, n26, n27, n28, n29, n30;
 
buf (A, S[0]);  
buf (B, L[0]); 
not (n19, A);  
shift_left_4u_2u shift_left_14 (.cin(1'b0), .a({4'b0001}), .amount({A, 
        B}), .o({n15, n16, n17, n18}));   
not (n20, B);   
and (n21, B, n19) ;  
assign n22 = n21 ? n15 : y[7];   
assign n23 = n21 ? n16 : y[6];   
assign n24 = n21 ? n17 : y[5];   
assign n25 = n21 ? n18 : y[4];   
and (n26, n20, n19) ;   
assign n27 = n26 ? n15 : y[3];   
assign n28 = n26 ? n16 : y[2];   
assign n29 = n26 ? n17 : y[1];  
assign n30 = n26 ? n18 : y[0]; 

buf (y[8], n22);
buf (y[7], n23);
buf (y[6], n24);
buf (y[5], n25);
buf (y[4], n27);
buf (y[3], n28);
buf (y[2], n29);
buf (y[1], n30);
buf (y[0], n26);

assign D[0] = y[0]; 
assign D[1] = y[1]; 
assign D[2] = y[2]; 
assign D[3] = y[3]; 
assign D[4] = y[4]; 
assign D[5] = y[5]; 
assign D[6] = y[6]; 
assign D[7] = y[7];
assign D[8] = y[8]; 

endmodule

//
// Description of OPERATOR shift_left_4u_2u
//

module shift_left_4u_2u (cin, a, amount, o);
input cin;
input [3:0]a;
input [1:0]amount;
output [3:0]o;

wire n1, n2, n3, n4;

assign n1 = amount[0] ? a[2] : a[3];
assign n2 = amount[0] ? a[1] : a[2];
assign n3 = amount[0] ? a[0] : a[1];
assign n4 = amount[0] ? cin : a[0];
assign o[3] = amount[1] ? n3 : n1;
assign o[2] = amount[1] ? n4 : n2;
assign o[1] = amount[1] ? cin : n3;
assign o[0] = amount[1] ? cin : n4;

endmodule

1.read_verilog xx.v
2.synth -flatten
3.prep -top TOP
4.eval -set-undef -table L

\L	\D
1'0	9'000xxx0xx
1'1	9'xxx000000

Assumed undef (x) value for the following signals: \S

1.read_verilog xx.v
2.synth -flatten
3.write_blif xx.blif
ABC:
5.read xx.blif
6.write_pla xx.pla
.i 2
.o 9
.ilb S L
.ob D[0] D[1] D[2] D[3] D[4] D[5] D[6] D[7] D[8]
.p 3
00 100000000
00 010000000
01 000000100
.e

For example, when L = 0 and S = x, D[3] is 0, not x.

[yujning]

yosys> sat -set-all-undef S -set D[3] 0 -show L

13. Executing SAT pass (solving SAT problems in the circuit).

Setting up SAT problem:
Import set-constraint: \D [3] = 1'0
Final constraint equation: \D [3] = 1'0
Import all_undef constraint for this timestep: \S
Imported 12 cells to SAT database.
Import show expression: \L

Solving problem with 235 variables and 626 clauses..
SAT solving finished - model found:

Signal Name Dec Hex Bin

---

\L 1 1 1

The result obtained using the sat command is different from that of the eval command, but it matches the result from write_pla

[yujning]

If I use the form -set-all-undef S -set L 0, according to the PLA format file, I should get 000000xx, but I don't understand why it's 000xxx0xx.

Because when L=0, their truth table shows:

• 00 → 00000011
• 10 → 00000000

[KrystalDelusion]

Consider the following example script:

read_verilog << EOF
module top(input A, B, output X, Y);
  wire C = (A & !A);
  assign X = C;
  assign Y = B & C;
endmodule
EOF

eval -set-undef -table A
eval -set-undef -table B

The first eval returns

2. Executing EVAL pass (evaluate the circuit given an input).

  \A |  \Y  \X
 --- | --- ---
 1'0 | 1'0 1'0
 1'1 | 1'0 1'0

Assumed undef (x) value for the following signals: \B

where we can see that 0 & 'x == 0. But the second eval gives

3. Executing EVAL pass (evaluate the circuit given an input).

  \B |  \Y  \X
 --- | --- ---
 1'0 | 1'0 1'x
 1'1 | 1'x 1'x

Assumed undef (x) value for the following signals: \A

and we now see that 'x & 'x == 'x and 1 & 'x == 'x. Even though (A & !A) is 0 when A is 0 or 1, it is 'x when A is 'x, because 'x is undefined, not "0 or 1". I don't know exactly how the PLA format is defined, but I'm guessing it uses the latter "0 or 1" meaning rather than truly undefined, and hence it does not match what is reported by Yosys.

[yujning]

So the 'x' in Yosys has nothing to do with don't-care conditions?It's just about whether 'x' gets propagated

[KrystalDelusion]

x in Verilog (and Yosys) doesn't mean "don't-care". It's unknown/undefined. Verilog uses 4-state logic, '1', '0', 'X', and 'Z', where 'X' can be any of the other values, not just 0 or 1.

[KrystalDelusion]

Remember that Yosys is primarily intended for hardware, and physical systems don't always have true binary states, instead being a physical manifestation of voltage and impedance.