alaindargelas

Test UHDM-integration-tests/tests/OneInside/dut.v ./run_formal_verif.sh test=OneInside_dut.v sv2v correctly translate this assign b = a[2] & (a inside {OP_1, OP_2, OP_3}); into: assign b = a[2] & |{a == OP_1, a == OP_2,...

Test: UHDM-integration-tests/tests/PatternAsParameterOfInstance/top.sv ./run_formal_verif.sh test=PatternAsParameterOfInstance_top.sv UHDM tree is correct, plugin send the wrong parameter value to Yosys AST

Test: UHDM-integration-tests/tests/TypedefAliasInPackage/top.sv ./run_formal_verif.sh test=TypedefAliasInPackage_top.sv Produces all zero output, Yosys gate is correct, so is UHDM.

The following test creates incorrect gate-level: ./UHDM-integration-tests/tests/TypedefedRangedFunctionArgument/top.sv Ran with ./run_formal_verif.sh test=TypedefedRangedFunctionArgument_top.sv I just fixed Surelog function evaluation to compute correctly the return value of the function, see https://github.com/chipsalliance/Surelog/pull/3191 But the...

The test ./yosys/tests/simple/case_expr_query.sv Ran with ./run_formal_verif.sh test=simple_case_expr_query.sv Produces a wrong constant 5'b00001 vs 5'b11111. I simplified the testcase to this minimum: ``` module top( output logic [5:0] out ); initial...

The following case: sv2v/test/core/struct_tern.sv ./run_formal_verif.sh test=core_struct_tern.sv Produces a bogus Yosys AST. I checked UHDM, it is correct.

Formal equiv diff state machine

1

The testcase https://github.com/chipsalliance/UHDM-integration-tests/tree/master/tests/fsm_using_function Ran like this: ./run_formal_verif.sh test=fsm_using_function_dut.v Fails with a diff. The gate level netlist is quite different. I inspected the UHDM output very carefully and it seems all...

Testcase: ./yosys/tests/simple/module_scope.v Trimmed down to the following example: ``` module module_scope_Example(o1); parameter [31:0] v1 = 10; output wire [31:0] o1; assign module_scope_Example.o1 = module_scope_Example.v1; endmodule module module_scope_top( output wire [31:0]...

uhdm plugin misses one optimization pass

2

When comparing gate level netlists generated by the Yosys parser and UHDM, it looks like the UHDM plugin is missing an optimization pass for non-observable logic. sv2v/test/relong/split_ports.v ./run_formal_verif.sh test= relong_split_ports.v...

Test ./UHDM-integration-tests/tests/ConstSizes/dut.v The trimmed down test below is failing: ``` module dut (output logic[63:0] b); assign b = 7698294523898761276; endmodule ``` The plugin passes an incorrect value to Yosys, Surelog...