Minimizing Logic Expressions

栏目: IT技术 · 发布时间: 5年前

内容简介: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.

minlogic.rkt (download)
#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》,希望对大家有所帮助,如果大家有任何疑问请给我留言,小编会及时回复大家的。在此也非常感谢大家对 码农网 的支持!

查看所有标签

猜你喜欢:

本站部分资源来源于网络,本站转载出于传递更多信息之目的,版权归原作者或者来源机构所有,如转载稿涉及版权问题,请联系我们

引爆点

引爆点

[美] 马尔科姆·格拉德威尔 / 钱清、覃爱冬 / 中信出版社 / 2009-8 / 27.00元

我们的世界看上去很坚固,但在《纽约客》怪才格拉德威尔的眼里,只要你找到那个点,轻轻一触,这个世界就会动起来:一位满意而归的顾客能让新开张的餐馆座无虚席,一位涂鸦爱好者能在地铁掀起犯罪浪潮,一位精明小伙传递的信息拉开了美国独立战争的序幕——这个看起来不起眼的点,却是任何人都不能忽视的引爆点。 《引爆点》是一本谈论怎样让产品发起流行潮的专门性著作。书中将产品爆发流行的现象归因为三种模式:个别人物......一起来看看 《引爆点》 这本书的介绍吧!

CSS 压缩/解压工具
CSS 压缩/解压工具

在线压缩/解压 CSS 代码

html转js在线工具
html转js在线工具

html转js在线工具

HEX CMYK 转换工具
HEX CMYK 转换工具

HEX CMYK 互转工具