Formal equiv diff common_logic.v

[alaindargelas]

Test: ./yosys/tests/arch/common/logic.v The trimmed down version of that test has 3 errors in the plugin code (Visible in the corresponding gate netlist):

module top
(
    input [0:7] in,
    output B3,B4
);
    assign B3 =  in[0] ~& in[1]; 
    assign B4 =  in[0] ~| in[1]; 
endmodule

• The "in" range is reverted
• There is no "binary bitwise nand" operator in Verilog, so in Surelog I use the "bitwise reduction nand" with 2 operands to model "in[0] ~& in[1]", the plugin should translate to the appropriate Yosys operator or use a "and" and "bitwize negation" operators.
• The bitwize nor operator is correct in Surelog, but another operator is used after the plugin (Can't tell which).

[alaindargelas]

https://class.ece.uw.edu/cadta/verilog/operators.html

[mandrys]

Fixed by https://github.com/chipsalliance/yosys-f4pga-plugins/pull/394.

[mandrys]

Test added to formal verification passlist in PR #1331.