Minimizing Logic Expressions
source link: https://lab.whitequark.org/notes/2020-04-06/minimizing-logic-expressions/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
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 foran 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.
#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))
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK