## BAT Examples

The following are two simple examples to help you get the basic idea on how to define and solve problems using BAT. Many more complicated examples can be found on our benchmarks page.### ALU

The BAT input file for this example can be found here.

((:functions (maj (1) ((a 1) (b 1) (c 1)) (or (and a b) (and b c) (and a c))) (fa (2) ((a 1) (b 1) (cin 1)) (cat (maj a b cin) (xor a b cin))) (mux-4 (1) ((in0 1) (in1 1) (in2 1) (in3 1) (sel 2)) (local ((nsel0 (not (sel 0))) (nsel1 (not (sel 1)))) (or (and in0 nsel0 nsel1) (and in1 (sel 0) nsel1) (and in2 nsel0 (sel 1)) (and in3 (sel 0) (sel 1))))) (alu-slice (2) ((a 1) (b 1) (cin 1) (bnegate 1) (op 2)) (local ((nb (xor bnegate b)) (res0 (and a nb)) (res1 (or a nb)) (((cout 1) (res2 1)) (fa a nb cin))) (cat cout (mux-4 res0 res1 res2 1u op)))) (alu-2-bit (4) ((a 2) (b 2) (bnegate 1) (op 2)) (local ((c 2)) (((t0 (c 0)) (alu-slice (a 0) (b 0) bnegate bnegate op)) ((t1 (c 1)) (alu-slice (a 1) (b 1) t0 bnegate op)) (zero (= c 0))) (cat t1 c zero)))) (:vars (i1 2) (i2 2) (bn 1) (op 2) (out 2) (cout 1) (zero 1)) (:init (and (= out 0) (= cout 1b1) (= zero 1b0))) (:trans (= (cat (next cout) (next out) (next zero)) (alu-2-bit i1 i2 bn op))) (:spec (AG (<-> zero (not cout)))))

This example describes an ALU. We cover pieces of this code in the documentation. The functions section takes a list of
function definitions. In this example, we define 5 functions. A
function definition starts with the function name. Our first function
is called

The third part of a function definition is its arguments. This is just
a list of variable definitions just like the ones in the

In our example, the

### Two Stage Pipeline Machine

The BAT input file for this example can be found here.

We now present an example of a 2-bit 2 stage pipeline machine. In the machine spec, we give definitions for the ISA and RTL level models of the 2 stage pipelined machine, and we check that the pipelined machine refines the ISA machine. We will formulate this as a :forall problem. That is, we will present BAT with a formula over a given set of user-defined functions and variables and ask BAT to determine if it is true for all inputs. Let's start with the variable definitions:

((mastate 7) (rf 4 2) (imem 4 7))

We briefly walk through this example. The machine state is
represented by 3 variables, declared in the

