synlig icon indicating copy to clipboard operation
synlig copied to clipboard

Formal equiv diff const function

Open alaindargelas opened this issue 2 years ago • 0 comments

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.

alaindargelas avatar Aug 30 '22 04:08 alaindargelas