How to use Yosys to convert a Verilog file into logic expressions? Or into POS form?

[yujning]

help

[KrystalDelusion]

I think the closest backend we have would be write_aiger. What is the use case you are asking about? Is it to process further within Yosys, or write an output file?

[yujning]

module TOP (A, B, C, D, E, F);
    input A;
    input B;
    input C;
    input D;
    input E;
    output F;
    
    wire and_tmp0;
    wire and_tmp1;
    wire and_tmp2;
    
    xor (and_tmp0, A, B) ;
    and (and_tmp1, and_tmp0, C) ;
    and (and_tmp2, and_tmp1, D) ;
    or (F, and_tmp2, E) ;
    
endmodule

For this simple Verilog code, I want to obtain the expression (A ^ B) & C & D | E. How can I use Yosys to achieve this? Additionally, when I use the following SAT command:
sat -set-all-undef C -set-all-undef D -set F 0 -show A -show B -show E
I can indeed find a solution.
Is there another command that can set C and D to X (undefined) and directly obtain the values of A and B without being affected by E?
In other words, I want to be able to get A=0, B=0 or A=1, B=1. I sincerely appreciate your response

[KrystalDelusion]

I want to obtain the expression (A ^ B) & C & D | E

I think you would have to write a plugin to get something that looks like that. Natively in Yosys you would be looking at RTLIL, which describes cells that have specified inputs and outputs. You could do something like the following:

read_verilog << EOF
module TOP (A, B, C, D, E, F);
    input A;
    input B;
    input C;
    input D;
    input E;
    output F;
    
    wire and_tmp0;
    wire and_tmp1;
    wire and_tmp2;
    
    xor (and_tmp0, A, B) ;
    and (and_tmp1, and_tmp0, C) ;
    and (and_tmp2, and_tmp1, D) ;
    or (F, and_tmp2, E) ;
    
endmodule
EOF

prep -top TOP
eval -set-undef -set E 0 -table A,B

which gives

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

  \A  \B |  \F
 --- --- | ---
 1'0 1'0 | 1'0
 1'0 1'1 | 1'x
 1'1 1'0 | 1'x
 1'1 1'1 | 1'0

but there isn't a way in eval to say you only want rows for a specific output value.

write_btor and write_smt2 are the other backends used in SBY for SAT solving. But in general Yosys is intended more for circuits than a human readable logic expression.

[yujning]

Thank you for your answer, it's very helpful to me.I saw that Yosys can generate SOP form, but I didn't see POS form. Does Yosys have a command to generate POS form?

[KrystalDelusion]

Are you referring to the $sop cell? There is no equivalent for POS form, no (the $pos cell is unrelated)