Formal equiv diff assign op type

alaindargelas commented 2 years ago

Test UHDM-integration-tests/tests/xor_assignment/top.sv ./run_formal_verif.sh test=xor_assignment_top.sv

module top(output logic a);
   initial begin
      a  = 1; 
      a ^= 0;
   end
endmodule

The plugin ignores the assign op type and treats the 2nd assignment as a regular assignment where it is an assign with op type vpiBitXorOp

   |vpiStmt:
      \_assignment: , id:7, line:4:7, endln:4:13
        |vpiParent:
        \_begin: (work@top), id:1, line:2:12, endln:5:7
        |vpiOpType:30                <<<<<<<<<  #define vpiBitXorOp               30   /* binary bitwise XOR */
        |vpiBlocking:1
        |vpiRhs:
        \_constant: , id:6, line:4:12, endln:4:13
          |vpiParent:
          \_assignment: , id:7, line:4:7, endln:4:13
          |vpiDecompile:0
          |vpiSize:64
          |UINT:0
          |vpiConstType:9
        |vpiLhs:
        \_ref_obj: (work@top.a), id:5, line:4:7, endln:4:8
          |vpiParent:
          \_begin: (work@top), id:1, line:2:12, endln:5:7
          |vpiName:a
          |vpiFullName:work@top.a
          |vpiActual:
          \_logic_net: (work@top.a), id:11, line:1:25, endln:1:26

alaindargelas commented 2 years ago

Similarly: Test: yosys/tests/simple/local_loop_var.sv ./run_formal_verif.sh test=simple_local_loop_var.sv

The += op is translated into = op by the plugin: AST_ADD op is missing on the RHS (Plugin AST)

Screenshot from 2022-09-09 20-59-02

mandrys commented 2 years ago

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

chipsalliance / synlig

Formal equiv diff assign op type #1050