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