md_def: THEORY
BEGIN

	IMPORTING tag, fpu_import_md

	%%% This renaming is historical; we have verified the control
	%%% using uninterpreted functions with the names from below.

	md_unp(I: fpu_inp_t): md_unp_out_t = md_unpack(I);
	md_md1(I: md_md1in_t): md_md2in_t  = md_stg1(I);
	md_md2(I: md_md2in_t): [# md1: md_md1in_t, selfd: md_selfdin_t, rd: rd_rd1in_t #] = md_stg2(I);
	md_selfd(I: md_selfdin_t): rd_rd1in_t = selfd_stg(I);
	md_rd1(I: rd_rd1in_t): rd_rd2in_t = rd_stg1(I);
	md_rd2(I: rd_rd2in_t): fpu_out_t = rd_stg2(I)`out;

	md_f(I: fpu_inp_t): fpu_out_t = md_comb(I);

	md_Din2Ctrl(Din: fpu_inp_t): [# muldiv_in, double_in: bool #] =
			(# muldiv_in := isDIV(Din`op),  double_in := is_double(Din`op) #);


	md_f_special: LEMMA FORALL (Din: fpu_inp_t): md_unp(Din)`special => md_f(Din)=md_unp(Din)`spec_dout;
	md_f_mul: LEMMA
	   FORALL (Din: fpu_inp_t):
	     NOT md_unp(Din)`special AND NOT md_Din2Ctrl(Din)`muldiv_in =>
    	  md_f(Din) = md_rd2(md_rd1(md_md2(md_md1(md_unp(Din)`d_out))`rd));
	md_f_divsgl: LEMMA
	   FORALL (Din: fpu_inp_t):
	     NOT md_unp(Din)`special AND  md_Din2Ctrl(Din)`muldiv_in AND NOT md_Din2Ctrl(Din)`double_in =>
		  LET D=md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(md_md1(
					md_unp(Din)`d_out))`md1))`md1))`md1))`md1))`md1) IN 
    	  md_f(Din) = md_rd2(md_rd1(md_selfd(md_md2(D)`selfd)));

	md_f_divdbl: LEMMA
	   FORALL (Din: fpu_inp_t):
	     NOT md_unp(Din)`special AND  md_Din2Ctrl(Din)`muldiv_in AND md_Din2Ctrl(Din)`double_in =>
		  LET D=md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(md_md1(md_md2(
					md_md1(md_md2(md_md1(md_md2(md_md1(md_unp(Din)`d_out))`md1))`md1))
					`md1))`md1))`md1))`md1))`md1) IN 
    	  md_f(Din) = md_rd2(md_rd1(md_selfd(md_md2(D)`selfd)));



%	  md_state_t: TYPE = bvec[4];
%	  Sselfd: md_state_t = fill[2](FALSE) o fill[2](FALSE);                
%	  SdivEb: md_state_t = fill[2](FALSE) o fill[1](FALSE) o fill[1](TRUE);
%	  SdivE : md_state_t = fill[2](FALSE) o fill[1](TRUE) o fill[1](FALSE);
%	  Sdiv00: md_state_t = fill[2](FALSE) o fill[2](TRUE);                
%	  Sdiv01: md_state_t = fill[1](FALSE) o fill[1](TRUE) o fill[2](FALSE);                
%	  Sdiv10: md_state_t = fill[1](FALSE) o fill[1](TRUE) o fill[1](FALSE) o fill[1](TRUE);
%	  Sdiv11: md_state_t = fill[1](FALSE) o fill[1](TRUE) o fill[1](TRUE) o fill[1](FALSE);
%	  Sdiv20: md_state_t = fill[1](FALSE) o fill[3](TRUE);                
%	  Sdiv21: md_state_t = fill[1](TRUE) o fill[3](FALSE);
%	  Smul  : md_state_t = fill[1](TRUE) o fill[2](FALSE) o fill[1](TRUE);
%	  Sspecial: md_state_t = fill[1](TRUE) o fill[1](FALSE) o fill[1](TRUE) o fill[1](FALSE);
%
%
%	 bveq4(a,b: bvec[4]): bool =(NOT a(0) XOR b(0)) AND
%							 (NOT a(1) XOR b(1)) AND
%							 (NOT a(2) XOR b(2)) AND
%							 (NOT a(3) XOR b(3));
%
%
%	 md_nxtstate(t: md_state_t): md_state_t =
%	   COND t = Sselfd -> Sselfd,
%			t = SdivEb -> Sselfd,
%			t = SdivE -> SdivEb,
%			t = Sdiv00 -> SdivE,
%			t = Sdiv01 -> Sdiv00,
%			t = Sdiv10 -> Sdiv01,
%			t = Sdiv11 -> Sdiv10,
%			t = Sdiv20 -> Sdiv11,
%			t = Sdiv21 -> Sdiv20,
%			t = Smul -> Smul,
%			ELSE -> Smul  % Sspecial -> Smul
%	   ENDCOND
%

%	md_state_t: TYPE = 
%		 {Sselfd, SdivEb, SdivE, Sdiv00, Sdiv01, Sdiv10, Sdiv11, Sdiv20, Sdiv21, Smul,
%		  Sspecial}
%
%	bveq4(t1,t2: md_state_t): bool = t1=t2


	md_ctrl_t: TYPE+ = [# 
			unp_full: bool,
			unp_tag: tag_t,
			unp_state: md_state_t,

			md1_full: bool,
			md1_tag: tag_t,
			md1_state: md_state_t,
			
			md2_full: bool,
			md2_tag: tag_t,
			md2_state: md_state_t,
	
			selfd_full: bool,
			selfd_tag: tag_t,
			
			rd1_full: bool,
			rd1_tag: tag_t #];


	md_t: TYPE = [#
			d_unp: md_unp_out_t,
			d_md1: md_md2in_t,
			d_md2: [# md1: md_md1in_t, selfd: md_selfdin_t, rd: rd_rd1in_t #],
			d_selfd: rd_rd1in_t,
			d_rd1: rd_rd2in_t,
			ctrl: md_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
%
%	md_dontcare_state: md_t; %% this is left uninterpreted, and is
%						  %% implemented as don't cares in verilog
%
%	md_init: md_t = md_dontcare_state WITH [ `ctrl`unp_full:=FALSE, 
%								 `ctrl`md1_full:=FALSE, 
%								 `ctrl`md2_full:=FALSE, 
%								 `ctrl`selfd_full:=FALSE, 
%								 `ctrl`rd1_full:=FALSE ];

	md_init_t: TYPE+ = (LAMBDA (x:md_t): NOT x`ctrl`unp_full AND 
					     NOT x`ctrl`md1_full AND
					     NOT x`ctrl`md2_full AND
					     NOT x`ctrl`selfd_full AND
					     NOT x`ctrl`rd1_full);

	md_init: VAR md_init_t;

	md_init_c: LEMMA LET c=md_init`ctrl IN NOT (c`unp_full OR c`md1_full OR c`md2_full OR c`selfd_full OR c`rd1_full);


	c: VAR md_ctrl_t;


	md_outsel(c): bool = NOT c`rd1_full AND c`unp_full AND bveq4(c`unp_state, Sspecial);
	md_valout(stallin: bool, c): bool = NOT stallin AND (md_outsel(c) OR c`rd1_full);
	md_md1sel(c): bool = c`md2_full AND NOT (bveq4(c`md2_state, Smul) OR bveq4(c`md2_state, Sselfd));

	md_tagout(c): tag_t = IF md_outsel(c) THEN c`unp_tag ELSE c`rd1_tag ENDIF;

	md_rd1ce(stallin: bool, c): bool = md_valout(stallin, c) OR NOT c`rd1_full;
	md_selfdce(stallin: bool, c): bool = md_rd1ce(stallin, c) OR NOT c`selfd_full;
	md_md2ce(stallin: bool, c): bool = 
			(bveq4(c`md2_state, Smul) AND md_rd1ce(stallin, c) AND NOT c`selfd_full) OR
			(bveq4(c`md2_state, Sselfd) AND md_selfdce(stallin, c)) OR
			NOT (bveq4(c`md2_state, Smul) OR bveq4(c`md2_state, Sselfd)) OR 
			NOT c`md2_full;
	md_md1ce(stallin: bool, c): bool = md_md2ce(stallin, c) OR NOT c`md1_full;
	md_unpce(stallin: bool, c): bool = 
			(md_md1ce(stallin, c) AND NOT md_md1sel(c) AND NOT bveq4(c`unp_state, Sspecial)) OR
			(md_valout(stallin, c) AND md_outsel(c)) OR
			NOT c`unp_full;

	md_ctrl_nxt(valin, muldiv_in, double_in, stallin, specin: bool, tagin: tag_t, c): md_ctrl_t =
			LET unpce=md_unpce(stallin, c),
				md1ce=md_md1ce(stallin, c),
				md2ce=md_md2ce(stallin, c),
				selfdce=md_selfdce(stallin, c),
				rd1ce=md_rd1ce(stallin, c),
				md1sel=md_md1sel(c),
				nxtstate=md_nxtstate(c`md1_state)
			IN

			(# unp_full   := IF unpce THEN valin ELSE c`unp_full ENDIF,
		  	   unp_tag    := IF unpce THEN tagin ELSE c`unp_tag ENDIF,
			   unp_state  := IF NOT unpce THEN c`unp_state ELSE
							 IF specin THEN Sspecial ELSE
							 IF NOT muldiv_in THEN Smul ELSE
							 IF double_in THEN Sdiv21 ELSE Sdiv11 
							 ENDIF ENDIF ENDIF ENDIF,

			   md1_full   := IF md1ce THEN md1sel OR c`unp_full AND NOT bveq4(c`unp_state, Sspecial)
								 ELSE c`md1_full ENDIF,
			   md1_tag    := COND
						md1ce AND md1sel -> c`md2_tag,
						md1ce AND NOT md1sel -> c`unp_tag,
						NOT md1ce -> c`md1_tag
					ENDCOND,
			   md1_state  := COND
						md1ce AND md1sel -> c`md2_state,
						md1ce AND NOT md1sel -> c`unp_state,
						NOT md1ce -> c`md1_state
					ENDCOND,

			   md2_full   := IF md2ce THEN c`md1_full ELSE c`md2_full ENDIF,
			   md2_tag	  := IF md2ce THEN c`md1_tag ELSE c`md2_tag ENDIF,
			   md2_state  := IF md2ce THEN nxtstate ELSE c`md2_state ENDIF,

			   selfd_full := IF selfdce THEN c`md2_full AND bveq4(c`md2_state, Sselfd)
								ELSE c`selfd_full ENDIF,
			   selfd_tag	  := IF selfdce THEN c`md2_tag ELSE c`selfd_tag ENDIF,

			   rd1_full   := IF rd1ce THEN c`selfd_full OR c`md2_full AND bveq4(c`md2_state, Smul)
								ELSE c`rd1_full ENDIF,
			   rd1_tag    := COND
								rd1ce AND c`selfd_full -> c`selfd_tag,
								rd1ce AND NOT c`selfd_full -> c`md2_tag,
								NOT rd1ce -> c`rd1_tag
							  ENDCOND #);

	 md_nxt(clear: bool, data_in: fpu_inp_t, 
			valin, muldiv_in, double_in, stallin: bool, tagin: tag_t, d: md_t): md_t =

		  IF clear THEN 
% sbeyer 30.01.2003:
% clean implementation of 'clear'
			d WITH [ `ctrl`unp_full:=FALSE, 
				 `ctrl`md1_full:=FALSE, 
				 `ctrl`md2_full:=FALSE, 
				 `ctrl`selfd_full:=FALSE, 
				 `ctrl`rd1_full:=FALSE ]
		  ELSE
			 LET unp=md_unp(data_in),
				 specialin=unp`special,

				 c=d`ctrl,
				 nxt_c=md_ctrl_nxt(valin, muldiv_in, double_in, stallin, specialin, tagin, c),

				 unpce=md_unpce(stallin, c),
				 md1ce=md_md1ce(stallin, c),
				 md2ce=md_md2ce(stallin, c),
				 selfdce=md_selfdce(stallin, c),
				 rd1ce=md_rd1ce(stallin, c),
				 md1sel=md_md1sel(c) IN

			 (# d_unp   := IF unpce THEN unp ELSE d`d_unp ENDIF,
				d_md1   := IF not md1ce THEN d`d_md1 ELSE
							md_md1(IF md1sel THEN d`d_md2`md1 ELSE d`d_unp`d_out ENDIF)
						   ENDIF,
				d_md2	:= IF md2ce THEN md_md2(d`d_md1) ELSE d`d_md2 ENDIF,
				d_selfd := IF selfdce THEN md_selfd(d`d_md2`selfd) ELSE d`d_selfd ENDIF,
				d_rd1   := IF NOT rd1ce THEN d`d_rd1 ELSE
							md_rd1(IF c`selfd_full THEN d`d_selfd ELSE d`d_md2`rd ENDIF)
						   ENDIF,
				ctrl	:= nxt_c #)
			ENDIF;



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

	TOMmd_nxt_state(S: md_t, Din: fpu_inp_t, tag_in: tag_t, val_in, stall_in, clear: bool):
		 md_t =
		     LET C = md_Din2Ctrl(Din) IN
		       md_nxt(clear, Din, val_in, C`muldiv_in, C`double_in, stall_in, tag_in, S);

	TOMmd_Dout(S: md_t, Din: fpu_inp_t, val_in, stall_in, clear: bool): fpu_out_t =
		IF md_outsel(S`ctrl) THEN S`d_unp`spec_dout ELSE md_rd2(S`d_rd1) ENDIF;

	TOMmd_tag(S: md_t, tag_in: tag_t, val_in, stall_in, clear: bool): tag_t =
		md_tagout(S`ctrl);

	TOMmd_valid(S: md_t, val_in, stall_in, clear: bool): bool =
		NOT clear AND md_valout(stall_in, S`ctrl);

	TOMmd_stall(S: md_t, stall_in: bool): bool = NOT md_unpce(stall_in, S`ctrl);

end md_def