synlig
synlig copied to clipboard
Formal equiv diff state machine
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.