Espresso的cube

我准备介绍一下Espresso。这是第一篇,讲一讲它用来表示简单合取式(elementary conjunction,又称termcube)的数据结构和相关操作。

目录

我说的是哪个Espresso

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

Espresso-II所处理的是布尔逻辑,每个变量只可能有三种情况:不存在、 x\bar{x}Ruddel1986年将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/espresso2.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的与平面),每一行代表一个cube,例如“0111----”代表 \bar{x_0} x_1 x_2 x_3
  • 空格右边的是输出(PLA的或平面),如果要看第一个输出 y_0 ,就要看“1010----”和“0111----”构成的析取范式。

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

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

Rocket Chip的表示方法

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

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

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

Positional cube notation

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

bits含义
00空(出现于0和1取交集)
10\bar{x_i} (cube包含点0)
01x_i (cube包含点1)
11变量不存在(cube同时包含点0和点1)

输出部分也在同一个数组里面:01代表无和有(在操作时再把整个输出当成一个多值变量)。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的作用是查看ab间有没有相反的变量,乍看很抽象,但可以枚举所有可能取值来验证:

一个布尔变量(两位)
x = a[w] & b[w]01101100
x >> 1?0?1?1?0
x | x >> 1?11111?0
~(x | x >> 1)?00000?1
~(x | x >> 1) & 0b0100000001

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

没有相反变量有相反变量
x0001
x << 10010
x | (x << 1)0011

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是第一个使用什么进行最小化的实现么?