Minimizing logic expressions
Tags:While working on reverse-engineering the Microchip ATF15xx CPLD family, I found myself deriving minimal logic functions from a truth table. This useful because while it is easy to sample all possible states of a black box combinatorial function using e.g. boundary scan, these truth tables are unwieldy and don’t provide much insight into the hardware. While a minimal function with the same truth table would not necessarily be the function implemented by the hardware (which may have hidden variables, or simply use a larger equivalent function that is more convenient to implement), deriving one still provides great insight. In this note I explore this process.
My chosen approach (thanks to John Regehr for the suggestion) I got for an earlier project is to implement an interpreter for a simple logic expression abstract syntax tree in Racket and then use Rosette to translate assertions about the results of interpreting an arbitrary logic expression, as well as a cost function, into a query for an SMT solver.
Although I could use an off-the-shelf logic minimizer here (like Espresso), most logic minimizers solve a different problem: quickly translating large designs to simple netlists. However, I would like to have a complex output netlist: the ATF15xx CPLDs have a hardware XOR gate that I would like the minimizer to infer on its own. On the other hand, I don’t really care about the runtime of the minimizer as long as it’s on the order of minutes to hours. Rosette’s flexibility is a perfect match for this task.
The following code demonstrates the approach and its ability to derive a XOR gate from3 the input expression. It can be easily modified for a particular application by extending (or reducing, e.g. for translation to an and-inverter graph) the logic language, or altering the cost function.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
#lang rosette/safe
(require rosette/lib/angelic
rosette/lib/match)
(define (^^ x y) (|| (&& x (! y)) (&& (! x) y)))
(struct lnot (a) #:transparent)
(struct land (a b) #:transparent)
(struct lor (a b) #:transparent)
(struct lxor (a b) #:transparent)
(struct lvar (v) #:transparent)
(struct llit (v) #:transparent)
(define (ldump e)
(match e
[(lnot a) `(! ,(ldump a))]
[(land a b) `(&& ,(ldump a) ,(ldump b))]
[(lor a b) `(\|\| ,(ldump a) ,(ldump b))]
[(lxor a b) `(^^ ,(ldump a) ,(ldump b))]
[(lvar v) v]
[(llit v) v]))
(define (leval e)
(match e
[(lnot a) (! (leval a))]
[(land a b) (&& (leval a) (leval b))]
[(lor a b) (|| (leval a) (leval b))]
[(lxor a b) (^^ (leval a) (leval b))]
[(lvar v) v]
[(llit v) v]))
(define (lcost e)
(match e
[(lnot a) (+ 1 (lcost a))]
[(land a b) (+ 2 (lcost a) (lcost b))]
[(lor a b) (+ 2 (lcost a) (lcost b))]
[(lxor a b) (+ 2 (lcost a) (lcost b))]
[(lvar v) 0]
[(llit v) 1]))
(define (??lexpr terminals #:depth depth)
(apply choose*
(if (<= depth 0) terminals
(let [(a (??lexpr terminals #:depth (- depth 1)))
(b (??lexpr terminals #:depth (- depth 1)))]
(append terminals
(list (lnot a) (land a b) (lor a b) (lxor a b)))))))
(define (lmincost #:forall inputs #:tactic template #:equiv behavior)
(define model
(optimize
#:minimize (list (lcost template))
#:guarantee (assert (forall inputs (equal? (leval template) behavior)))))
(if (unsat? model) model
(evaluate template model)))
(define-symbolic a b c boolean?)
(define f
(lmincost
#:forall (list a b c)
#:tactic (??lexpr (list (lvar a) (lvar b) (lvar c) (llit #f)) #:depth 3)
#:equiv (&& (|| a (! (&& b c))) (! (&& a (|| (! b) (! c)))))))
(displayln (ldump f)) ; (! (^^ (&& c b) a))