## 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)