Espresso的cube

2022-07-19

我准备介绍一下Espresso。这是第一篇，讲一讲它用来表示简单合取式（elementary conjunction，又称term或cube）的数据结构和相关操作。

目录

• 我说的是哪个Espresso
• 输入与输出：PLA
• Rocket Chip的表示方法
• Positional cube notation
  • 交集、并集
  • Consensus
• cube_struct
• 结尾

我说的是哪个Espresso

Espresso指一系列逻辑最小化程序（约等于卡诺图究极进化版）。Espresso-I诞生于1981年一个关于逻辑操控的研讨会，它是使用递归进行最小化的第一个实现。次年，Espresso-II和它的APL实现诞生了。第三年，伯克利的研究生Richard Rudell用C实现了Espresso-IIC。

Espresso-II所处理的是布尔逻辑，每个变量只可能有三种情况：不存在、x和\bar{x}。Ruddel在1986年将Espresso-IIC扩展到了多值逻辑（Espresso-MV），这项改进让布尔函数的输出可以像输入一样处理，提高了运行速度。第二年，Ruddel又用Espresso的基础设施和Quine–McCluskey的思想实现了Espresso-EXACT，自此，Espresso不再只是启发式算法。

Quine提出质蕴含项可以构成最小化解，所以最初大家都把所有质蕴含项生成出来再排除——直到1994年，Patrick C. McGeer使用Signature cube改进了Espresso-EXACT——在Espresso-SIGNATURE中，得到最小化解不再需要生成所有质蕴含项。

由于资金问题，伯克利最后一次更新Espresso的时间停在了1995年。我们现在仍然可以下载伯克利的最后一版：这一版包含了Espresso-MV、Espresso-EXACT、Espresso-SIGNATURE。本文标题里的Espresso，就是指这一版程序。

如果你想亲自编译、运行它，可以克隆chipsalliance/espresso的2.x分支，这一版使用CMake构建、修改了一些阻止编译的问题。

输入与输出：PLA

Espresso处理的是Programmable logic array，比如下面的例子:

010----0 0001000
0000--0- 0010100
0010-0-- 0011101
001--1-- 0100110
0-00--1- 0100110
1010---- 1001111
0011---- 0100110
01000--- 0101111
010-1--- 0110110
0111---- 1010111
1001---- 0110111
0101---- 0110111

一张卡诺图所处理的数据就是一个单输出的PLA，而Espresso相当于可以同时处理几张卡诺图。同时处理多个的秘诀就是不再局限于布尔逻辑，把PLA中的输出部分当作和输出一样的变量一起处理。也就是说，“0010100”不再代表有7个可以取0、1的输出变量，而代表一个可以取2⁷-1个值的输入变量。^[1]那不是没有输出变量了？画卡诺图时也没有标注哪个是输出——一张卡诺图只有一个输出，只要写出来的输入，就会让输出为1。

现在我们知道了Espresso所处理的数据什么样，可是如何在程序里表示它呢？

Rocket Chip的表示方法

Rocker Chip（RC）中的Decode.scala实现了单输出的Quine–McCluskey方法。在运行时，RC会把N输出的PLA拆成N个PLA，分别最小化后再合起来。所以它的核心数据结构不需要记录输出部分，仅由value和mask构成：

class Term(val value: BigInt, val mask: BigInt = 0) {/* 省略 */}

• 当mask(i)为1时，i变量不存在；
• 当mask(i)为0时，i变量是value(i)。

这样很简洁，但Quine–McCluskey本身可以处理多输出的PLA，结果实现给写死了。

Positional cube notation

Espresso的答案是一个unsigned数组（可以理解成无限长的比特列表），输入部分中，每两位比特按下表翻译：

输出部分也在同一个数组里面：0和1代表无和有（在操作时再把整个输出当成一个多值变量）。Espresso中对cube的处理大多是一个函数两个循环，分别处理布尔变量和多值变量（Espresso把两比特的变量称为binary变量。可以理解，但容易和二进制搞混，所以我称它们为布尔变量）。

