synlig icon indicating copy to clipboard operation
synlig copied to clipboard

Formal equiv diff state machine

Open alaindargelas opened this issue 2 years ago • 1 comments

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 OK. I assume something wrong is happening in the plugin when assembling the allModule and topModule views (Since the UHDM elab is not used).

You might have to diff the Yosys ASTs to find more info on where the plugin introduces the error.

alaindargelas avatar Aug 26 '22 03:08 alaindargelas