说明
当您将full_case的合成属性应用到案例语句标题中时，它将工具解释为"不在乎"值。 Quartus® II 软件推断其他逻辑以代表"不在乎"状态。此附加逻辑可能与通过正式验证工具推断的逻辑不同，从而导致正式验证不匹配。
要克服不匹配的问题，在状态机器中定义 所有状态。
有关状态机编码指南的详细信息，请参阅 Quartus II 手册卷 1 中的 HDL 编码风格 （PDF）一章。