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
• Two Stage Pipelined Machine
• Decimal Counter

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 maj. The second element in the definition is the type. This is a list containing 1 positive integer for a bit vector function (maj, for example returns a 1-bit bit vector), 2 positive integers if the return type is a memory, and a list of 1 integer lists and 2 integer lists if there are multiple values returned. For example ((1) (8 4)) would specify that the function returns a 1-bit bit vector and a memory with 8 4-bit words.

The third part of a function definition is its arguments. This is just a list of variable definitions just like the ones in the :vars section. In the case of maj, the inputs are 3 1-bit bit vectors, a, b, and c. The final element of a function definition is the body. Its return type must be compatible with that of the function.

In our example, the maj function calculates the majority function on the inputs, fa is a full adder that returns the carry out bit and the sum bit, alu-slice is a 1-bit piece of the alu, and alu-2-bit is the 2-bit alu constructed out of the alu slices. The :vars section includes inputs i1 and i2, an output out, the negation bit (whether i2 should be negated in the case of addition), the operation code, the carry out bit, and the zero bit. The :init specifies that initial states must have an out of 0, a cout of 1, and a zero of 0. The transition relation sets the next values of cout, out, and zero according to the outputs of the alu-2-bit function. The :spec checks that zero is true if and only if cout is not.

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 :vars section: mastate, rf, and imem. The varaiable mastate represents most pieces of the state concatenated together, including the program counter. The register file is represented by rf and the instruction memory is imem. Now let's look at the functions.

((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 mastate. For example, getppc gets the program counter, which are in bits 0 to 1 of the mastate. The next 4 functions are used to decode an instruction. They take the instruction as input and produce the source and destination addresses and a control signal that indicates if the instruction should update the register file.

The nextspc and nextsrf show how to update the pc and rf for the ISA model. The step-isa function steps the ISA model. It takes the pc, register file, and instruction memory, and returns the new pc, register file, and instruction memory. Using the local construct, it sets the variable inst to be instruction at the address pointed to by the pc. The regwrite variable is set to the appropriate piece of the instruction. The two arguments are fetched from the rf according to the addresses given in the instruction. The result is just set to the sum of the two arguments (with the high bit chopped off). Finally, the new pc, new rf, and the imem are returned using mv.

The next 3 functions describe how the RTL model is stepped. The step-ma function takes in the mastate, rf, and imem, and returns the new values for each. Its behavior is similar to that of the step-isa function. It gets the pieces of the mastate, loads the appropriate instruction and input values and computes the new values for each piece of the state.

Finally, we have a function that is very similar to the step-ma function, called flush-ma. This function is used to flush an MA state by completing the partially executed instruction in the pipeline latch without fetching any new instruction. Finally, here is the formula we want to check:

(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 w1, s-rf, and s-imem to be the result of flushing the RTL machine in its initial state. Then s-pc is set to the pc out of w1. This gives us all the pieces of the ISA state -- s-pc, s-rf, and s-imem -- that correspond to the current RTL state. Next, u-pc, u-rf, and u-imem are declared to be the result of stepping the current ISA state.

We then step the original RTL machine and flush again, giving us v1, v1-rf, and v1-imem. We then check that the pc of v1 is equal to u-pc and that v1-rf is equal to u-rf.

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, which is a bit vector of size 8. Each decimal digit is represented using 4 bits. The lower four bits of x and the higher four bits of x represent the first and the second digit of the decimal counter, respectively.

((x 8)) 

The BAT functions used to model the circuit that increments the decimal counter is described next. The inc4 function increments a digit represented using a 4-bit bit-vector and returns two values that include the incremented digit and a carry bit. If the value of the input digit is less than 9, then inc4 returns an incremented digit and a carry bit with value 0. If the value of the input digit is not less than 9, then inc4 returns a digit with value 0 and a carry bit with value 1.

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

The inc_digit function takes a digit and a carry bit as input. If the carry bit has a value of 1, inc_digit returns an incremented digit and the carry obtained by incrementing the input digit using the inc4 function. If the value of the input carry bit is 0, then the input digit and input carry are returned.

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

The inc_digits function is used to increment the decimal counter. The inc_digits function takes the entire state of the decimal counter as input. The first digit is incremented using the inc_digit function and the carry generated is used to increment the second digit.

 
(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 function checks if each digit of the decimal counter is valid, i.e., if the value of each digit is less than 10.

(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 function, then these digits will remain valid after being incremented using the inc_digits functions.

(-> (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 gen_dec_counter can be used to generate the BAT model for a decimal counter with any number of digits. The number of digits is given as input to the gen_dec_counter function. The BAT decimal counter example was based on an ACL2 decimal counter example that we obtained from Erik Reeber and Warren Hunt. We would like to thank Erik and Warren for the ACL2 decimal counter example.

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