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. reset t ==> (out t = T)) /\ 13 (!t. out(t+1) = ((reset t \/ reset(t+1)) => T | in t))");; 14 15%----------------------------------------------------------------------------% 16% Note that the above specification is only partial; it doesn't specify the % 17% output at time 0 when there is no reset. % 18%----------------------------------------------------------------------------% 19 20%----------------------------------------------------------------------------% 21% An implementation of the restable register using non-resetable registers % 22% that power-up storing F. % 23% % 24% reset in % 25% | | % 26% | *-----* | % 27% | | ONE | | % 28% | *-----* | % 29% | | | % 30% |------| |l1 | % 31% | | | | % 32% | *------------------* % 33% | | MUX | % 34% | *------------------* % 35% | | % 36% | | % 37% | |------|l2 % 38% | | | % 39% | | | % 40% | | *-----* % 41% | | | REG | % 42% | | *-----* % 43% | | | % 44% | | | l3 % 45% | | | % 46% *-----------------* % 47% | MUX | % 48% *-----------------* % 49% | % 50% out % 51% % 52% ONE, MUX and REG are as used in the PARITY example % 53% (hol/examples/PARITY.ml). % 54%----------------------------------------------------------------------------% 55 56new_parent `PARITY`;; 57 58let RESET_REG_IMP = 59 new_definition 60 (`RESET_REG_IMP`, 61 "RESET_REG_IMP(reset,in,out) = 62 ?l1 l2 l3. ONE l1 /\ 63 MUX(reset,l1,in,l2) /\ 64 REG(l2,l3) /\ 65 MUX(reset,l2,l3,out)");; 66 67%----------------------------------------------------------------------------% 68% We load in the definitions of the primitive parts from the theory PARITY. % 69%----------------------------------------------------------------------------% 70 71let ONE = definition `PARITY` `ONE_DEF` 72and REG = definition `PARITY` `REG_DEF` 73and MUX = definition `PARITY` `MUX_DEF`;; 74 75%----------------------------------------------------------------------------% 76% We verify the correctness of the implementation. Since the sepcification is% 77% only partial, we can only prove an implication, not an equivalence. % 78%----------------------------------------------------------------------------% 79 80let RESET_REG_THM = 81 prove_thm 82 (`RESET_REG_THM`, 83 "RESET_REG_IMP(reset,in,out) ==> RESET_REG(reset,in,out)", 84 REWRITE_TAC[RESET_REG;RESET_REG_IMP;REG;ONE;MUX] 85 THEN REPEAT STRIP_TAC 86 THEN ASM_REWRITE_TAC[SUC_SUB1;NOT_SUC;SYM(SPEC_ALL ADD1)] 87 THEN ASM_CASES_TAC "(reset:num->bool) t" 88 THEN ASM_CASES_TAC "(reset:num->bool)(SUC t)" 89 THEN ASM_REWRITE_TAC[]);; 90