Quaigh

逻辑简化和分析工具

本 crate 提供了逻辑优化、综合、技术映射和分析的工具。我们的目标是提供一个易于使用的库，并随着时间的推移不断提高其质量，以匹配工业工具。

使用和特性

Quaigh 提供了一个命令行工具，可以使用 Cargo 进行安装： cargo install quaigh。

显示可用命令

quaigh help

atpg 命令执行 自动测试模式生成，为设计创建测试向量。

quaigh atpg mydesign.bench -o atpg.test

check-equivalence 命令执行有界 等价性检查，以确认设计的功能在变换后得到保留。

quaigh equiv mydesign.bench optimized.bench

optimize 命令执行 逻辑优化。目前，逻辑优化远未达到最佳状态：对于生产设计，您通常应坚持使用 Yosys 中包含的工具。

quaigh opt mydesign.bench -o optimized.bench

Quaigh 支持部分 Blif 文件格式，以及 ISCAS 基准测试使用的简单 Bench 文件格式。基准测试可以从 这里 下载。随着时间的推移，将添加更多功能，例如技术映射、算子优化等。完整的文档可在 docs.rs 上找到。

开发

主要的数据结构是 Network，它是一个逻辑电路的典型门-反相器-图表示。反相器是隐含的，只占用 Signal 中的一个比特。它支持许多种逻辑，并且所有逻辑都可以存在于同一个电路中。

• 如Xor、Mux和Maj3这样的复杂门都是一等公民。
• 带有使能和复位功能的触发器是直接表示的。

在大多数逻辑优化库（如 ABC、Mockturtle 等）中，有许多不同的方式来表示逻辑，使用不同的数据结构：AIG、MIG、LUT等。根据电路的不同，可能更偏好某一视图。利用它们所有可能需要分割电路，这使得大多数操作变得更加复杂。更通用的网表，如Yosys RTLIL，将允许在单一数据结构中包含所有类型的逻辑门。由于它们不限制表示的函数，因此难以直接用于逻辑优化。

Quaigh的目标介于两者之间。所有算法共享相同的网表表示，即 Network，但有一些限制使得优化变得容易。

• 所有门只有一个输出，表示一个单一的二进制值。
• 门按照拓扑顺序排列（一个门的索引高于它的输入）。
• 不表示名称和设计层次结构。

例如，这里是一个全加器电路。

let mut net = Network::new();
let i0 = net.add_input();
let i1 = net.add_input();
let i2 = net.add_input();
let carry = net.add(Gate::maj(i0, i1, i2));
let out = net.add(Gate::xor3(i0, i1, i2));
net.add_output(carry);
net.add_output(out);

除了核心数据结构外，Quaigh还提供用于逻辑优化、仿真（包括故障仿真）和测试模式生成的算法。在优化和等价性检查方面，Quaigh尽可能依赖其他包。

• Kissat（使用 rustsat）作为Sat求解器，
• Highs（使用 good_lp）作为优化求解器。