1 2%----------------------------------------------------------------------------% 3% Specification of a register with a reset line. % 4%----------------------------------------------------------------------------% 5 6new_theory `RESET_REG`;; 7 8let RESET_REG = 9 new_definition 10 (`RESET_REG`, 11 "RESET_REG(reset,in,out) = 12 !t. out(t+1) = (reset(t+1) => T | in t)");; 13 14%----------------------------------------------------------------------------% 15% Note that the above specification is only partial; it doesn't specify the % 16% output at time 0. % 17%----------------------------------------------------------------------------% 18 19%----------------------------------------------------------------------------% 20% An implementation of the restable register using non-resetable registers % 21% that power-up storing F. % 22% % 23% reset in % 24% | | % 25% | *-----* *-----* % 26% | | ONE | | REG | % 27% | *-----* *-----* % 28% | | | % 29% | |l1 |l2 % 30% | | | % 31% *-------------------------* % 32% | MUX | % 33% *-------------------------* % 34% | % 35% out % 36% % 37% ONE, MUX and REG are as used in the PARITY example % 38% (hol/examples/PARITY.ml). % 39%----------------------------------------------------------------------------% 40 41new_parent `PARITY`;; 42 43let RESET_REG_IMP = 44 new_definition 45 (`RESET_REG_IMP`, 46 "RESET_REG_IMP(reset,in,out) = 47 ?l1 l2. ONE l1 /\ REG(in,l2) /\ MUX(reset,l1,l2,out)");; 48 49%----------------------------------------------------------------------------% 50% We load in the definitions of the primitive parts from the theory PARITY. % 51%----------------------------------------------------------------------------% 52 53let ONE = definition `PARITY` `ONE_DEF` 54and REG = definition `PARITY` `REG_DEF` 55and MUX = definition `PARITY` `MUX_DEF`;; 56 57%----------------------------------------------------------------------------% 58% We verify the correctness of the implementation. Since the sepcification is% 59% only partial, we can only prove an implication, not an equivalence. % 60%----------------------------------------------------------------------------% 61 62let RESET_REG_THM = 63 prove_thm 64 (`RESET_REG_THM`, 65 "RESET_REG_IMP(reset,in,out) ==> RESET_REG(reset,in,out)", 66 REWRITE_TAC[RESET_REG;RESET_REG_IMP;REG;ONE;MUX] 67 THEN REPEAT STRIP_TAC 68 THEN ASM_REWRITE_TAC[SUC_SUB1;NOT_SUC;SYM(SPEC_ALL ADD1)]);; 69