2012.4 Vivado synthesis generates incorrect logic when attempting to convert a HDL code containing priority-mux into parallel mux as part of optimization.
Post-synthesis simulation and Onespin formal equivalency check results showed an incorrect value on a sum register. The same design worked fine in XST and Synplify.
An issue was found in the Vivado synthesis code that performed the optimization of the following type of priority-mux structure:
if(a == b)
out <= bdata;
else if(a == c)
out <= cdata;
out <= ddata;
The intent of the optimization was to convert the priority-mux into a parallel-mux to minimize logic levels.
Unfortunately, this issue in version 2012.4 resulted in an incorrect logic.
To work around this issue in 2012.4, the following Tcl command needs to be used to turn off the mux optimization (before running synthesis):
set_param synth.elaboration.rodinMoreOptions "rt::set_parameter inferMuxOpt 0"
This issue is resolved in the 2013.1 version of Vivado.