This adds logic that prevents tristate drive conflicts. For every tristate buffer which drives the signal target and has an enable enable_b we add a singal target_select_enable_b that is derived from enable_b but can only be active (low) when no other target_select_* signal is active.
This makes the design pass the tribuf -formal assertion without any assumptions, and thus prevents all drive conflicts.
To make sure that each tristate buffer can still be selected, I added two cover statements to the enable signal within the tristate buffer module.
mattvenn
commented
2 years ago
This adds logic that prevents tristate drive conflicts. For every tristate buffer which drives the signal
targetand has an enableenable_bwe add a singaltarget_select_enable_bthat is derived fromenable_bbut can only be active (low) when no othertarget_select_*signal is active.This makes the design pass the
tribuf -formalassertion without any assumptions, and thus prevents all drive conflicts.To make sure that each tristate buffer can still be selected, I added two cover statements to the enable signal within the tristate buffer module.