d "move.l accext01, d0" ab80 0x0 (seq (set src (var accext01)) (set d0 (cast 32 false (var src))))
d "maaac.w d1l, d0l, acc0, acc1" a0010005 0x0 (seq (set src0 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d1) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d1))) (cast 16 false (var d1))) (cast 32 false (cast 16 false (var d1)))))) (set src1 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d0) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 false (cast 16 false (var d0)))))) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (var prod_wide)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "masac.w d2l, d0l, acc0, acc1" a0020007 0x0 (seq (set src0 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d2) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d2))) (cast 16 false (var d2))) (cast 32 false (cast 16 false (var d2)))))) (set src1 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d0) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 false (cast 16 false (var d0)))))) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (var prod_wide)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "msaac.l d2, d3, acc0, acc1" a6020905 0x0 (seq (set src0 (var d2)) (set src1 (var d3)) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (var prod_wide)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "mssac.l d2, d3, acc2, acc3" a602091f 0x0 (seq (set src0 (var d2)) (set src1 (var d3)) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (var prod_wide)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc2)) (set acc_ext (cast 16 false (var accext23))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc2 (cast 32 false (var res))) (set accext23 (cast 32 false (| (& (var accext23) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc3)) (set acc_ext (cast 16 false (>> (var accext23) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc3 (cast 32 false (var res))) (set accext23 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext23) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x800))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x400) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x800) (bv 32 0x0)))))
d "maaac.w d1l, d0l, <<, acc0, acc1" a0010205 0x0 (seq (set src0 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d1) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d1))) (cast 16 false (var d1))) (cast 32 false (cast 16 false (var d1)))))) (set src1 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d0) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 false (cast 16 false (var d0)))))) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (<< (var prod_wide) (bv 8 0x1) false)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "masac.w d2l, d0l, >>, acc0, acc1" a0020407 0x0 (seq (set src0 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d2) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d2))) (cast 16 false (var d2))) (cast 32 false (cast 16 false (var d2)))))) (set src1 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (<< (var d0) (bv 8 0x10) false) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 32 (msb (cast 16 false (var d0))) (cast 16 false (var d0))) (cast 32 false (cast 16 false (var d0)))))) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (>> (var prod_wide) (bv 8 0x1) (msb (var prod_wide))) (>> (var prod_wide) (bv 8 0x1) false))) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "msaac.l d2, d3, <<, acc0, acc1" a6020b05 0x0 (seq (set src0 (var d2)) (set src1 (var d3)) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (<< (var prod_wide) (bv 8 0x1) false)) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc0)) (set acc_ext (cast 16 false (var accext01))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc0 (cast 32 false (var res))) (set accext01 (cast 32 false (| (& (var accext01) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc1)) (set acc_ext (cast 16 false (>> (var accext01) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (+ (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (+ (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc1 (cast 32 false (var res))) (set accext01 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext01) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x200))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x100) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x200) (bv 32 0x0)))))
d "mssac.l d2, d3, >>, acc2, acc3" a6020d1f 0x0 (seq (set src0 (var d2)) (set src1 (var d3)) (set prod_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (* (cast 80 (msb (var src0)) (var src0)) (cast 80 (msb (var src1)) (var src1))) (* (cast 80 false (var src0)) (cast 80 false (var src1))))) (set prod_scaled (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (>> (var prod_wide) (bv 8 0x1) (msb (var prod_wide))) (>> (var prod_wide) (bv 8 0x1) false))) (set prod (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 64 (msb (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (cast 40 false (+ (>> (var prod_wide) (bv 8 0x18) false) (ite (&& (! (is_zero (& (var macsr) (bv 32 0x10)))) (|| (! (ule (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000))) (&& (== (& (var prod_wide) (bv 80 0xffffff)) (bv 80 0x800000)) (! (is_zero (& (>> (var prod_wide) (bv 8 0x18) false) (bv 80 0x1))))))) (bv 80 0x1) (bv 80 0x0))))) (ite (is_zero (& (var macsr) (bv 32 0x40))) (cast 64 (msb (cast 40 false (var prod_scaled))) (cast 40 false (var prod_scaled))) (cast 64 false (cast 40 false (var prod_scaled)))))) (set prod_overflow (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (bv 32 0x0) (ite (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (cast 40 (msb (var prod_scaled)) (var prod_scaled))) (var prod_scaled))) (! (is_zero (>> (var prod_scaled) (bv 8 0x28) false)))) (bv 32 0x1) (bv 32 0x0)))) (set acc_word (var acc2)) (set acc_ext (cast 16 false (var accext23))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc2 (cast 32 false (var res))) (set accext23 (cast 32 false (| (& (var accext23) (bv 32 0xffff0000)) (cast 32 false (var ext16))))) (set ov_first (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_first (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set acc_word (var acc3)) (set acc_ext (cast 16 false (>> (var accext23) (bv 8 0x10) false))) (set acc_full (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 48 false (>> (var acc_ext) (bv 8 0x8) false)) (bv 8 0x28) false) (| (<< (cast 48 false (var acc_word)) (bv 8 0x8) false) (cast 48 false (& (var acc_ext) (bv 16 0xff))))) (| (<< (cast 48 false (var acc_ext)) (bv 8 0x20) false) (cast 48 false (var acc_word))))) (set acc (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (cast 64 (msb (var acc_full)) (var acc_full)) (cast 64 false (var acc_full)))) (set res_wide (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (- (cast 80 (msb (var acc)) (var acc)) (cast 80 (msb (var prod)) (var prod))) (- (cast 80 false (var acc)) (cast 80 false (var prod))))) (set res_full (cast 48 false (var res_wide))) (set res (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (cast 32 false (>> (var res_full) (bv 8 0x8) false)) (cast 32 false (var res_full)))) (set ext16 (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (| (<< (cast 16 false (>> (var res_full) (bv 8 0x28) false)) (bv 8 0x8) false) (cast 16 false (& (var res_full) (bv 48 0xff)))) (cast 16 false (>> (var res_full) (bv 8 0x20) false)))) (set acc3 (cast 32 false (var res))) (set accext23 (cast 32 false (| (<< (cast 32 false (var ext16)) (bv 8 0x10) false) (& (var accext23) (bv 32 0xffff))))) (set ov_second (ite (|| (! (is_zero (var prod_overflow))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 48 (msb (var res_wide)) (var res_wide))) (cast 48 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x30) false))))) (bv 32 0x1) (bv 32 0x0))) (set ev_second (ite (ite (! (is_zero (& (var macsr) (bv 32 0x20)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 40 (msb (var res_wide)) (var res_wide))) (cast 40 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x28) false)))) (ite (|| (! (is_zero (& (var macsr) (bv 32 0x20)))) (is_zero (& (var macsr) (bv 32 0x40)))) (! (== (cast 80 (msb (cast 32 (msb (var res_wide)) (var res_wide))) (cast 32 (msb (var res_wide)) (var res_wide))) (var res_wide))) (! (is_zero (>> (var res_wide) (bv 8 0x20) false))))) (bv 32 0x1) (bv 32 0x0))) (set macsr (| (| (| (| (| (| (& (var macsr) (bv 32 0xfffffff0)) (ite (msb (var res_full)) (bv 32 0x8) (bv 32 0x0))) (ite (is_zero (var res_full)) (bv 32 0x4) (bv 32 0x0))) (ite (|| (! (is_zero (var ov_second))) (! (is_zero (& (var macsr) (bv 32 0x800))))) (bv 32 0x2) (bv 32 0x0))) (ite (! (is_zero (var ev_second))) (bv 32 0x1) (bv 32 0x0))) (ite (! (is_zero (var ov_first))) (bv 32 0x400) (bv 32 0x0))) (ite (! (is_zero (var ov_second))) (bv 32 0x800) (bv 32 0x0)))))
