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