Library multi_sub_s_s_prg
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.
Require Import pick_sign_prg multi_add_s_u_prg multi_sub_s_u_prg.
Local Open Scope mips_cmd_scope.
Section multi_sub_s_s_sect.
Variables rk rx ry a0 a1 a2 a3 a4 a5 rX rY : reg.
Import MachineInt.
Require Import mips_cmd.
Require Import pick_sign_prg multi_add_s_u_prg multi_sub_s_u_prg.
Local Open Scope mips_cmd_scope.
Section multi_sub_s_s_sect.
Variables rk rx ry a0 a1 a2 a3 a4 a5 rX rY : reg.
x <- x - y with x and y signed, expect x and y to be rk words long
Definition multi_sub_s_s :=
lw rY four16 ry ;
pick_sign ry a0 a1 ;
If_bgez a1 Then
If_beq a1 , r0 Then
addiu a3 r0 zero16
Else
multi_sub_s_u rk rx rY a0 a1 a2 a3 a4 a5 rX
Else
multi_add_s_u rk rx rY a0 a1 a2 a3 a4 a5 rX.
End multi_sub_s_s_sect.
lw rY four16 ry ;
pick_sign ry a0 a1 ;
If_bgez a1 Then
If_beq a1 , r0 Then
addiu a3 r0 zero16
Else
multi_sub_s_u rk rx rY a0 a1 a2 a3 a4 a5 rX
Else
multi_add_s_u rk rx rY a0 a1 a2 a3 a4 a5 rX.
End multi_sub_s_s_sect.