This is a bit of code on top of #4282 to have the structural choices that abc9 comes up reimported back into Yosys, for inspection and possibly other uses.
Minimal example where one sees it in action:
read_verilog <<EOF
(* top *)
module top(a, b, y);
input wire [1:0] a;
input wire [1:0] b;
output wire [1:0] y;
assign y = a * b;
endmodule
EOF
opt_clean
techmap
splitnets -ports
abc9 -script +&synch2;,&ps;;
show
Let me leave a note that the imported $__choice nodes represent equivalences up to a negation. (One can find out the value of the referenced nodes under all PIs being zero to recover polarities.)
This is a bit of code on top of #4282 to have the structural choices that abc9 comes up reimported back into Yosys, for inspection and possibly other uses.
Minimal example where one sees it in action: