用 Sail 实现 Hack 指令集

Hack 概览 · English · 下一篇：Hack ISA →

这是一个面向学习的、可执行的 Hack ISA family 模型。默认 hack16 是 canonical nand2tetris 机器，hack32 是 32 位 Verylogic 扩展；共享 Sail 语义描述 ALU、寄存器、内存与控制流，再通过 Sail C 后端运行真实 Hack 汇编程序。

如果 nand2tetris 教你“怎样从 NAND 门搭出一台计算机”，这个仓库关注的是紧接着的一层：

怎样把处理器手册中的指令行为，写成一份精确、可检查、还能真正运行的 ISA 规范？

本教程聚焦 Hack 模块及其 ISA 层行为，不模拟门级电路或芯片时序。

先理清几个名字

Hack 从哪里来？

Hack 是课程与教材 The Elements of Computing Systems（通常称为 nand2tetris）中设计的一台 16 位教学计算机。学习者从 NAND 门开始，依次完成组合逻辑、ALU、寄存器、CPU、汇编器、虚拟机、编译器和操作系统。

与本仓库最相关的是：

Project 05: Computer Architecture —— 用 HDL 构建 Hack CPU、Memory 和 Computer；
Project 06: Assembler —— 把 Hack 汇编翻译为 16 位机器码；
教材第 4 章介绍机器语言，第 5 章介绍 Hack 硬件体系结构。

nand2tetris 是课程/项目名，Hack 才是这里实现的 CPU 与指令集名称。

Sail 是什么？

Sail 是一种用来描述指令集架构（ISA）的强类型语言。它适合表达：

一条指令的位编码；
指令解码后的结构；
寄存器和内存状态；
每条指令如何改变架构状态；
可执行测试，以及面向 C、OCaml 和定理证明工具的后端。

它看起来有一点像 OCaml，但 Sail 不是 OCaml。本仓库使用 Sail 的类型检查与 C 代码生成能力，让同一份 ISA 描述既是可读规范，也是可运行实现。工作区级的为什么选择 Sail会进一步比较它与自然语言、C/C++、Verilog/SystemVerilog、临时模型和证明助理各自适合的层次。

nandgame.com 又是什么？

nandgame.com 是另一条很直观的交互式学习路线：在浏览器中从 NAND 门开始，一步步搭建逻辑门、算术部件、处理器和计算机。它非常适合建立硬件直觉；nand2tetris 提供系统课程与 Hack 平台；本仓库则把注意力放在 ISA 语义和可执行规范 上。三者可以互补，但不应把各自的电路或指令集细节混为一谈。

你会在这里学到什么

读完并运行本项目后，你应该能回答：

Hack 的两种指令如何编码为 hack16 与 hack32 机器字？
A、D、PC 和 RAM 构成了哪些可观察的架构状态？
C 指令中的 a、comp、dest、jump 字段如何共同决定一次状态转换？
为什么同时写入 A 与 M 或发生跳转时，内存地址和跳转目标必须使用旧的 A？
如何把汇编程序、机器码、Sail driver、生成的 C 程序和断言串成一条回归测试链？

快速开始

1. 准备环境

先安装 Pixi，然后在仓库根目录执行：

pixi run just install
pixi run sail --version
pixi run just hack check

项目固定使用 Sail 0.20.2，并安装到 Git 忽略的 .pixi/sail/，不依赖系统 PATH 中的 Sail。支持的宿主平台是：

Windows AMD64；
Linux x86_64；
Linux aarch64。

这个 Sail 版本没有官方 macOS 二进制资产，因此 macOS 不在支持的平台集合中。Pixi 还会提供 Python、Pytest、Just、GCC/MinGW GCC 和 GMP。

2. 运行第一个 Hack 程序

pixi run just hack list
pixi run just hack run multiply                    # 默认 hack16
pixi run just hack run multiply --profile hack32

下面示例继续使用默认 hack16；hack32 经过相同源码流程，但机器字为 32 位，状态十六进制输出也更宽。multiply 使用重复加法计算 6 × 7。源码在 isa/hack/programs/multiply.asm：

.description Repeated-addition multiplication: 6 times 7

SET R0, 6
SET R1, 7
SET R2, 0

(LOOP)
JEQ R1, DONE
@R0
D=M
@R2
M=D+M
DEC R1
GOTO LOOP

(DONE)
HALT

.assert R2 == 42

SET、JEQ target, label、DEC、GOTO 和 HALT 是仓库汇编器提供的 Hack+ 伪指令。汇编器先把它们替换成 canonical A/C 汇编，再进行标签解析，并按所选 profile 生成机器字。例如：

// SET R0, 6
@6
D=A
@R0
M=D

// JEQ R1, DONE
@R1
D=M
@DONE
D;JEQ

所以伪指令只是汇编层的便捷写法，不会扩展 Sail 中定义的 ISA。全部展开规则及其对 A、D 的影响见 Hack ISA 详解：Hack+ 如何降级。.description 不产生机器字：workflow 用它发现程序，artifact.py 将它保存在带注释机器映像 manifest 的 description 字段。

3. 观察 `.assert` 成功与失败

multiply 最后一行：

.assert R2 == 42

会被 executor 写成生成 driver 中的 Sail 断言。正常运行时可看到：

ASSERT PASS
A  = ...
D  = ...
PC = ...
R2 = 0x002A

如果故意改成 .assert R2 == 43，核心错误类似：

Assertion failed: assertion R2 == 0x002B from source line 20 failed

生成程序随后以状态 1 退出，run 或 test 失败。错误指向原始 .asm 行号；Python workflow 不比较打印文本，真正判定发生在 Sail 中。共享 equality/ordered 语法见公共教学契约，Hack target 见执行器与测试。

4. 查看真正执行的机器码

pixi run just hack assemble multiply
pixi run just hack run multiply full

默认的 summary 为每个 A/C 机器字显示规范化源码，把 Hack+ 展开标为 [i/n] 源伪指令 => 正式指令，并将行内汇编注释放在最右侧。显式选择 full 后，会保留精确源码文本，并增加更多 driver 阶段和断言解释；

默认输出位于 isa/hack/.build/hack16/asm/multiply/multiply.hack，每条指令仍是标准 16 位 Hack 机器字，只额外保留 ROM 地址、源码行和伪指令展开信息。--profile hack32 则把 32 位 artifact 写入 .build/hack32/asm/multiply/：

0000000000000110 // ROM[0000] L5 [1/4] SET R0, 6 => @6 // RAM[0] = 被乘数
1110110000010000 // ROM[0001] L5 [2/4] SET R0, 6 => D=A // RAM[0] = 被乘数

这一步很适合把教材中的编码表、汇编源码和 Sail 解码规则放在一起对照。

跟着 profile 模型读一遍处理器

当前模型按责任拆分，建议依次阅读：

从 model/profiles/hack16.sail 开始：先看 profile 位宽与合法性，再沿 include 进入共享 core；
model/core.sail：instruction/exception 类型、架构状态、total 64-control ALU、fetch/decode/encode/execute 和 hack_step()；
回到 hack16.sail 底部阅读 scattered A/C mapping clauses，再与 hack32.sail 的 C envelope 对比；
查看 projects/hack16.sail_project 与 projects/hack32.sail_project：每个完整构建闭包都只指向自己的一个 profile 入口。

Profile	机器字/`A`/`D`	A 指令	C 指令
`hack16`	16 位	`0` + 15 位立即数	`111accccccdddjjj`
`hack32`	32 位	`0` + 31 位立即数	`0xFFFF` + `111accccccdddjjj`

两个 profile 都使用 15 位 PC、各 32768 word 的 ROM/RAM，并以旧 A[14:0] 完成 RAM 写入和跳转。hack32 的 A 高位仍参与 32 位 ALU 运算。汇编器只暴露 canonical nand2tetris comp mnemonic，而共享门级 control ALU 定义六位 control 的全部 64 种结果。

从汇编到可执行程序

完整执行链如下：

programs/*.asm
  │  两遍汇编 + Hack+ 展开
  ▼
.build/<profile>/asm/<program>/<program>.hack
  │  重新加载机器字、断言和 HALT 元数据
  ▼
生成的 .driver.sail + projects/<profile>.sail_project
  │  Sail 类型检查与 C 后端
  ▼
.build/<profile>/asm/<program>/<program>.exe
  │  执行到 HALT 或步数上限；离开已加载映像会报错
  ▼
检查源码中的 .assert

汇编后再重新读取 .hack 是有意设计：运行阶段只依赖磁盘上真实生成的机器码与元数据，不携带汇编器中的隐藏状态。

各部分职责：

isa/hack/model/ 与 projects/*.sail_project：共享语义与 profile composition；
isa/hack/tools/assembler.py：两遍汇编、Hack+ 展开、带注释机器码；
isa/hack/tools/executor.py：生成 Sail driver，调用 C 后端并执行；
isa/hack/programs/*.asm：示例与端到端回归程序；
isa/hack/tests/sail/<profile>/conformance.sail：直接验证 profile 编码、ALU、跳转、写回与状态转换；
isa/hack/tests/：汇编器和执行器的 Python 测试。

建议的学习实验

实验一：对照 A/C 指令编码

阅读所选 profile 的 mapping clauses，编码时直接使用 encdec(instruction)，再沿 include 查看 model/core.sail 中负责合法性检查的 decode_hack；
写一小段标准 Hack 汇编；
执行 pixi run just hack assemble <程序名>；
先把默认 hack16 产物中的 16 位机器字与 Project 06 编码表对照，再观察 hack32 如何用 32 位 envelope 承载同一组 C 指令控制字段。

实验二：增加一个 ALU 回归用例

在对应 tests/sail/<profile>/conformance.sail 中增加断言，先运行窄检查，再运行完整测试：

pixi run just hack check --profile hack32
pixi run just hack test

这里的测试直接调用 Sail 函数，不经过 Python 模拟 ISA。

实验三：写一个新的汇编程序

新建 isa/hack/programs/<名称>.asm，文件 stem 就是程序名；
添加一条 .description <非空说明>，供 workflow 自动发现；
在源码中加入至少一条 .assert；
执行 pixi run just hack run <名称>；
执行 pixi run just hack test 做完整回归。

断言示例：

.assert R2 == 42
.assert signed(R6) >= -5
.assert unsigned(R6) > 0x8000
.assert RAM[100] != 0

项目边界

模型的范围限定在 ISA 层：

实现 A/C 指令、ALU、寄存器、RAM 和 PC 状态转换；
使用普通 RAM 表示 15 位地址空间，Screen、Keyboard 等内存映射设备行为不在模型范围内；
不模拟 NAND 门、芯片延迟或 nand2tetris HDL；
Hack+ 只是汇编器便利语法，不是 Hack ISA 的扩展；
执行路径使用 Sail C 后端，不对模型作已完成形式化证明的声明。

如果你想学习“门怎样组成 CPU”，先做 nandgame 或 nand2tetris Projects 01–05；如果你想学习“怎样精确描述 CPU 执行指令”，就从一个 profile 入口开始，沿 include 进入 model/core.sail，再回到该 profile 的 mapping clauses。

延伸资源

资源	推荐用途
Sail 项目主页	了解 Sail 的目标、后端和研究背景
Sail GitHub	源码、发行版、示例 ISA 与编辑器支持
Sail Language Reference	查询语法、类型、mapping、register 和后端
nand2tetris 官网	课程、软件工具、项目材料与 Hack 平台入口
The Elements of Computing Systems	系统学习从硬件到操作系统的完整路径
Project 05	构建 Hack CPU、Memory 与 Computer
Project 06	实现 Hack 汇编器并理解机器码编码
NandGame	在浏览器中从 NAND 门交互式搭建计算机

下一步：理解 Hack 的机器契约。

#用 Sail 实现 Hack 指令集

#先理清几个名字

#Hack 从哪里来？

#Sail 是什么？

#nandgame.com 又是什么？

#你会在这里学到什么

#快速开始

#1. 准备环境

#2. 运行第一个 Hack 程序

#3. 观察 .assert 成功与失败

#4. 查看真正执行的机器码

#跟着 profile 模型读一遍处理器

#从汇编到可执行程序

#建议的学习实验

#实验一：对照 A/C 指令编码

#实验二：增加一个 ALU 回归用例

#实验三：写一个新的汇编程序

#项目边界

#延伸资源