unwind/Manual/description.tex

3 This document describes the facilities provided by the \ml{unwind} library
4 for the HOL system~\cite{description}. The library provides conversions and
9 Most of the functions fall into one of five groups. The first group consists
14 of these begin with \ml{UNFOLD}. The functions in the third group perform
20 I have tried to make the behaviour of the functions uniform. The conversions
21 apply to the smallest term possible, to provide maximum flexibility. The
22 inference rules, on the other hand, are designed to apply to the definition
23 of a hardware component. They expect to be given a theorem of the form:
30 \section{Using the library}
32 The \ml{unwind} library can be loaded into a \HOL\ session using the function
33 \ml{load\_library}\index{load\_library@{\ptt load\_library}} (see the \HOL\
34 manual for a general description of library loading). The first action in the
35 load sequence initiated by \ml{load\_library} is to update the \HOL\
37 updated with a pathname to online help files for the \ML\ functions in the
38 library. After updating the help search path, the \ML\ functions in the
41 The following session shows how the \ml{unwind} library may be loaded using
54 We now illustrate the use of the library on the parity-checker example.
65 We define the sub-components used:
112 Now we define the parity-checker implementation:
136 prune the body of this definition:
157 when trying to unwind and prune the internal lines in the logical
160 which lines to unwind. The tools in the \ml{unwind} library allow the user
161 to be selective in this way. However, it is possible for the machine itself to
162 be selective. The function \ml{UNWIND\_AUTO\_CONV} attempts to analyze the
165 Consider the following term which arises in the parity-checker example:
178 We can represent the dependencies of the lines using a directed graph:
205 which can in turn be represented by the following list:
216 Since we wish to eliminate the internal lines, we want to be left with a
218 be `breaking the loop' at {\small\verb%out%}, giving the following structure:
229 Note that {\small\verb%out%} has been removed from the structure. From the
232 of looping. They can be recognized in the datastructure by the fact that their
236 removed from the datastructure:
252 Unwinding {\small\verb%l3%} then leaves us with the required recursive
255 The problem with the approach just described is that it only unwinds fully if
256 there is at most one loop in the circuit, and the output is in that loop. We
257 can be a bit more general. Consider the circuit:
288 represented by the graph:
302 {\small\verb%out%} will not help because it is not in the loop. However, if we
303 break the loop at {\small\verb%l2%} we can unwind {\small\verb%l1%}. This will
305 {\small\verb%out%} in terms of {\small\verb%l2%}. This is the best that we can
306 do, and it is now up to the user to deal with the recursive equation.
356 {\small\verb%l2%} or {\small\verb%l7%} we will still get stuck because of the
359 the outer loop. However, if we break at {\small\verb%l3%} or {\small\verb%l4%}
362 {\small\verb%out%} in terms of that line. So, the choice of where to break a
363 loop may determine how far the unwinding can go.
365 \ml{UNWIND\_AUTO\_CONV} attempts to break every loop in the circuit using the
368 to break, so that if possible the recursive equations are in terms of these
371 The algorithm used determines from the term a list of line variables. Each
374 line variables are placed in the dependency list for the corresponding line.
375 From the dependency structure, the loops are determined. Lines are then
378 A study of the following circuit reveals why {\em all\/} loops have to be
379 broken. If not all loops are broken, then a remaining loop can make the
427 The dependency structure for the circuit is:
441 The loops for the circuit are:
475 the internal lines except for {\small\verb%l4%} can be pruned. This leaves
479 recursion is also possible. This is illustrated by the following example:
529 is sufficient to break all the loops. The result is three equations: an
533 be seen that the loop analysis technique used by \ml{UNWIND\_AUTO\_CONV} does