3、硬件描述语言与形式化模型：Verilog/VHDL的语义模型、有限状态机（FSM）的形式化建模、FSM的等价性与化简、从RTL代码提取形式化模型

好，我们进入第三章。这一章，说白了就是打通「RTL代码」和「形式化验证」之间的那堵墙。

你想想看，形式化验证工具再厉害，它也不认识你的Verilog代码。它只认数学——布尔公式、状态机、时序逻辑。所以，我们必须把硬件描述语言翻译成形式化模型。这个翻译过程，就是本章的核心。

3.1 Verilog/VHDL的语义模型

先聊语义模型。什么是语义模型？就是给硬件描述语言一个严格的数学解释。

Verilog和VHDL，本质上都是用来描述「并发执行的硬件行为」的语言。但问题是，它们本身不是数学。比如Verilog里的 always @(posedge clk)，在形式化世界里对应什么？对应一个时钟驱动的状态转移。

我个人习惯把Verilog的语义模型分成三层：

• 调度语义：事件驱动的仿真行为。比如阻塞赋值和非阻塞赋值的区别，在形式化模型里必须精确建模。
• 时序语义：时钟沿、组合逻辑、延迟。形式化验证里我们通常用「同步假设」——所有寄存器在同一个时钟沿更新。
• 结构语义：模块的层次化连接。顶层模块调用了哪些子模块？信号怎么连的？这些在提取模型时都要展开。

举个例子。我曾经遇到一个项目，同事写了一段Verilog，里面用了 #5 的延迟控制。形式化验证工具直接报错——因为它不支持延迟建模。嗯，这里要注意：形式化模型是「功能模型」，不是「时序模型」。延迟、毛刺、竞争冒险，这些通常不在形式化验证的考虑范围内。

3.2 有限状态机（FSM）的形式化建模

FSM是数字电路设计的灵魂。几乎所有的控制逻辑，最终都可以抽象成一个FSM。

形式化建模FSM，我一般用六元组：(S, I, O, δ, λ, s0)。

• S：状态集合。比如IDLE、READ、WRITE、ERROR。
• I：输入集合。比如按键信号、数据有效信号。
• O：输出集合。比如读使能、写使能。
• δ：状态转移函数。当前状态+输入 → 下一状态。
• λ：输出函数。Moore型输出只依赖当前状态，Mealy型依赖状态+输入。
• s0：初始状态。通常是复位后的状态。

在Verilog里，一个典型的FSM长这样：

// 三段式FSM示例
module fsm_example (
    input clk, rst_n,
    input start,
    output reg done
);
    typedef enum logic [1:0] {IDLE, BUSY, DONE} state_t;
    state_t state, next_state;

    // 状态寄存器
    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n) state <= IDLE;
        else state <= next_state;
    end

    // 下一状态逻辑
    always_comb begin
        next_state = state;
        case (state)
            IDLE: if (start) next_state = BUSY;
            BUSY: next_state = DONE;
            DONE: next_state = IDLE;
        endcase
    end

    // 输出逻辑
    always_comb begin
        done = (state == DONE);
    end
endmodule

这段代码，形式化工具提取出来的模型就是：三个状态、三个转移、一个输出。简单明了。

3.3 FSM的等价性与化简

为什么要讨论等价性？因为形式化验证里，我们经常需要比较两个FSM是否行为一致。

比如，你重构了一段控制逻辑，想验证新代码和旧代码功能一样。这时候就需要FSM等价性检查。

FSM等价性有两种：

• 状态等价：两个状态，在任意输入序列下，输出序列完全相同。
• FSM等价：两个FSM，从初始状态开始，对任意输入序列，输出序列完全相同。

化简呢？就是把冗余的状态合并掉。我记得有一次做验证，发现一个FSM有16个状态，但实际只需要8个。剩下的8个状态，要么不可达，要么等价于其他状态。

化简算法其实不复杂：

1. 先找出所有不可达状态（从初始状态永远到不了的状态）。
2. 再对可达状态做等价类划分。
3. 合并等价的状态。

3.4 从RTL代码提取形式化模型

这一步是实战中的关键。工具怎么把Verilog变成形式化模型？

流程大致如下：

1. 解析RTL：读入Verilog/VHDL，生成抽象语法树（AST）。
2. 展开层次：把模块实例化展开，形成扁平化的网表。
3. 识别时序元件：找到所有寄存器、锁存器、存储器。
4. 提取组合逻辑：把组合逻辑翻译成布尔表达式或BDD（二叉决策图）。
5. 构建状态机：根据寄存器和组合逻辑，构建出FSM模型。

这里有个细节：不是所有RTL都能被完整提取。比如：

• 循环语句（for循环）如果循环次数不固定，工具可能展开不了。
• 动态数组、指针、递归调用——这些在硬件里很少见，但一旦出现，形式化工具就头疼。
• X态、Z态——形式化模型通常只处理0和1，三态和未知态需要特殊处理。

下面这张图，展示了从RTL到形式化模型的完整流程：

实际项目中，提取模型这一步往往是自动化的。但作为验证工程师，你必须理解工具在做什么，才能判断提取出来的模型是否正确。

好了，这一章的内容就到这里。从语义模型到FSM建模，再到等价性化简和模型提取，这些是形式化验证的「基础设施」。理解透了，后面学断言和属性检查才会顺手。

---

公众号:蓝海资料掘金营，微信deep3321