Alexandre Janniaux使用OCaml实现了Espresso-MV，他的term如下所示，是布尔值列表的列表。合理怀疑他所用的也是positional cube notation，不过我没细看。

type literal_t = bool list
type cube_t = literal_t list

交集、并集

Positional cube notation的优势不仅在于可以表示多值变量，还在于操作方式简单：交集和并集就只是C语言的按位与和按位或。例如x_0 x_1 x_2 \cup x_1 \bar{x_2} = x_1就是01 01 01 | 11 01 10 = 11 01 11。

与之相比，Rocket Chip的求并集就要复杂些：

// Term类
def merge(x: Term) = {
  // 省略
  val bit = value - x.value
  new Term(value &~ bit, mask | bit)
}

Consensus

Positional cube notation当然不止可以处理简单的交集并集，一个较复杂的例子是用位运算得到consensus。

两个cube间如果N个相反的变量，就称它们间的距离为N。例如x_0 x_2 x_4和\bar{x_0} x_2 x_3间的距离为一（第一个变量相反）。

Consensus就是删掉相反变量，求剩下的cube的交集。同样以x_0 x_2 x_4和\bar{x_0} x_2 x_3为例，它们的consensus就是x_2 x_4 \cap x_2 x_3 = x_2 x_3 x_4。

以下是对布尔变量部分求consensus的代码，a、b是输入，r是输出：

for (int w = 1; w < last; w++) {
    r[w] = x = a[w] & b[w];
    x = ~(x | x >> 1) & 0x55555555;
    if (x) {
        unsigned mask = (x | (x << 1));
        r[w] |= mask & 0xFFFFFFFF;
    }
}

~(x | x >> 1) & 0x55555555的作用是查看a和b间有没有相反的变量，乍看很抽象，但可以枚举所有可能取值来验证：

可见，只要~(x | x >> 1) & 0x55555555的值不是0，就一定有相反变量。之后再用x | (x << 1)作为掩码选择那些相反变量：

在r里为那些相反的变量或上11，就得到了consensus的结果。这一套位运算行云流水，我不知道作者是怎么想出来的。

cube_struct

如前所述，Espresso将两比特的布尔变量和不定长的多值变量按位存储在连续的unsigned数组里，那我们怎么知道第i个变量到底占多长？

Espresso使用如下结构体来记录如何翻译unsigned数组，它是一个全局变量：

struct cube_struct {
    int num_vars, num_binary_vars, num_mv_vars;
    int size;
    int *first_part, *last_part, *part_size, *first_word, *last_word;
    unsigned *binary_mask, *mv_mask, **var_mask;
    // 省略
};

其中num_vars为变量数。带星号的都是长度为num_vars的数组。size是这些变量一共需要多少比特来表示，first_part[i]、last_part[i]表示x_i在哪几位。

计算机并不擅长按比特为最小单位处理信息，它擅长的是以字为最小单位（每种架构字长不一样，Espresso可以被配置成一个字16比特或32比特）。如果你真的要按位处理，最好是以字为单位，对其中的每一位做统一处理。cube_struct中的first_word[i]、last_word[i]用来选择哪个字。var_mask[i]用来提取x_i，以便单独处理一个变量。

结尾

把所有变量都以比特的形式挤在一起存储，是好是坏？挤在一起后，Espresso可以用C语言的位运算对一串变量统一操作，生成汇编后可能只要一条指令就可以处理所有变量——这肯定是好事。但是，要对cube做有选择的操作时，就要用mask进行辅助，有些麻烦。在上世纪，内存比现在金贵，用两位表示一个布尔变量肯定比两个int好，可现在仍然更好么？我不知道。

另一种表示cube的方法是binary decision diagram（BDD）。有一些最小化程序使用BDD，不过我并不了解它们。

下一篇准备介绍一下Espresso的分治策略：还记得1981年的Espresso-I是第一个使用什么进行最小化的实现么？