fp_misc_unpack: THEORY
BEGIN

	IMPORTING fp_rd2int, fp_compare_impl

	fpm_rd1in_dontcare: fpm_rd1in_t;

	fpm_noexceptions: exception_t =
			 (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, UNIMPL:=FALSE, INV:=FALSE #);

    fpm_unp_out_t: TYPE = [# d_out: fpm_rd1in_t, spec_dout: fpu_out_t, special: bool #];

	fpm_double(op: bvec[9]): bool = is_dblNEG(op) OR is_dblABS(op) OR is_dblCMP(op) OR
									is_dblMOV(op) OR is_CVTd2s(op) OR is_CVTd2i(op);

	fp_misc_unpack(I: fpu_inp_t): fpm_unp_out_t =
		 LET U1=unpack_impl(fpm_double(I`op), FALSE, I`F1),
			 U2=unpack_impl(fpm_double(I`op), FALSE, I`F2),
	    	 SU1=spec_unpack_impl(U1`s, U1`einf, U1`ez, U1`fz, U1`h(51)),
	    	 SU2=spec_unpack_impl(U2`s, U2`einf, U2`ez, U2`fz, U2`h(51)) IN
		 
		 IF isNEG(I`op) THEN
			(# d_out := fpm_rd1in_dontcare,
			   spec_dout := (# result := fill[1](NOT I`F1(63)) o I`F1^(62,0),
							   exceptions := fpm_noexceptions,
							   double := is_dblNEG(I`op) #),
			   special := TRUE #)
         ELSE 
		 IF isABS(I`op) THEN
			(# d_out := fpm_rd1in_dontcare,
			   spec_dout := (# result := fill[1](FALSE) o I`F1^(62,0),
							   exceptions := fpm_noexceptions,
							   double := is_dblABS(I`op) #),
			   special := TRUE #)
         ELSE 
		 IF isMOV(I`op) THEN
			(# d_out := fpm_rd1in_dontcare,
			   spec_dout := (# result := I`F1,
							   exceptions := fpm_noexceptions,
							   double := is_dblMOV(I`op) #),
			   special := TRUE #)
		 ELSE
		 IF is_mf2i(I`op) OR is_mi2f(I`op) THEN
			(# d_out := fpm_rd1in_dontcare,
			   spec_dout := (# result := I`F1,
							   exceptions := fpm_noexceptions,
							   double := FALSE #),
			   special := TRUE #)
		 ELSE
		 IF isCMP(I`op) THEN
			(# d_out := fpm_rd1in_dontcare,
			   spec_dout := fp_compute_fcc(U1`s, U2`s, U1`e, U2`e, U1`f, U2`f,
						   		SU1`QNAN,SU2`QNAN, SU1`SNAN,SU2`SNAN, SU1`ZERO,SU2`ZERO, 
						   		SU1`pINF,SU2`pINF, SU1`nINF,SU2`nINF, I`op),
			   special := TRUE #)
		 ELSE 
		 IF is_CVTs2i(I`op) OR is_CVTd2i(I`op) THEN
			LET RNG=rd2int_range(U1`e, TRUE),
			    SML=rd2int_small_int_impl(U1`s, U1`e, U1`f, I`RM),
			    MED=rd2int_stg(U1`e, TRUE) IN
			(# d_out := (# rdinp := (# sr:=U1`s, er:=MED, 
									   fr:=fill[1](FALSE) o U1`f o fill[3](FALSE), 
								       RM:=I`RM, double:=TRUE, mask:=fill[6](FALSE) #),
						   origF := I`F1, cvtf2i := TRUE, cvtd2s := FALSE,
						   OVFen := OVFen(I`mask), UNFen := UNFen(I`mask) #),
			   spec_dout := (# result := SML o fill[32](FALSE),
							   exceptions := (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, 
									INV:=RNG`large OR SU1`INF OR SU1`QNAN OR SU1`SNAN, UNIMPL:=FALSE #),
							   double := FALSE #),
			   special := RNG`small OR RNG`large OR SU1`INF OR SU1`QNAN OR SU1`SNAN #)
		 ELSE
		 IF is_CVTi2s(I`op) OR is_CVTi2d(I`op) THEN
			LET INTU=fx_unpack(I`F1^(63,32)), ISZERO=zero_impl[32](I`F1^(63,32)) IN
			(# d_out := (# rdinp := (# sr:=INTU`s, er:=INTU`e, fr:=INTU`f,
									   RM:=I`RM, double:=is_CVTi2d(I`op), mask:=I`mask #),
						   origF := I`F1,  cvtf2i := FALSE, cvtd2s := FALSE,
						   OVFen := OVFen(I`mask), UNFen := UNFen(I`mask) #),
			   spec_dout := (# result := fill[64](FALSE),
							   exceptions := fpm_noexceptions,
							   double := FALSE #),
			   special := ISZERO #)
		 ELSE
		 IF is_CVTs2d(I`op) THEN
			(# d_out := (# rdinp := (# sr:=U1`s, er:=sext_impl[11,13](U1`e), 
									   fr:=fill[1](FALSE) o U1`f o fill[3](FALSE),
									   RM:=I`RM, double:=TRUE, mask:=I`mask #),
						   origF := I`F1, cvtf2i := FALSE, cvtd2s := FALSE, 
						   OVFen := OVFen(I`mask), UNFen := UNFen(I`mask) #),
			   spec_dout := (# result := IF SU1`SNAN THEN fill[64](TRUE) 
										 ELSE IF SU1`QNAN THEN 
											fill[1](I`F1(63)) o fill[11](TRUE) o 
											I`F1^(54,32) o fill[29](FALSE) % preserve sign,significant
										 ELSE IF SU1`ZERO THEN fill[1](I`F1(63)) o fill[63](FALSE)
										 ELSE fill[1](I`F1(63)) o fill[11](TRUE) o fill[52](FALSE) 
										 ENDIF ENDIF ENDIF,
							   exceptions := (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, 
												INV:=SU1`SNAN, UNIMPL:=FALSE  #),
							   double := TRUE #),
			   special := SU1`QNAN OR SU1`SNAN OR SU1`INF OR SU1`ZERO #)
		ELSE
		IF is_CVTd2s(I`op) THEN
			(# d_out := (# rdinp := (# sr:=U1`s, er:=sext_impl[11,13](U1`e), 
									   fr:=fill[1](FALSE) o U1`f o fill[3](FALSE),
									   RM:=I`RM, double:=FALSE, mask:=I`mask^(5,2) o fill[2](FALSE) #),
																%% OVFen/UNFen aus
						   origF := I`F1, cvtf2i := FALSE, cvtd2s := TRUE, 
						   OVFen := OVFen(I`mask), UNFen := UNFen(I`mask) #),
			   spec_dout := (# result := IF SU1`SNAN THEN fill[64](TRUE) 
										 ELSE IF SU1`QNAN THEN 
											fill[1](I`F1(63)) o fill[8](TRUE) o 
											I`F1^(51,30) o fill[33](TRUE)
										 %% the 1 in pos 32 is necessary to ensure f/=0 in the result QNAN
										 ELSE IF SU1`ZERO THEN fill[1](I`F1(63)) o fill[63](FALSE)
										 ELSE
											fill[1](I`F1(63)) o fill[8](TRUE) o fill[55](FALSE) 
										 ENDIF ENDIF ENDIF,
							   exceptions := 
								  (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, 
									 INV:=SU1`SNAN, UNIMPL:=FALSE #),
							   double := FALSE #),
			   special := SU1`QNAN OR SU1`SNAN OR SU1`INF OR SU1`ZERO  #)
% sbeyer 31.01.2003:
% ELSE is UNIMPL
		ELSE	(# d_out := fpm_rd1in_dontcare,
			   spec_dout := (# result := I`F1,
							   exceptions := (# OVF:=FALSE, UNF:=FALSE, INX:=FALSE, DIVZ:=FALSE, 
									 INV:=FALSE, UNIMPL:=TRUE #),
							   double := FALSE #),
			   special := TRUE #)
		ENDIF ENDIF ENDIF ENDIF ENDIF ENDIF ENDIF ENDIF ENDIF;
END fp_misc_unpack