tom_circuit[stateT, tagT, Tin, Tout: TYPE+, initial_state: stateT]: THEORY BEGIN IMPORTING tom_circuit_types[stateT,tagT,Tin,Tout]; C: VAR tom_circuit_t; %%% Circuit is: VAR tom_inp_seq_t; %%% Input Sequence t, tmax: VAR nat; tg: VAR tagT; %%%%%%%%% Dies ist die Spezifikation %%% trans_iterate computes the content of the state register %%% during cycle t tom_trans_iterate(t, is, C): RECURSIVE stateT = IF t = 0 THEN initial_state ELSE C`nxt_state (tom_trans_iterate(t - 1, is, C), is(t - 1)`D, is(t - 1)`tag, is(t - 1)`valid, is(t - 1)`stall, FALSE) %%%% CLEAR ist immer FALSE ENDIF MEASURE t; %%% The combinatorial outputs during cycle t Dout(t, is, C): Tout = C`D(tom_trans_iterate(t, is, C), is(t)`D, is(t)`valid, is(t)`stall, FALSE); tag_out(t, is, C): tagT = C`tag(tom_trans_iterate(t, is, C), is(t)`tag, is(t)`valid, is(t)`stall, FALSE); val_out(t, is, C): bool = C`valid(tom_trans_iterate(t, is, C), is(t)`valid, is(t)`stall, FALSE); stall_out(t, is, C): bool = C`stall(tom_trans_iterate(t, is, C), is(t)`stall); %%% Praedikate ueber Input <-> StateTrans stalli_no_valo(is, C): bool = %%% G stall_in -> /val_out FORALL t: stall_in(t,is) IMPLIES NOT val_out(t, is, C); stallo_no_vali(is, C): bool = %%% G stall_out -> /val_in FORALL t: stall_out(t, is, C) IMPLIES NOT val_in(t, is); stallo_fintrue(is, C): bool = %%% G F /stall_out finite_true(LAMBDA t: stall_out(t, is, C)); %%% A tag gets busy, if it is scheduled, i.e. if val_in & tag_in=tg tag_schedule(t, is, tg): bool = val_in(t, is) AND tag_in(t, is)=tg; %%% A tag is returned, if val_out & tag_out=tg tag_return(t, is, C, tg): bool = val_out(t, is, C) AND tag_out(t, is, C)=tg; %%% A tag is in use, if it was scheduled and not yet released tag_inuse(tP:nat, is, C, tg): bool = EXISTS (t: below(tP)): tag_schedule(t, is, tg) AND FORALL(tPP: subrange(t, tP-1)): NOT tag_return(tPP, is, C, tg); %%% G val_in & tg=tag_in -> %%% [(clear | val_out & tag_out=tg) R /(val_in & tag_in=tg)] %%% (FOCTL) tag_unique(is, C): bool = FORALL t: LET tg = tag_in(t, is) IN tag_schedule(t, is, tg) IMPLIES (FORALL (tP: above(t)): (NOT tag_schedule(tP, is, tg) OR (EXISTS (tPP: subrange(t, tP - 1)): tag_return(tPP, is, C, tg)))); %%% Wird benoetigt fuer beschraenkte Induktionen tag_unique_until(is, C, tmax): bool = FORALL t: LET tg = tag_in(t, is) IN tag_schedule(t, is, tg) IMPLIES (FORALL (tP: subrange(t+1, tmax)): (NOT tag_schedule(tP, is, tg) OR (EXISTS (tPP: subrange(t, tP - 1)): tag_return(tPP, is, C, tg)))); tag_unique_rewr: LEMMA tag_unique(is, C) IFF FORALL t: tag_schedule(t, is, tag_in(t, is)) IMPLIES NOT tag_inuse(t, is, C, tag_in(t, is)); %%% G val_in & tg=tag_in -> %%% F (clear | val_out & tg=tag_out) liveness(is, C): bool = FORALL t: LET tg = tag_in(t, is) IN tag_schedule(t, is, tg) IMPLIES (EXISTS (tP: upfrom(t)): tag_return(tP, is, C, tg)); consistency(is, C): bool = FORALL (tP: nat): LET tg = tag_out(tP, is, C) IN tag_return(tP, is, C, tg) IMPLIES (EXISTS (t: upto(tP)): (tag_schedule(t, is, tg) AND (FORALL (tPP: subrange(t, tP - 1)): NOT tag_return(tPP, is, C, tg)))); consistency_until(is, C, tmax): bool = FORALL (tP: upto(tmax)): LET tg = tag_out(tP, is, C) IN tag_return(tP, is, C, tg) IMPLIES (EXISTS (t: upto(tP)): (tag_schedule(t, is, tg) AND (FORALL (tPP: subrange(t, tP - 1)): NOT tag_return(tPP, is, C, tg)))); consistency_rewr: LEMMA tag_unique(is,C) IMPLIES (consistency(is, C) IFF (FORALL t: LET tg=tag_out(t, is, C) IN tag_return(t, is, C, tg) IMPLIES %% either it was scheduled previously, or it is a combinatorial return (tag_inuse(t, is, C, tg) OR tag_schedule(t, is, tg)))); tom_circuit_ok(C): bool = FORALL (is): (stallo_no_vali(is, C) IMPLIES (stalli_no_valo(is, C) AND (stalli_fintrue(is) IMPLIES stallo_fintrue(is, C) AND liveness(is, C) AND (FORALL tmax: tag_unique_until(is, C, tmax) IMPLIES consistency_until(is, C, tmax))))); END tom_circuit f_circuit[stateT, tagT, Tin, Tout: TYPE+, initial_state: stateT, f: [Tin -> Tout]]: THEORY BEGIN IMPORTING tom_circuit[stateT, tagT, Tin, Tout, initial_state] C: VAR tom_circuit_t; %%% Circuit is: VAR tom_inp_seq_t; %%% Input Sequence t,tmax: VAR nat; strong_consistency(is, C): bool = FORALL (tP: nat): LET tg = tag_out(tP, is, C) IN tag_return(tP, is, C, tg) IMPLIES (EXISTS (t: upto(tP)): (tag_schedule(t, is, tg) AND Dout(tP, is, C) = f(Din(t, is)) AND (FORALL (tPP: subrange(t, tP - 1)): NOT tag_return(tPP, is, C, tg)))); strong_consistency_until(is, C, tmax): bool = FORALL (tP: upto(tmax)): LET tg = tag_out(tP, is, C) IN tag_return(tP, is, C, tg) IMPLIES (EXISTS (t: upto(tP)): (tag_schedule(t, is, tg) AND Dout(tP, is, C)=f(Din(t, is)) AND (FORALL (tPP: subrange(t, tP - 1)): NOT tag_return(tPP, is, C, tg)))); strong_liveness(is, C): bool = FORALL t: LET tg = tag_in(t, is) IN tag_schedule(t, is, tg) IMPLIES (EXISTS (tP: upfrom(t)): tag_return(tP, is, C, tg) AND Dout(tP, is ,C)=f(Din(t, is))); strong_live_is_live: LEMMA strong_liveness(is, C) IMPLIES liveness(is, C); strong_live_cons: LEMMA (FORALL is: consistency(is, C) AND strong_liveness(is, C)) IMPLIES FORALL is: strong_consistency(is, C); strong_live_cons2: LEMMA (FORALL is: stallo_no_vali(is, C) AND stalli_fintrue(is) IMPLIES (tag_unique(is, C) => consistency(is, C)) AND strong_liveness(is, C)) IMPLIES (FORALL is: stallo_no_vali(is, C) AND stalli_fintrue(is) IMPLIES (tag_unique(is, C) => strong_consistency(is, C))); cons_until_lem: LEMMA (FORALL is: stallo_no_vali(is, C) AND stalli_fintrue(is) IMPLIES (tag_unique(is, C) => strong_consistency(is, C))) IMPLIES (FORALL is: stallo_no_vali(is, C) AND stalli_fintrue(is) => FORALL tmax: tag_unique_until(is, C, tmax) => strong_consistency_until(is, C, tmax)) ; f_circuit_ok(C): bool = FORALL (is): (stallo_no_vali(is, C) IMPLIES (stalli_no_valo(is, C) AND (stalli_fintrue(is) IMPLIES stallo_fintrue(is, C) AND liveness(is, C) AND (FORALL tmax: tag_unique_until(is, C, tmax) IMPLIES strong_consistency_until(is, C, tmax))))); f_circuit_ok_rewr: LEMMA f_circuit_ok(C) WHEN FORALL is: (stallo_no_vali(is, C) IMPLIES (stalli_no_valo(is, C) AND (stalli_fintrue(is) IMPLIES stallo_fintrue(is, C) AND strong_liveness(is, C) AND (tag_unique(is, C) IMPLIES consistency(is, C))))); END f_circuit