alaindargelas

Test UHDM-integration-tests/tests/IndexedPartSelectInUniqueCase/top.sv ./run_formal_verif.sh test=IndexedPartSelectInUniqueCase_top.sv After performing constant size computation in Surelog https://github.com/chipsalliance/Surelog/pull/3244 The AST generated by the plugin is still incorrect. A struct with 2 x 32 bit constants is...

Test yosys/tests/sat/alu.v ./run_formal_verif.sh test=sat_alu.v Trimmed down test show the problem in the plugin: This test fails as the implicit typespec of the parameter ALU_OP_SHR is a int_typespec with a range....

Test UHDM-integration-tests/tests/fsm_using_always ./run_formal_verif.sh test=fsm_using_always_dut.v UHDM is correct, I inspected every node. Plugin generates a very different AST compared to Yosys, the gate level is not equivalent.

Test sv2v/test/core/net_or_var.v ./run_formal_verif.sh test=core_net_or_var.v All of the signed constants are mishandled by the plugin.

Test ./UHDM-integration-tests/tests/IndexedPartSelectOfArrayElement/top.sv ./run_formal_verif.sh test=IndexedPartSelectOfArrayElement_top.sv SV2V+Yosys is correct, UHDM is correct, The plugin does not treat the range operator correctly.

Test UHDM-integration-tests/tests/ParameterInGenScopeInitializedWithLongConstant/top.sv ./run_formal_verif.sh test=ParameterInGenScopeInitializedWithLongConstant_top.sv The plugin AST is drastically different from the Yosys AST. UHDM contains the correct representation of the gererate stmt and the parameter value.

Test /UHDM-integration-tests/tests/ImportedPackageEnumItemInInterface/top.sv ./run_formal_verif.sh test=ImportedPackageEnumItemInInterface_top.sv The interface is modeled as a module incorrectly

Formal equiv diff PatternDefault_top.sv

1

Test: UHDM-integration-tests/tests/PatternDefault/top.sv ./run_formal_verif.sh test=PatternDefault_top.sv The patter assign is not translated by the plugin correctly. UHDM contains a formal form of the pattern assign that needs to be flattened by the...

Test: UHDM-integration-tests/tests/ParameterPackedArraySurelogSubstitution/top.sv ./run_formal_verif.sh test=ParameterPackedArraySurelogSubstitution_top.sv The plugin is looking for the parameter value in the uhdmAllModules which is incorrect, it should take the value from the uhdmTopModules P[0] == 8 not...

Test: yosys/tests/svinterfaces/svinterface1.sv ./run_formal_verif.sh test=svinterfaces_svinterface1.sv UHDM is correct. Yosys treats this testcase correctly without sv2v. The plugin generates incorrect AST.