Emina Torlak

Lab 2: Going Pro with Solver-Aided Programming

The following exercises explore the concepts covered in Part 2 of the tutorial on solver-aided programming presented at CAV 2019.

A shallow circuit SDSL

Consider the problem of building a simple language for testing, verifying, and synthesizing boolean circuits. We are interested in circuit programs that are in static single assignment (SSA) form, and that use one of the following operations: Not, And, Or, Iff, and Xor, with their usual meaning.

Here is what a shallow embedding of this language would look like in Rosette:

#lang rosette

(define (Not a)   (if a #f #t))
(define (And a b) (if a b #f))
(define (Or a b)  (if a #t b))
(define (Iff a b) (if a b (! b)))
(define (Xor a b) (if a (! b) b))

And here are a few programs in this language:

(define (Niffp a b c d)
  (define r1 (Iff a b))
  (define r2 (Iff c d))
  (define r3 (Iff r1 r2))
  (define r4 (Not r3))
  r4)

(define (NXp a b c d)
  (define r1 (Xor a b))
  (define r2 (Not r1))
  (define r3 (Xor c d))
  (define r4 (Not r3))
  (define r5 (Xor r2 r4))
  r5)
  
(define (AIGp a b c d)
  (define r1 (Not a))
  (define r2 (Not b))
  (define r3 (And r1 r2))
  (define r4 (Not r3))
  (define r5 (And a b))
  (define r6 (Not r5))
  (define r7 (And r4 r6))
  (define r8 (Not r7))
  (define r9 (Not c))
  (define r10 (Not d))
  (define r11 (And r9 r10))
  (define r12 (Not r11))
  (define r13 (And c d))
  (define r14 (Not r13))
  (define r15 (And r12 r14))
  (define r16 (Not r15))
  (define r17 (Not r8))
  (define r18 (Not r16))
  (define r19 (And r17 r18))
  (define r20 (Not r19))
  (define r21 (And r8 r16))
  (define r22 (Not r21))
  (define r23 (And r20 r22))
  (define r24 (Not r23))
  (define r25 (Not r24))
  r25)

A deep circuit SDSL

The above exercise show that a shallow embedding makes it cumbersome to specify sketches of arbitrary length. In general, it’s a good rule of thumb to use deep embedding if you want to do synthesis; shallow embedding works well for verification and solving.

Let’s build a deep embedding of the circuit SDSL, reusing the semantics of the circuit operations we defined in the previous part of the lab.

To do so, add the following line to the module containing your shallow embedding and save it as, say, “shallow.rkt”:

#lang rosette

(provide Not And Or Xor Iff ver syn ??inst)
...

Now, create a file “deep.rkt” that imports the shallow semantic operations, but prefixes each operation’s name with “s” (for “shallow” or “semantics”), so that we can reuse the original names in the new implementation:

#lang rosette

(require 
  rosette/lib/match
  (prefix-in s (only-in "shallow.rkt" Not And Or Iff Xor)))

(struct Not (a)   #:transparent)
(struct And (a b) #:transparent)
(struct Or  (a b) #:transparent)
(struct Iff (a b) #:transparent)
(struct Xor (a b) #:transparent)

(define (interpret prog in)
  (define reg (make-vector (+ (car prog) (length (cdr prog))) #f))
  (define (store i v) (vector-set! reg i v))
  (define (load i) (vector-ref reg i))
  (define (last) (sub1 (vector-length reg)))
  (for ([(i idx) (in-indexed in)])
    (store idx i))
  (for ([(inst idx) (in-indexed (cdr prog))])
    (store
     (+ idx (car prog)) 
     (match inst
       [(Not a)   (sNot (load a))]
       [(And a b) (sAnd (load a) (load b))]
       [(Or a b)  (sOr (load a) (load b))]
       [(Xor a b) (sXor (load a) (load b))]
       [(Iff a b) (sIff (load a) (load b))])))
  (load (last)))

Circuit programs are now represented as a list where the first element is the number of arguments to the program, and the remaining elements are instructions. Each instruction’s fields are integers that identify the registers containing the instruction’s inputs. For example:

(define NXp
  (list 4 (Xor 0 1) (Not 4) (Xor 2 3) (Not 6) (Xor 5 7)))

(define Niffp
  (list 4 (Iff 0 1) (Iff 2 3) (Iff 4 5) (Not 6)))