synlig
synlig copied to clipboard
Formal equiv diff const function
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 computation only happens for parameters during Surelog elaboration. Note this happens without invoking the UHDM elaboration.
This testcase on the other hand is assigning the value though a const_assign. const_assign RHS are not reduced by Surelog as they appear in the allModules, and not in the topModules.
If you want the plugin code to compute the value and send only the evaluated result to Yosys, you have to add a "try" mechanism to try to reduce to a constant the rhs expression, else send the complete expression. You have access to the ExprEval::reduce function in UHDM to achive that.