ac.firing 语义设计
1. 目标
ac.firing 用于表达一个单 tick、全有或全无的硬件事务。它把以下行为放进同一个
原子提交边界:
消费固定数量的输入 Queue token
+
读取当前 committed state
+
执行纯组合计算
+
提出 Table / Reg next-state proposal
+
产生固定数量的输出 Queue token
ac.firing 解决的问题不是代码书写顺序,而是明确以下硬件约束:
输入消费、输出产生和状态更新必须在同一个 tick 全部成功,或者全部不发生。
本文只定义目标 Frozen ACIR 语义。Python 前端以后使用函数、装饰器、上下文或自动推导,
均不改变本文定义。
2. 抽象定义
一个 firing 具有静态确定的:
M 个输入 Queue
N 个输出 Queue
一个组合 guard
零个或多个状态 proposal
其统一提交条件为:
fire = all_input_valid
&& all_output_ready
&& guard
其中:
all_input_valid = 所有输入 Queue 的 committed head 都有效
all_output_ready = 所有输出 Queue 都能在本次 firing 接收一个 token
guard = firing region 计算出的 i1 组合条件
只有 fire = true 时才同时发生:
每个输入 Queue pop 一个 token
每个输出 Queue push 一个 token
提交所有有效的 Table write proposal
提交所有有效的 Reg write proposal
当 fire = false 时:
不消费任何输入
不产生任何输出
不提交任何状态 proposal
不允许发布部分结果,也不允许状态先于 Queue handshake 提交。
3. 目标 Frozen ACIR 形态
以下 assembly 只用于固定语义,具体 ODS assembly format 可以等价调整:
%out0, %out1 = ac.firing
inputs(%in0, %in1)
depths [1, 1]
latencies [1, 1] {
^body(
%arg0 : !ac.var<Input0>,
%arg1 : !ac.var<Input1>
):
// committed state observation
%entry = ac.table.get @entries[%index]
%state = ac.reg.get @state
// pure combinational calculation
%guard = ...
%next_entry = ...
%next_state = ...
%payload0 = ...
%payload1 = ...
// next-state proposals
ac.table.write @entries[%index], %next_entry
ac.reg.write @state, %next_state
ac.firing.yield
guard %guard
outputs(%payload0, %payload1)
} : (!ac.queue<Input0>, !ac.queue<Input1>)
-> (!ac.queue<Output0>, !ac.queue<Output1>)
Firing op 的结果是输出 Queue,不是当前 tick 的普通 SSA payload。Region 参数是从输入
Queue committed head 观察到的 firing-local immutable Var。
4. 输入和输出规则
4.1 静态拓扑
输入和输出 Queue 的数量、顺序与类型必须在 Frozen ACIR 中静态确定。运行时条件不能改变
firing 的 Queue 签名。
4.2 第一版固定 rate
第一版规定:
一次 firing 从每个输入 Queue 消费一个 token
一次 firing向每个输出 Queue 产生一个 token
每个 firing 每 tick 最多提交一次
不支持可变 rate、批量 pop/push 或在一个 tick 中重复 firing。
4.3 全输入消费
fire = true 时,所有声明的输入都被消费。不能只消费其中一部分。如果两个输入不应当
共同等待,应拆成不同 firing,并使用显式 Queue topology 协调。
4.4 全输出产生
fire = true 时,所有声明的输出都产生一个 token。不能只产生部分输出。可选结果应当:
拆成不同 firing
或使用 route
或在 payload 中显式携带 valid/tag
4.5 允许零输入或零输出
输入型状态更新可以没有输出:
ac.firing inputs(%completion) {
^body(%request : !ac.var<Completion>):
...
ac.table.write @rob[%index], %next
ac.firing.yield guard %true
}
状态驱动的输出规则可以没有输入:
%retired = ac.firing inputs() {
^body:
...
ac.firing.yield guard %can_retire outputs(%result)
} : () -> !ac.queue<CommitResult>
零输入 firing 每 tick 尝试一次,但仍受 guard 和所有输出 readiness 控制。
同时没有 Queue 输入、Queue 输出和状态 effect 的 firing 没有可观察硬件意义,应由 verifier
拒绝。
5. Region 内的合法逻辑
Region 是单 tick 的组合计算和状态 proposal 区域。
允许:
ac.table.get
ac.table.write
ac.reg.get
ac.reg.write
ac.var.*
arith.*
struct 构造、字段提取和字段替换
组合 mux/select
可静态有界并能组合实现的控制流
ac.firing.yield
禁止:
嵌套 ac.firing
显式 ac.queue.peek/pop/push
多周期等待
阻塞式 Module call
异步 request-response
隐藏 pipeline latency
数据相关的无界循环
Python 或 host side effect
独立于 firing 提交的状态修改
需要延迟、ready-valid、独立调度或异步响应的行为,应通过输出 Queue 连接到另一个
Module/firing,而不是放进 firing region 内等待。
6. Snapshot、Proposal 与 Commit
6.1 Committed snapshot
所有 ac.table.get 和 ac.reg.get 都读取 tick 开始时的 committed state。
同一个 firing 或其他 firing 在本 tick 提出的 write,不能被普通 get 观察到:
tick T committed snapshot
↓
所有 firing 读取并计算
↓
生成 next-state proposal
↓
clock edge / commit
↓
tick T+1 committed snapshot
6.2 Proposal
ac.table.write 和 ac.reg.write 在 region 中只提出候选 next state,不立即修改状态。
若后续组合逻辑需要使用新值,应直接复用其 SSA 值:
%old = ac.reg.get @counter
%next = arith.addi %old, %one
ac.reg.write @counter, %next
// 使用 %next;再次 get @counter 仍然只能得到 %old。
6.3 Commit
只有统一的 fire 为真,proposal 才在 tick 边界提交。输出反压、输入缺失或 guard 为假,
都会取消本次所有 proposal。
Table/Reg 本身没有 ready-valid,也不会单独拒绝 proposal。如果一个状态目标可能 busy、
需要仲裁或多周期响应,它应建模为 Queue-connected Module。
7. Guard 与局部 Enable
7.1 Firing guard
ac.firing.yield 必须提供一个 i1 guard。Guard 可以依赖:
输入 payload Var
当前 committed Table / Reg state
纯组合计算
Guard 不允许依赖:
本次 proposal 提交后的状态
本次 firing 的输出结果是否已经发布
下游输出 Queue readiness
其他 firing 在同 tick 的 proposal
输出 readiness 由 firing 实现统一加入 fire,不能混入功能 guard,以避免形成隐式
ready 组合环路。
7.2 局部 write enable
单个状态 proposal 可以具有局部 enable:
ac.table.write @entries[%index], %next enable %local_enable
其实际 RTL 写使能为:
write_enable = fire && local_enable
局部 enable 为假只禁用该 proposal,不取消 firing。需要阻止输入消费和全部输出产生时,
必须使用 firing guard。
8. 所有权与写冲突
ac.firing 不改变状态的 owner 规则:
一个 Table / Reg 只有一个组件 owner
只有 owner 内的 firing 可以修改该状态
组件之间通过 Queue 交互
同一个 firing 内,对同一个可能运行时地址的多个有效写必须满足以下条件之一:
编译器可以证明写地址不同
编译器可以证明 write enable 互斥
前端已经显式计算 priority,并只产生一个有效 write
否则 verifier 必须拒绝。ACIR 不定义后写覆盖前写,也不根据 op 顺序推导优先级。
同一个 owner 内的多个 firing 如果可能在同 tick 写入同一个 Reg/Table Entry,也必须证明
互斥、显式仲裁或合并为一个 firing。所有 firing 仍统一读取旧 snapshot。
9. 控制流和 Yield 约束
ac.firing region 必须是 single-entry,并最终到达 ac.firing.yield。所有可达 yield 必须:
返回相同数量的 output payload
返回与 firing 结果 Queue 对应的固定类型
返回一个 i1 guard
控制流可以选择 payload、guard 和局部 write enable,但不能改变 Queue 拓扑或提交边界。
实现必须拒绝会形成组合环路的 firing/Queue 网络。特别是功能 guard 不应直接读取输出
readiness;需要打断 ready 路径时,应插入有存储能力的 Queue/FIFO/elastic register。
10. 与现有 Queue Primitive 的关系
以下 primitive 可以视为 ac.firing 的受限特例,但可以继续保留独立 op,以便 verifier、
优化和 RTL provider 识别更窄的硬件结构:
ac.broadcast
= 1 个输入
+ N 个相同 payload 输出
+ guard = true
+ 无 Table / Reg effect
ac.transform
= M 个输入
+ N 个输出
+ 纯组合 region
+ guard = true
+ 无 Table / Reg effect
ac.firing
= M 个输入
+ N 个输出
+ 一般组合 guard
+ Table / Reg proposal
纯 Queue firing 如果满足 broadcast 或 transform 的约束,可以 canonicalize 为对应的
专用 primitive。
11. 示例
11.1 单输入状态更新
ROB completion 每次消费一个完成事件并 patch 对应 Entry:
ac.firing inputs(%completions) {
^body(%completion : !ac.var<Completion>):
%index = ac.var.get %completion["rob_index"]
%old = ac.table.get @rob[%index]
%next = ac.var.with %old["done"], %true
ac.table.write @rob[%index], %next
ac.firing.yield guard %true
} : (!ac.queue<Completion>) -> ()
RTL 概念等价:
fire = completions.valid
completions.ready = true
rob_we = fire
rob_waddr = completion.rob_index
rob_wdata = patched_entry
11.2 零输入状态驱动输出
ROB retirement 没有输入 Queue,由 committed head Entry 驱动:
%retired = ac.firing inputs() {
^body:
%head = ac.reg.get @head
%entry = ac.table.get @rob[%head]
%valid = ac.var.get %entry["valid"]
%done = ac.var.get %entry["done"]
%can_retire = arith.andi %valid, %done
%cleared = ac.var.with %entry["valid"], %false
ac.table.write @rob[%head], %cleared
%next_head = arith.addi %head, %one
ac.reg.write @head, %next_head
%result = ...
ac.firing.yield guard %can_retire outputs(%result)
} : () -> !ac.queue<CommitResult>
提交条件为:
fire = can_retire && retired.ready
当 retired.ready = false 时,ROB Entry 和 head 都保持不变。
11.3 多输入、多输出和状态更新
Rename 同时消费 decoded instruction 和 free physical register,产生 issue 与 ROB 两个输出,
并更新 rename map:
%renamed, %record = ac.firing
inputs(%decoded, %free_phys) {
^body(
%inst : !ac.var<DecodedInstruction>,
%new_phys : !ac.var<PhysicalRegister>
):
%src0 = ...
%src1 = ...
%dst = ...
%old_mapping = ac.table.get @rename_map[%dst]
%next_mapping = ...
ac.table.write @rename_map[%dst], %next_mapping
%renamed_inst = ...
%rename_record = ...
%has_destination = ...
ac.firing.yield
guard %has_destination
outputs(%renamed_inst, %rename_record)
} : (!ac.queue<DecodedInstruction>, !ac.queue<PhysicalRegister>)
-> (!ac.queue<RenamedInstruction>, !ac.queue<RenameRecord>)
统一提交条件为:
fire = decoded.valid
&& free_phys.valid
&& renamed.ready
&& record.ready
&& has_destination
任何一个条件为假,两个输入、两个输出和 rename map 都不改变。
12. GFSim 对应模型
GFSim 中一个 firing 应作为一个整体 transaction object 执行:
1. 从 tick snapshot 检查所有 input valid
2. 检查所有 output capacity / ready
3. 使用 input head Var 和 committed state 计算 region
4. 取得 guard、output payload 和 state proposal
5. 若统一 fire 为真:
- proposal 所有 input pop
- proposal 所有 output push
- proposal 所有 Table / Reg write
6. 在统一 commit 阶段应用 proposal
不能让多个独立 GFSim Work 分别提交 Queue 与状态 effect,否则可能产生部分提交。
现有 QueueAtomicTransform 可以复用多输入、多输出 Queue transaction 的骨架,但需要增加
guard 和 Table/Reg proposal 的统一 commit。
13. RTL 对应结构
一个 firing 的主要 RTL footprint 为:
input valid reduction
+
output ready reduction
+
guard combinational logic
↓
fire
├── input pop enable
├── output push enable
├── Table write enable
└── Reg write enable
概念逻辑:
assign fire = all_input_valid && all_output_ready && guard;
assign input_pop = fire;
assign output_push = fire;
assign table_we = fire && table_local_enable;
assign reg_we = fire && reg_local_enable;
这里的 input_pop 和 output_push 是 Queue storage 的原子提交使能,不等同于直接暴露
在组件边界上的 ready-valid 信号。具体 ready-valid 实现可以消除代数上冗余的信号,
但不得让任一输入或输出提前完成,从而改变全有或全无语义。
大型 firing 会形成宽 valid/ready reduction、长 guard 路径和大量 write enable,因此
ac.firing 应用于局部的单 tick 原子规则,不应把整个组件或整条流水线包进一个 firing。
14. 当前实现与目标语义的差异
截至本文编写时,仓库现有 ac.firing 是较窄的显式 Queue-effect region:
只有 Queue operands
没有输出 Queue results
没有输入 payload block arguments
没有显式 guard
region 内使用 queue.peek/pop/push
本文定义的是 Table/Reg 设计需要的目标 Frozen ACIR 语义。实现时至少需要补齐:
输入 Queue 对应的 region payload 参数
输出 Queue results 与 yield payload
显式 firing guard
Table / Reg proposal effect
Queue 与状态的统一 atomic commit
跨 firing 状态写冲突验证
GFSim transaction lowering
在这些能力完成前,本文示例不能视为当前工具链已经可编译的 ACIR。
15. 定义总结
ac.firing 可以最终概括为:
一个固定 Queue 签名、单 tick、组合求值、原子提交的 ACIR transaction region。它读取
committed snapshot,计算 guard、输出 payload 和状态 proposal,并在所有输入有效、所有
输出可接收且 guard 为真时,同时消费输入、产生输出和提交状态。
ac.firing语义设计1. 目标
ac.firing用于表达一个单 tick、全有或全无的硬件事务。它把以下行为放进同一个原子提交边界:
ac.firing解决的问题不是代码书写顺序,而是明确以下硬件约束:本文只定义目标 Frozen ACIR 语义。Python 前端以后使用函数、装饰器、上下文或自动推导,
均不改变本文定义。
2. 抽象定义
一个 firing 具有静态确定的:
其统一提交条件为:
其中:
只有
fire = true时才同时发生:当
fire = false时:不允许发布部分结果,也不允许状态先于 Queue handshake 提交。
3. 目标 Frozen ACIR 形态
以下 assembly 只用于固定语义,具体 ODS assembly format 可以等价调整:
Firing op 的结果是输出 Queue,不是当前 tick 的普通 SSA payload。Region 参数是从输入
Queue committed head 观察到的 firing-local immutable
Var。4. 输入和输出规则
4.1 静态拓扑
输入和输出 Queue 的数量、顺序与类型必须在 Frozen ACIR 中静态确定。运行时条件不能改变
firing 的 Queue 签名。
4.2 第一版固定 rate
第一版规定:
不支持可变 rate、批量 pop/push 或在一个 tick 中重复 firing。
4.3 全输入消费
fire = true时,所有声明的输入都被消费。不能只消费其中一部分。如果两个输入不应当共同等待,应拆成不同 firing,并使用显式 Queue topology 协调。
4.4 全输出产生
fire = true时,所有声明的输出都产生一个 token。不能只产生部分输出。可选结果应当:4.5 允许零输入或零输出
输入型状态更新可以没有输出:
状态驱动的输出规则可以没有输入:
零输入 firing 每 tick 尝试一次,但仍受 guard 和所有输出 readiness 控制。
同时没有 Queue 输入、Queue 输出和状态 effect 的 firing 没有可观察硬件意义,应由 verifier
拒绝。
5. Region 内的合法逻辑
Region 是单 tick 的组合计算和状态 proposal 区域。
允许:
禁止:
需要延迟、ready-valid、独立调度或异步响应的行为,应通过输出 Queue 连接到另一个
Module/firing,而不是放进 firing region 内等待。
6. Snapshot、Proposal 与 Commit
6.1 Committed snapshot
所有
ac.table.get和ac.reg.get都读取 tick 开始时的 committed state。同一个 firing 或其他 firing 在本 tick 提出的 write,不能被普通
get观察到:6.2 Proposal
ac.table.write和ac.reg.write在 region 中只提出候选 next state,不立即修改状态。若后续组合逻辑需要使用新值,应直接复用其 SSA 值:
6.3 Commit
只有统一的
fire为真,proposal 才在 tick 边界提交。输出反压、输入缺失或 guard 为假,都会取消本次所有 proposal。
Table/Reg 本身没有 ready-valid,也不会单独拒绝 proposal。如果一个状态目标可能 busy、
需要仲裁或多周期响应,它应建模为 Queue-connected Module。
7. Guard 与局部 Enable
7.1 Firing guard
ac.firing.yield必须提供一个i1guard。Guard 可以依赖:Guard 不允许依赖:
输出 readiness 由 firing 实现统一加入
fire,不能混入功能 guard,以避免形成隐式ready 组合环路。
7.2 局部 write enable
单个状态 proposal 可以具有局部 enable:
其实际 RTL 写使能为:
局部 enable 为假只禁用该 proposal,不取消 firing。需要阻止输入消费和全部输出产生时,
必须使用 firing guard。
8. 所有权与写冲突
ac.firing不改变状态的 owner 规则:同一个 firing 内,对同一个可能运行时地址的多个有效写必须满足以下条件之一:
否则 verifier 必须拒绝。ACIR 不定义后写覆盖前写,也不根据 op 顺序推导优先级。
同一个 owner 内的多个 firing 如果可能在同 tick 写入同一个 Reg/Table Entry,也必须证明
互斥、显式仲裁或合并为一个 firing。所有 firing 仍统一读取旧 snapshot。
9. 控制流和 Yield 约束
ac.firingregion 必须是 single-entry,并最终到达ac.firing.yield。所有可达 yield 必须:控制流可以选择 payload、guard 和局部 write enable,但不能改变 Queue 拓扑或提交边界。
实现必须拒绝会形成组合环路的 firing/Queue 网络。特别是功能 guard 不应直接读取输出
readiness;需要打断 ready 路径时,应插入有存储能力的 Queue/FIFO/elastic register。
10. 与现有 Queue Primitive 的关系
以下 primitive 可以视为
ac.firing的受限特例,但可以继续保留独立 op,以便 verifier、优化和 RTL provider 识别更窄的硬件结构:
纯 Queue firing 如果满足
broadcast或transform的约束,可以 canonicalize 为对应的专用 primitive。
11. 示例
11.1 单输入状态更新
ROB completion 每次消费一个完成事件并 patch 对应 Entry:
RTL 概念等价:
11.2 零输入状态驱动输出
ROB retirement 没有输入 Queue,由 committed head Entry 驱动:
提交条件为:
当
retired.ready = false时,ROB Entry 和head都保持不变。11.3 多输入、多输出和状态更新
Rename 同时消费 decoded instruction 和 free physical register,产生 issue 与 ROB 两个输出,
并更新 rename map:
统一提交条件为:
任何一个条件为假,两个输入、两个输出和 rename map 都不改变。
12. GFSim 对应模型
GFSim 中一个 firing 应作为一个整体 transaction object 执行:
不能让多个独立 GFSim Work 分别提交 Queue 与状态 effect,否则可能产生部分提交。
现有
QueueAtomicTransform可以复用多输入、多输出 Queue transaction 的骨架,但需要增加guard 和 Table/Reg proposal 的统一 commit。
13. RTL 对应结构
一个 firing 的主要 RTL footprint 为:
概念逻辑:
这里的
input_pop和output_push是 Queue storage 的原子提交使能,不等同于直接暴露在组件边界上的 ready-valid 信号。具体 ready-valid 实现可以消除代数上冗余的信号,
但不得让任一输入或输出提前完成,从而改变全有或全无语义。
大型 firing 会形成宽 valid/ready reduction、长 guard 路径和大量 write enable,因此
ac.firing应用于局部的单 tick 原子规则,不应把整个组件或整条流水线包进一个 firing。14. 当前实现与目标语义的差异
截至本文编写时,仓库现有
ac.firing是较窄的显式 Queue-effect region:本文定义的是 Table/Reg 设计需要的目标 Frozen ACIR 语义。实现时至少需要补齐:
在这些能力完成前,本文示例不能视为当前工具链已经可编译的 ACIR。
15. 定义总结
ac.firing可以最终概括为: