:machine
((: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)))))
5