Library multi_sub_s_s_s_prg
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.
Require Import pick_sign_prg multi_add_s_s_u_prg multi_sub_s_s_u_prg copy_s_s_prg.
Local Open Scope mips_cmd_scope.
Import MachineInt.
Require Import mips_cmd.
Require Import pick_sign_prg multi_add_s_s_u_prg multi_sub_s_s_u_prg copy_s_s_prg.
Local Open Scope mips_cmd_scope.
z <- x - y with z, x, y signed
Definition multi_sub_s_s_s rk rz rx ry a0 a1 a2 a3 a4 a5 rX rY rZ :=
lw rY four16 ry ;
pick_sign ry a0 a1 ;
If_bgez a1 Then
If_beq a1 , r0 Then
copy_s_s rk rz rx a0 a1 a2 a3 a4 ;
addiu a3 r0 zero16
Else
multi_sub_s_s_u rk rz rx rY a0 a1 a2 a3 a4 a5 rX rZ
Else
multi_add_s_s_u rk rz rx rY a0 a1 a2 a3 a4 a5 rX rZ.
lw rY four16 ry ;
pick_sign ry a0 a1 ;
If_bgez a1 Then
If_beq a1 , r0 Then
copy_s_s rk rz rx a0 a1 a2 a3 a4 ;
addiu a3 r0 zero16
Else
multi_sub_s_s_u rk rz rx rY a0 a1 a2 a3 a4 a5 rX rZ
Else
multi_add_s_s_u rk rz rx rY a0 a1 a2 a3 a4 a5 rX rZ.