fpm_def: THEORY
BEGIN

	IMPORTING tag, fpu_import_misc

	fpm_unp(I: fpu_inp_t): fpm_unp_out_t = fp_misc_unpack(I);
%	fpm_rd1(I: fpm_rd1in_t): fpm_rd2in_t = fpm_rd1(I); %% defined in fp_misc
%	fpm_rd2(I: fpm_rd2in_t): fpu_out_t = fpm_rd2(I);

	fpm_f(I: fpu_inp_t): fpu_out_t = fpm_comb(I);

	fpm_f_special: LEMMA FORALL (Din: fpu_inp_t): fpm_unp(Din)`special IMPLIES
					fpm_f(Din)=fpm_unp(Din)`spec_dout;

	fpm_f_nospecial: LEMMA FORALL (Din: fpu_inp_t): NOT fpm_unp(Din)`special IMPLIES
					fpm_f(Din)=fpm_rd2(fpm_rd1(fpm_unp(Din)`d_out));

	fpm_ctrl_t: TYPE+ = [#	
			unp_full: bool,
			unp_tag: tag_t,
			unp_special: bool,

			rd1_full: bool,
			rd1_tag: tag_t #];

	fpm_t: TYPE = [#
			d_unp: fpm_unp_out_t,
			d_rd1: fpm_rd2in_t,
			ctrl: fpm_ctrl_t #];

% sbeyer 30.01.2003:
% we do not fix an arbitrary initial state,
% but define a subtype for admissible initial states
% the correctness criteria then are quantified over initial states
% that are admissible
%
%	fpm_dontcare_state: fpm_t; %% this is left uninterpreted, and is
%						  %% implemented as don't cares in verilog
%
%	fpm_init: fpm_t = fpm_dontcare_state WITH [ `ctrl`unp_full:=FALSE, 
%								 `ctrl`rd1_full:=FALSE ];

	fpm_init_t: TYPE+ = (LAMBDA (x:fpm_t): NOT x`ctrl`unp_full AND NOT x`ctrl`rd1_full);

	fpm_init : VAR fpm_init_t;

	fpm_init_c: LEMMA NOT (fpm_init`ctrl`unp_full  OR fpm_init`ctrl`rd1_full);
	
	c: VAR fpm_ctrl_t;

	fpm_outsel(c): bool = NOT c`rd1_full AND c`unp_full AND c`unp_special;
	fpm_valout(stallin: bool, c): bool = NOT stallin AND (fpm_outsel(c) OR c`rd1_full);
	fpm_tagout(c): tag_t = IF fpm_outsel(c) THEN c`unp_tag ELSE c`rd1_tag ENDIF;

	fpm_rd1ce(stallin: bool, c): bool = fpm_valout(stallin, c) OR NOT c`rd1_full;
	fpm_unpce(stallin: bool, c): bool = (fpm_rd1ce(stallin, c) AND NOT c`unp_special) OR
										(fpm_outsel(c) AND fpm_valout(stallin, c)) OR
										NOT c`unp_full;

	fpm_ctrl_nxt(valin, stallin, specin: bool, tagin: tag_t, c): fpm_ctrl_t =
			LET unpce=fpm_unpce(stallin, c),
				rd1ce=fpm_rd1ce(stallin, c)
			IN (#
				unp_full	:= IF unpce THEN valin ELSE c`unp_full ENDIF,
				unp_tag		:= IF unpce THEN tagin ELSE c`unp_tag ENDIF,
				unp_special := IF unpce THEN specin ELSE c`unp_special ENDIF,

				rd1_full	:= IF rd1ce THEN c`unp_full AND NOT c`unp_special ELSE c`rd1_full ENDIF,
				rd1_tag		:= IF rd1ce THEN c`unp_tag ELSE c`rd1_tag ENDIF #);

	fpm_nxt(clear: bool, data_in: fpu_inp_t, 
			valin, stallin: bool, tagin: tag_t, d: fpm_t): fpm_t = 
% sbeyer 30.01.2003:
% clean implementation of 'clear'
			IF clear THEN d WITH [`ctrl`unp_full := FALSE,`ctrl`rd1_full:=FALSE] ELSE
			LET unp=fpm_unp(data_in),
				specialin=unp`special,

				c=d`ctrl,
				nxt_c=fpm_ctrl_nxt(valin, stallin, specialin, tagin, c),

			    unpce=fpm_unpce(stallin, c),
				rd1ce=fpm_rd1ce(stallin, c) IN
			(#  d_unp	:= IF unpce THEN unp ELSE d`d_unp ENDIF,
				d_rd1	:= IF rd1ce THEN fpm_rd1(d`d_unp`d_out) ELSE d`d_rd1 ENDIF,
				ctrl	:= nxt_c #)
			ENDIF;

	%%%%%% These are the five parts which form the tom_circuit for verification
	%%%%%% and the actual hardware for synthetization


	TOMfpm_nxt_state(S: fpm_t, Din: fpu_inp_t, tag_in: tag_t, valin, stall_in, clear: bool):
		fpm_t = fpm_nxt(clear, Din, valin, stall_in, tag_in, S);

	TOMfpm_Dout(S: fpm_t, Din: fpu_inp_t, val_in, stall_in, clear: bool): fpu_out_t =
		IF fpm_outsel(S`ctrl) THEN S`d_unp`spec_dout ELSE fpm_rd2(S`d_rd1) ENDIF;

	TOMfpm_tag(S: fpm_t, tag_in: tag_t, val_in, stall_in, clear: bool): tag_t =
		fpm_tagout(S`ctrl);

	TOMfpm_valid(S: fpm_t, val_in, stall_in, clear: bool): bool =
		NOT clear AND fpm_valout(stall_in, S`ctrl);

	TOMfpm_stall(S: fpm_t, stall_in: bool): bool = NOT fpm_unpce(stall_in, S`ctrl);

END fpm_def