Skip to content

Instantly share code, notes, and snippets.

@adamgreig
Created January 3, 2020 04:14
Show Gist options
  • Save adamgreig/5592c1bb9992c2cbbf8e718bf9f97f8e to your computer and use it in GitHub Desktop.
Save adamgreig/5592c1bb9992c2cbbf8e718bf9f97f8e to your computer and use it in GitHub Desktop.
#lang rosette/safe
(require rosette/lib/angelic rosette/lib/match)
; Circuit building block: NAND gates only
(struct nand (x y) #:transparent)
(define (interpret p)
(match p
[(nand x y) (not (and (interpret x) (interpret y)))]
[_ p]))
; Sketch of basic circuit node
(define (??node x y) (choose* x y (nand x y)))
; Sketch of circuit of given recursive depth and two inputs
(define (??circuit x y depth)
(if (= depth 0)
(??node x y)
(??node (??circuit x y (- depth 1)) (??circuit x y (- depth 1)))))
; Synthesize a circuit of NANDs that matches `f`
(define (find-nands f)
(define-symbolic a b boolean?)
(define sketch (??circuit a b 3))
(define sol (synthesize
#:forall (list a b)
#:guarantee (assert (eq? (interpret sketch) (f a b)))))
(evaluate sketch sol))
; Now find equivalent circuits for basic logic gates
(printf "AND: ")
(find-nands &&)
(printf "OR: ")
(find-nands ||)
(printf "NOR: ")
(define (nor x y) (! (|| x y)))
(find-nands nor)
(printf "NOT A:")
(define (xnot x y) (! x))
(find-nands xnot)
(printf "XOR: ")
(find-nands xor)
(printf "XNOR: ")
(define (xnor x y) (! (xor x y)))
(find-nands xnor)
Welcome to DrRacket, version 7.5 [3m].
Language: rosette/safe, with debugging; memory limit: 256 MB.
AND: (nand (nand a b) (nand a b))
OR: (nand (nand a a) (nand (nand a b) b))
NOR: (nand (nand (nand a (nand a b)) (nand b b)) (nand a (nand a a)))
NOT A:(nand (nand (nand a b) b) a)
XOR: (nand (nand a (nand a b)) (nand (nand a b) b))
XNOR: (nand (nand (nand (nand a b) b) b) (nand (nand (nand a b) b) (nand a (nand a b))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment