内容简介：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.M
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))
以上所述就是小编给大家介绍的《Minimizing Logic Expressions》，希望对大家有所帮助，如果大家有任何疑问请给我留言，小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持！
猜你喜欢:
本站部分资源来源于网络，本站转载出于传递更多信息之目的，版权归原作者或者来源机构所有，如转载稿涉及版权问题，请联系我们。
Twenty Lectures on Algorithmic Game Theory
Tim Roughgarden / Cambridge University Press / 2016-8-31 / USD 34.99
Computer science and economics have engaged in a lively interaction over the past fifteen years, resulting in the new field of algorithmic game theory. Many problems that are central to modern compute......一起来看看 《Twenty Lectures on Algorithmic Game Theory》 这本书的介绍吧!
