fpu_types: THEORY
BEGIN

	IMPORTING bitvectors@top

	exception_t: TYPE = [# OVF,UNF,INX,DIVZ,INV, UNIMPL: bool #];

	fpu_inp_t: TYPE = [# F1,F2: bvec[64], %% The operands; single operands
										  %% are encoded in the bits 61..32
			             RM: bvec[2],     %% Rounding-mode; encoded as in MP00
						 mask: bvec[6],	  %% The mask bits of the above exceptions
 			             op: bvec[9] #];  %% The op-code as in MP00

	fpu_out_t: TYPE = [# result: bvec[64], %% The result; single operands
										   %% are encoded in the bits 61..32
						 exceptions: exception_t,   %% the exceptions that
													%% occured during execution
						 double: bool #];  %% is result dbl-format?

END fpu_types