((getppc (2) ((mastate 7)) (bits mastate 0 1)) (getewdest (2) ((mastate 7)) (bits mastate 2 3)) (getewresult (2) ((mastate 7)) (bits mastate 4 5)) (getewregwrite (1) ((mastate 7)) (bits mastate 6 6)) (src1 (2) ((inst 7)) (bits inst 5 6)) (src2 (2) ((inst 7)) (bits inst 3 4)) (dest (2) ((inst 7)) (bits inst 1 2)) (getregwrite (1) ((inst 7)) (bits inst 0 0)) (nextspc (2) ((pc 2)) (bits (+ pc 1u) 0 1)) (nextsrf (4 2) ((inst 7) (regwrite 1) (rf 4 2) (result 2)) (if regwrite (set rf (dest inst) result) rf)) (step-isa ((2) (4 2) (4 7)) ((pc 2) (rf 4 2) (imem 4 7)) (local ((inst (get imem pc)) (regwrite (getregwrite inst)) (arg1 (get rf (src1 inst))) (arg2 (get rf (src2 inst))) (result (bits (+ arg1 arg2) 0 1))) (mv (nextspc pc) (nextsrf inst regwrite rf result) imem))) (nextppc (2) ((pc 2)) (bits (+ pc 1u) 0 1)) (nextprf (4 2) ((rf 4 2) (ewregwrite 1) (ewresult 2) (ewdest 2)) (if ewregwrite (set rf ewdest ewresult) rf)) (step-ma ((7) (4 2) (4 7)) ((mastate 7) (rf 4 2) (imem 4 7)) (local ((ppc (getppc mastate)) (ewdest (getewdest mastate)) (ewregwrite (getewregwrite mastate)) (ewresult (getewresult mastate)) (inst (get imem ppc)) (arg1_tmp (get rf (src1 inst))) (arg2_tmp (get rf (src2 inst))) (arg1 (if (and ewregwrite (= ewdest (src1 inst))) ewresult arg1_tmp)) (arg2 (if (and ewregwrite (= ewdest (src2 inst))) ewresult arg2_tmp)) (result (bits (+ arg1 arg2) 0 1))) (mv (cat (getregwrite inst) result (dest inst) (nextppc ppc)) (nextprf rf ewregwrite ewresult ewdest) imem))) (flush-ma ((7) (4 2) (4 7)) ((mastate 7) (rf 4 2) (imem 4 7)) (local ((ppc (getppc mastate)) (ewdest (getewdest mastate)) (ewregwrite (getewregwrite mastate)) (ewresult (getewresult mastate)) (inst (get imem ppc)) (arg1_tmp (get rf (src1 inst))) (arg2_tmp (get rf (src2 inst))) (arg1 (if (and ewregwrite (= ewdest (src1 inst))) ewresult arg1_tmp)) (arg2 (if (and ewregwrite (= ewdest (src2 inst))) ewresult arg2_tmp)) (result (bits (+ arg1 arg2) 0 1))) (mv (cat 1b0 result (dest inst) ppc) (nextprf rf ewregwrite ewresult ewdest) imem))))

The first 4 functions simply access the pieces of the

The

The next 3 functions describe how the RTL model is stepped. The

Finally, we have a function that is very similar to the

(local (((w1 s-rf s-imem) (flush-ma mastate rf imem)) (s-pc (getppc w1)) ((u-pc u-rf u-imem) (step-isa s-pc s-rf s-imem)) ((v v-rf v-imem) (step-ma mastate rf imem)) ((v1 v1-rf v1-imem) (flush-ma v v-rf v-imem))) (and (= (getppc v1) u-pc) (= v1-rf u-rf)))

We set

We then step the original RTL machine and flush again, giving us

### Decimal Counter

The following example is a BAT model of a 2 digit decimal counter. The model describes the circuit for incrementing the decimal counter. Each digit of the decimal counter is represented using a 4-bit unsigned bit-vector. A valid value of a 4-bit unsigned bit-vector representing a digit can only range between 0 and 9. The property checked is that if each of the digits of the decimal counter are valid, then the digits should remain valid after the decimal counter is incremented.

:forall ((x 8)) ((inc4 ((4) (1)) ((x 4)) (local ((xu (cat 0b0 x))) (if (< xu 9) (mv (mod+ x 1) 0b0) (mv 0 0b1)))) (inc_digit ((4) (1)) ((x 4) (c 1)) (if c (inc4 x) (mv x 0b0))) (valid_digits (1) ((x 8)) (and (< (cat 0b0 (bits x 0 3)) 10) (< (cat 0b0 (bits x 4 7)) 10))) (inc_digits (8) ((x 8)) (local ((((x0 4) (c0 1)) (inc4 (bits x 0 3))) (((x1 4) (c1 1)) (inc_digit (bits x 4 7) c0))) (cat x1 x0)))) (-> (valid_digits x) (valid_digits (inc_digits x)))

The state of the decimal counter is represented by a variable

((x 8))

The BAT functions used to model the circuit that increments the
decimal counter is described next. The

(inc4 ((4) (1)) ((x 4)) (local ((xu (cat 0b0 x))) (if (< xu 9) (mv (mod+ x 1) 0b0) (mv 0 0b1))))

The

(inc_digit ((4) (1)) ((x 4) (c 1)) (if c (inc4 x) (mv x 0b0)))

The

(inc_digits (8) ((x 8)) (local ((((x0 4) (c0 1)) (inc4 (bits x 0 3))) (((x1 4) (c1 1)) (inc_digit (bits x 4 7) c0))) (cat x1 x0)))

The

(valid_digits (1) ((x 8)) (and (< (cat 0b0 (bits x 0 3)) 10) (< (cat 0b0 (bits x 4 7)) 10)))

The formula corresponding to the correctness property of the
decimal counter is given below. The formula states that if the digit
of any state of the decimal counter is valid as given by the

(-> (valid_digits x) (valid_digits (inc_digits x)))

The example was generated using a simple Lisp program that is
given below. The top-level function of the lisp program

(defun gen-valid_digits (n) (loop for i from 0 below (* 4 n) by 4 collect `(< (cat 0b0 (bits x ,i ,(+ i 3))) 10) into lst finally (return `(valid_digits (1) ((x ,(* 4 n))) (and ,@lst))))) (defun xi (i) (read-from-string (format nil "x~D" i))) (defun ci (i) (read-from-string (format nil "c~D" i))) (defun gen-inc_digits (n) (loop for i from 1 below n for xi = (xi i) for i4 = (* i 4) collect `(((,xi 4) (,(ci i) 1)) (inc_digit (bits x ,i4 ,(+ i4 3)) ,(ci (1- i)))) into bindings collect xi into cat-args finally (return `(inc_digits (,(* 4 n)) ((x ,(* 4 n))) (local ,(cons '(((x0 4) (c0 1)) (inc4 (bits x 0 3))) bindings) (cat ,@(reverse (cons 'x0 cat-args)))))))) (defun gen_dec_counter (n) (print :forall) (print `((x ,(* 4 n)))) (print `((inc4 ((4) (1)) ((x 4)) (local ((xu (cat 0b0 x))) (if (< xu 9) (mv (mod+ x 1) 0b0) (mv 0 0b1)))) (inc_digit ((4) (1)) ((x 4) (c 1)) (if c (inc4 x) (mv x 0b0))) ,(gen-valid_digits n) ,(gen-inc_digits n))) (print '(-> (valid_digits x) (valid_digits (inc_digits x)))) nil)

### Sudoku Solver

The following example shows how BAT can be used to solve Sudoku problems. We wrote lisp code that generates a BAT file that can be used to solve Sudoku problems. The idea was to generate 91 variable, B11, ..., B99 (Bij stands for Board position i, j). Each variable is constrainted to be a 5-bit bit-vector between 1 and 9. The lisp code is shown first, and then the BAT code it generates follows. To solve a particular Sudoku problem, just enter the constraints for the board positions with fixed values where indicated. We include a problem from http://dingo.sbs.arizona.edu/~sandiway/sudoku/examples.html whose description is:These puzzles are not fun anymore. I wonder if they are tractable for non-computer puzzle solving. At some steps, they seem to require long chains of inference just to eliminate a single value.

This is solved in about 1/10 of a second (wall clock time).

The lisp code is:

; Generate the list of variables from the declarations (defun gen-vars () (mapcar #'car (gen-var-decls))) ; Generate the different function (defun gen-different () (loop for i from 1 to 9 collect `(,(read-from-string (format nil "X~D" i)) 5) into vars collect (loop for j from (1+ i) to 9 collect `(not (= ,(read-from-string (format nil "X~D" i)) ,(read-from-string (format nil "X~D" j))))) into body finally (return `(different (1) ,vars ,(cons 'and (reduce #'append body)))))) (defun different-row-col (row?) (loop for i from 1 to 9 collect (loop for j from 1 to 9 collect (read-from-string (format nil "B~D~D" (if row? i j) (if row? j i)))) into row-diff finally (return (mapcar #'(lambda (x) (cons 'different x)) row-diff)))) (defun different-block () (loop for i from 0 to 2 collect (loop for j from 0 to 2 collect (loop for r from (1+ (* i 3)) to (* (1+ i) 3) collect (loop for c from (1+ (* j 3)) to (* (1+ j) 3) collect (read-from-string (format nil "B~D~D" r c))) into r-l finally (return (reduce #'append r-l))) into j-l finally (return (mapcar #'(lambda (x) (cons 'different x)) j-l))) into i-l finally (return (reduce #'append i-l)))) (defun sudoku () (print :exists) (print (gen-var-decls)) (print `((in-range (1) ((x 5)) (and (<= 1 x) (<= x 9))) ,(gen-different))) (print `(and ,@(mapcar #'(lambda (x) `(in-range ,x)) (gen-vars)) ,@(different-row-col t) ,@(different-row-col nil) ,@(different-block))) nil) (sudoku)

The BAT file generated is

:exists ((B11 5) (B12 5) (B13 5) (B14 5) (B15 5) (B16 5) (B17 5) (B18 5) (B19 5) (B21 5) (B22 5) (B23 5) (B24 5) (B25 5) (B26 5) (B27 5) (B28 5) (B29 5) (B31 5) (B32 5) (B33 5) (B34 5) (B35 5) (B36 5) (B37 5) (B38 5) (B39 5) (B41 5) (B42 5) (B43 5) (B44 5) (B45 5) (B46 5) (B47 5) (B48 5) (B49 5) (B51 5) (B52 5) (B53 5) (B54 5) (B55 5) (B56 5) (B57 5) (B58 5) (B59 5) (B61 5) (B62 5) (B63 5) (B64 5) (B65 5) (B66 5) (B67 5) (B68 5) (B69 5) (B71 5) (B72 5) (B73 5) (B74 5) (B75 5) (B76 5) (B77 5) (B78 5) (B79 5) (B81 5) (B82 5) (B83 5) (B84 5) (B85 5) (B86 5) (B87 5) (B88 5) (B89 5) (B91 5) (B92 5) (B93 5) (B94 5) (B95 5) (B96 5) (B97 5) (B98 5) (B99 5)) ((IN-RANGE (1) ((X 5)) (AND (<= 1 X) (<= X 9))) (DIFFERENT (1) ((X1 5) (X2 5) (X3 5) (X4 5) (X5 5) (X6 5) (X7 5) (X8 5) (X9 5)) (AND (NOT (= X1 X2)) (NOT (= X1 X3)) (NOT (= X1 X4)) (NOT (= X1 X5)) (NOT (= X1 X6)) (NOT (= X1 X7)) (NOT (= X1 X8)) (NOT (= X1 X9)) (NOT (= X2 X3)) (NOT (= X2 X4)) (NOT (= X2 X5)) (NOT (= X2 X6)) (NOT (= X2 X7)) (NOT (= X2 X8)) (NOT (= X2 X9)) (NOT (= X3 X4)) (NOT (= X3 X5)) (NOT (= X3 X6)) (NOT (= X3 X7)) (NOT (= X3 X8)) (NOT (= X3 X9)) (NOT (= X4 X5)) (NOT (= X4 X6)) (NOT (= X4 X7)) (NOT (= X4 X8)) (NOT (= X4 X9)) (NOT (= X5 X6)) (NOT (= X5 X7)) (NOT (= X5 X8)) (NOT (= X5 X9)) (NOT (= X6 X7)) (NOT (= X6 X8)) (NOT (= X6 X9)) (NOT (= X7 X8)) (NOT (= X7 X9)) (NOT (= X8 X9))))) (AND (IN-RANGE B11) (IN-RANGE B12) (IN-RANGE B13) (IN-RANGE B14) (IN-RANGE B15) (IN-RANGE B16) (IN-RANGE B17) (IN-RANGE B18) (IN-RANGE B19) (IN-RANGE B21) (IN-RANGE B22) (IN-RANGE B23) (IN-RANGE B24) (IN-RANGE B25) (IN-RANGE B26) (IN-RANGE B27) (IN-RANGE B28) (IN-RANGE B29) (IN-RANGE B31) (IN-RANGE B32) (IN-RANGE B33) (IN-RANGE B34) (IN-RANGE B35) (IN-RANGE B36) (IN-RANGE B37) (IN-RANGE B38) (IN-RANGE B39) (IN-RANGE B41) (IN-RANGE B42) (IN-RANGE B43) (IN-RANGE B44) (IN-RANGE B45) (IN-RANGE B46) (IN-RANGE B47) (IN-RANGE B48) (IN-RANGE B49) (IN-RANGE B51) (IN-RANGE B52) (IN-RANGE B53) (IN-RANGE B54) (IN-RANGE B55) (IN-RANGE B56) (IN-RANGE B57) (IN-RANGE B58) (IN-RANGE B59) (IN-RANGE B61) (IN-RANGE B62) (IN-RANGE B63) (IN-RANGE B64) (IN-RANGE B65) (IN-RANGE B66) (IN-RANGE B67) (IN-RANGE B68) (IN-RANGE B69) (IN-RANGE B71) (IN-RANGE B72) (IN-RANGE B73) (IN-RANGE B74) (IN-RANGE B75) (IN-RANGE B76) (IN-RANGE B77) (IN-RANGE B78) (IN-RANGE B79) (IN-RANGE B81) (IN-RANGE B82) (IN-RANGE B83) (IN-RANGE B84) (IN-RANGE B85) (IN-RANGE B86) (IN-RANGE B87) (IN-RANGE B88) (IN-RANGE B89) (IN-RANGE B91) (IN-RANGE B92) (IN-RANGE B93) (IN-RANGE B94) (IN-RANGE B95) (IN-RANGE B96) (IN-RANGE B97) (IN-RANGE B98) (IN-RANGE B99) (DIFFERENT B11 B12 B13 B14 B15 B16 B17 B18 B19) (DIFFERENT B21 B22 B23 B24 B25 B26 B27 B28 B29) (DIFFERENT B31 B32 B33 B34 B35 B36 B37 B38 B39) (DIFFERENT B41 B42 B43 B44 B45 B46 B47 B48 B49) (DIFFERENT B51 B52 B53 B54 B55 B56 B57 B58 B59) (DIFFERENT B61 B62 B63 B64 B65 B66 B67 B68 B69) (DIFFERENT B71 B72 B73 B74 B75 B76 B77 B78 B79) (DIFFERENT B81 B82 B83 B84 B85 B86 B87 B88 B89) (DIFFERENT B91 B92 B93 B94 B95 B96 B97 B98 B99) (DIFFERENT B11 B21 B31 B41 B51 B61 B71 B81 B91) (DIFFERENT B12 B22 B32 B42 B52 B62 B72 B82 B92) (DIFFERENT B13 B23 B33 B43 B53 B63 B73 B83 B93) (DIFFERENT B14 B24 B34 B44 B54 B64 B74 B84 B94) (DIFFERENT B15 B25 B35 B45 B55 B65 B75 B85 B95) (DIFFERENT B16 B26 B36 B46 B56 B66 B76 B86 B96) (DIFFERENT B17 B27 B37 B47 B57 B67 B77 B87 B97) (DIFFERENT B18 B28 B38 B48 B58 B68 B78 B88 B98) (DIFFERENT B19 B29 B39 B49 B59 B69 B79 B89 B99) (DIFFERENT B11 B12 B13 B21 B22 B23 B31 B32 B33) (DIFFERENT B14 B15 B16 B24 B25 B26 B34 B35 B36) (DIFFERENT B17 B18 B19 B27 B28 B29 B37 B38 B39) (DIFFERENT B41 B42 B43 B51 B52 B53 B61 B62 B63) (DIFFERENT B44 B45 B46 B54 B55 B56 B64 B65 B66) (DIFFERENT B47 B48 B49 B57 B58 B59 B67 B68 B69) (DIFFERENT B71 B72 B73 B81 B82 B83 B91 B92 B93) (DIFFERENT B74 B75 B76 B84 B85 B86 B94 B95 B96) (DIFFERENT B77 B78 B79 B87 B88 B89 B97 B98 B99) ; Enter the constraints for your specific Sudoku problem here (= B12 2) (= B24 6) (= B29 3) (= B32 7) (= B33 4) (= B35 8) (= B46 3) (= B49 2) (= B52 8) (= B55 4) (= B58 1) (= B61 6) (= B64 5) (= B75 1) (= B77 7) (= B78 8) (= B81 5) (= B86 9) (= B98 4) )