状态机可靠性：非法状态、输出毛刺与可证明属性

状态机不仅要覆盖正常路径，还要定义非法编码、同时事件、超时和复位中的行为。画图好看不等于实现完整，转移优先级和输出时序必须在RTL与规格中一致。

Moore与Mealy

Moore输出只依赖状态，通常边沿间稳定但可能多一拍；Mealy输出还依赖输入，响应快却可能受组合毛刺影响。跨模块或外部控制输出常寄存更安全。

完整赋值

组合always块先给默认值，再覆盖条件，避免遗漏分支推断锁存。使用unique case等提示时，仿真与综合对非法状态的处理可能不同，仍需显式恢复策略。

状态编码

二进制省触发器，one-hot在FPGA常有较短译码，Gray减少相邻转换位数。编码选择结合速度、面积、功耗与故障检测，不只凭风格。

非法状态恢复

回到复位态未必永远安全，可能重复执行启动动作。根据系统后果进入错误锁定、等待上层确认或安全停机，并保留错误原因。

断言

写“请求后N拍内响应”“互斥输出不同时为1”“无授权不写存储”等属性。形式工具可探索所有输入序列，但证明范围受抽象和环境假设限制。

练习：为通信控制器写状态图、优先级表和五条断言，包含超时与非法状态。