The order of inputs in generated Verilog is unpredictable

[atomb]

When generating Verilog from What4, the order of inputs in the generated Verilog file is determined by which inputs are discovered first during traversal of the term. This doesn't affect satisfiability, but it does affect the mapping of counter-example or model values back to logical variables.

This affects the SAW w4_abc_verilog command, as can be demonstrated here:

sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[8]) -> x == 5 /\ y == 2}}
[19:39:41.827] Sat: [x = 5, y = 2]
sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[8]) -> y == 5 /\ x == 2}}
[19:39:44.436] Sat: [x = 5, y = 2]
sawscript> sat w4_abc_verilog {{ \(x:[8]) -> \(y:[32]) -> y == 0x81050fff /\ x == 2}}
[19:39:51.359] Sat: [x = 255, y = 42009871]
sawscript>