%%* "Formal Verification of a 64-bit Multiplier" -- 
%%*   To appear in Proceedings of the Fifth International Workshop
%%*   on Computer-Aided Verification (CAV'93)
%%*  
%%*  A TLA+ specification of
%%*     1. a multiplier and its environment
%%*     2. the implementation of a 2n-bit multiplier by four n-bit multipliers
%%*     3. the statement of correctness of the implementation
%%*  and the S/R translation of this specification.
%
%  Preliminary draft cleared by Sam Fuller 18 Nov 92
%
% Modified 26 Jan 93 and 27 Jan 93 to correct typos found by Urban Engberg.
% Some notes for changes added 18 Mar 93.
%
% Drastically modified version of April 93

\documentstyle{article}
\makeatletter
% LLNCS DOCUMENT STYLE -- version 1.1
% for LaTeX version 2.09
% last modified on Mon Jan 17 09:09:45 PST 1994 by lamport

% This style file is an adaptation of
% the original LaTeX article.sty, by:
% Frank Holzwarth, Springer-Verlag Heidelberg,
% Tiergartenstrasse 17, D-6900 Heidelberg.
%
% Modified by Leslie Lamport to
%  * remove the silly ``This article was typset using the ...'' at the
%    end.
%  * remove stretch between paragraphs.
%  * add page numbers, far enough from the text that Springer should
%    be able to cope with them.
%  * made optional argument work with the figure command
%
\typeout{Document Style `llncs', <version 1.1>}

\frenchspacing
\def~{\penalty\@M\kern3pt}

\def\thebibliography#1{\section*{References}\small\list
  {\arabic{enumi}.}{\settowidth\labelwidth{#1.}\leftmargin\labelwidth
    \advance\leftmargin\labelsep
    \usecounter{enumi}}
    \def\newblock{\hskip .11em plus .33em minus -.07em}
    \sloppy
    \sfcode`\.=1000\relax}

\def\ds@citeauthoryear{\def\thebibliography##1{\section*{References}%
    \small\list{}{\settowidth\labelwidth{}\leftmargin\parindent
    \itemindent=-\parindent
    \labelsep=\z@
    \usecounter{enumi}}%
    \def\newblock{\hskip .11em plus .33em minus -.07em}%
    \sloppy
    \sfcode`\.=1000\relax}%
    \def\@cite##1{##1}%
    \def\@lbibitem[##1]##2{\item[]\if@filesw
      {\def\protect####1{\string ####1\space}\immediate
    \write\@auxout{\string\bibcite{##2}{##1}}}\fi\ignorespaces}}%

\newif\if@envcountreset\@envcountresetfalse
\def\ds@envcountreset{\@envcountresettrue}

\def\@mbi{cmmib10}
\def\@ptsize{0} \@namedef{ds@11pt}{\def\@ptsize{1}}
\@namedef{ds@12pt}{\def\@ptsize{2}}
\def\ds@twoside{\@twosidetrue \@mparswitchtrue}
\def\ds@draft{\overfullrule
5pt}
\@options

\ds@twoside

\lineskip 1pt \normallineskip 1pt
\def\baselinestretch{1}

\def\@normalsize{\@setsize\normalsize{12pt}\xpt\@xpt
\abovedisplayskip=3 mm plus6pt minus 4pt
\belowdisplayskip=3 mm plus6pt minus 4pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt}

\mathchardef\Gamma="0100
\mathchardef\Delta="0101
\mathchardef\Theta="0102
\mathchardef\Lambda="0103
\mathchardef\Xi="0104
\mathchardef\Pi="0105
\mathchardef\Sigma="0106
\mathchardef\Upsilon="0107
\mathchardef\Phi="0108
\mathchardef\Psi="0109
\mathchardef\Omega="010A

\def\small{\@setsize\small{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\footnotesize{\@setsize\footnotesize{11pt}\ixpt\@ixpt
\abovedisplayskip=2.5 mm plus5pt minus 3pt
\belowdisplayskip=2.5 mm plus5pt minus 3pt
\abovedisplayshortskip=0mm plus6pt minus 2pt
\belowdisplayshortskip=2 mm plus4pt minus 4pt
\def\@listi{\leftmargin\leftmargini\topsep 4pt plus 2pt minus 2pt}}

\def\scriptsize{\@setsize\scriptsize{8.4pt}\viipt\@viipt}

\def\tiny{\@setsize\tiny{6pt}\vpt\@vpt}
\def\large{\@setsize\large{13.2pt}\xipt\@xipt}
\def\Large{\@setsize\Large{14.4pt}\xiipt\@xiipt}
\def\LARGE{\@setsize\LARGE{16.8pt}\xivpt\@xivpt}
\def\huge{\@setsize\huge{22pt}\xxpt\@xxpt}
\def\Huge{\@setsize\Huge{30pt}\xxvpt\@xxvpt}
\@normalsize

\if@twoside
   \oddsidemargin  44pt
   \evensidemargin 82pt
   \marginparwidth 107pt
\else \oddsidemargin 63pt \evensidemargin 63pt
 \marginparwidth 90pt
\fi
\marginparsep 11pt
\topmargin 11pt \headheight 12pt \headsep 13.66pt
\footheight 12pt \footskip 30pt
\textwidth 12.2truecm
\textheight 19.3truecm
\columnsep 1cc \columnseprule 0pt

\footnotesep 7.7pt
\skip\footins 9pt plus 4pt minus 2pt
\floatsep 12pt plus 2pt minus 2pt
\textfloatsep 8mm plus 2pt minus 4pt
\intextsep 8mm plus 2pt minus 2pt 
\@maxsep 8mm

\dblfloatsep 12pt plus 2pt minus 2pt
\dbltextfloatsep 20pt plus 2pt minus 4pt
\@dblmaxsep 20pt

\@fptop 0pt plus 1fil \@fpsep 8pt plus 2fil \@fpbot 0pt plus 1fil
\@dblfptop0pt plus1fil \@dblfpsep8pt plus2fil\@dblfpbot 0pt plus1fil
\marginparpush 5pt

\parskip 0pt %%%% plus 1pt %% stretch removed by LL 92-09-14
\parindent 1.5em \topsep 8pt plus 2pt minus 4pt
\partopsep 2pt plus 1pt minus 1pt \itemsep \z@
\@lowpenalty 51 \@medpenalty 151 \@highpenalty 301
\@beginparpenalty-\@lowpenalty\@endparpenalty -\@lowpenalty\@itempenalty
-\@lowpenalty

\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle\bf#1$}}
{\mbox{\boldmath$\textstyle\bf#1$}}
{\mbox{\boldmath$\scriptstyle\bf#1$}}
{\mbox{\boldmath$\scriptscriptstyle\bf#1$}}}

\def\@sect#1#2#3#4#5#6[#7]#8{\ifnum #2>\c@secnumdepth
  \def\@svsec{}\else
  \refstepcounter{#1}\edef\@svsec{\csname the#1\endcsname\quad }\fi
  \@tempskipa #5\relax
   \ifdim \@tempskipa>\z@
  \begingroup #6\relax
  \noindent{\hskip #3\relax\@svsec}{\interlinepenalty \@M #8\par}
  \endgroup
    \csname #1mark\endcsname{#7}\addcontentsline
   {toc}{#1}{\ifnum #2>\c@secnumdepth \else
            \protect\numberline{\csname the#1\endcsname}\fi
          #7}\else
  \def\@svsechd{#6\hskip #3\@svsec #8\csname #1mark\endcsname
            {#7}\addcontentsline
             {toc}{#1}{\ifnum #2>\c@secnumdepth \else
               \protect\numberline{\csname the#1\endcsname}\fi
             #7}}\fi
  \@xsect{#5}}

\def\part{\par \addvspace{4ex} \@afterindentfalse \secdef\@part\@spart}

\def\@part[#1]#2{\ifnum \c@secnumdepth >\m@ne \refstepcounter{part}
\addcontentsline{toc}{part}{\thepart \hspace{1em}#1}\else
\addcontentsline{toc}{part}{#1}\fi { \parindent 0pt \raggedright
 \ifnum \c@secnumdepth >\m@ne \Large \bf
 Part\thepart\par\nobreak\fi\huge
\bf #2\markboth{}{}\par } \nobreak \vskip 3ex \@afterheading }

\def\@spart#1{{\parindent 0pt \raggedright
 \huge \bf
 #1\par} \nobreak \vskip 3ex \@afterheading }

\def\section{\@startsection {section}{1}{\z@}{-18pt plus -4pt minus
-4pt}{12pt plus 4pt minus 4pt}{\Large\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsection{\@startsection{subsection}{2}{\z@}{-18pt plus-4pt minus
 -4pt}{8pt plus 4pt minus 4pt}{\normalsize\bf\boldmath
\pretolerance=10000\relax\rightskip=0pt plus8em}}
\def\subsubsection{\@startsection{subsubsection}{3}{\z@}{-18pt plus-4pt
 minus -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\bf\boldmath}}
\def\paragraph{\@startsection{paragraph}{4}{\z@}{-12pt plus -4pt minus
 -4pt}{-0.5em plus -.22em minus -0.1em}{\normalsize\it}}
\def\subparagraph#1{\typeout{LLNCS Warning: You should not use
\protect\subparagraph \space in this style.}\vskip0.5cm
You should not use $\backslash${\tt subparagraph} in this
style.\vskip0.5cm}

\setcounter{secnumdepth}{2}

\def\appendix{\par
 \setcounter{section}{0}
 \setcounter{subsection}{0}
 \def\thesection{\Alph{section}}}

\leftmargini 17pt     \leftmarginii 17pt
\leftmarginiii 17pt   \leftmarginiv 17pt
\leftmarginv 10pt       \leftmarginvi 10pt
\leftmargin\leftmargini \labelwidth\leftmargini
\advance\labelwidth-\labelsep
\labelsep 5pt
\parsep 0pt plus 1pt
\def\@listi{\leftmargin\leftmargini}
\def\@listii{\leftmargin\leftmarginii
 \labelwidth\leftmarginii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiii{\leftmargin\leftmarginiii
 \labelwidth\leftmarginiii\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listiv{\leftmargin\leftmarginiv
 \labelwidth\leftmarginiv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listv{\leftmargin\leftmarginv
 \labelwidth\leftmarginv\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}
\def\@listvi{\leftmargin\leftmarginvi
 \labelwidth\leftmarginvi\advance\labelwidth-\labelsep
 \topsep 0pt plus 1pt}

\def\labelenumi{\arabic{enumi}.}
\def\theenumi{\arabic{enumi}}
\def\labelenumii{(\alph{enumii})}
\def\theenumii{\alph{enumii}}
\def\p@enumii{\theenumi}
\def\labelenumiii{\roman{enumiii}.}
\def\theenumiii{\roman{enumiii}}
\def\p@enumiii{\theenumi(\theenumii)}
\def\labelenumiv{\Alph{enumiv}.}
\def\theenumiv{\Alph{enumiv}}
\def\p@enumiv{\p@enumiii\theenumiii}

\def\labelitemi{\bf --}
\def\labelitemii{$\bullet$}
\def\labelitemiii{$\ast$}
\def\labelitemiv{$\cdot$}

\def\verse{\let\\=\@centercr
 \list{}{\itemsep\z@ \itemindent -1.5em\listparindent \itemindent
 \rightmargin\leftmargin\advance\leftmargin 1.5em}\item[]}
\let\endverse\endlist
\def\quotation{\list{}{\listparindent 1.5em
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[]}
\let\endquotation=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

\def\descriptionlabel#1{\hspace\labelsep \bf #1}
\def\description{\list{}{\labelwidth\z@ \itemindent-\leftmargin
 \let\makelabel\descriptionlabel}}
\let\enddescription\endlist

\def\theequation{\arabic{equation}}

\def\titlepage{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
 \else \newpage \fi \thispagestyle{empty}\c@page\z@}
\def\endtitlepage{\if@restonecol\twocolumn \else \newpage \fi}

\arraycolsep 1.4pt \tabcolsep 1.4pt \arrayrulewidth .4pt \doublerulesep
2pt
\tabbingsep \labelsep

\skip\@mpfootins = \skip\footins
\fboxsep = 3pt \fboxrule = .4pt

%\newcounter{part}
%\newcounter {section}
%\newcounter {subsection}[section]
%\newcounter {subsubsection}[subsection]
%\newcounter {paragraph}[subsubsection]

\def\thepart{\Roman{part}}
\def\thesection {\arabic{section}}
\def\thesubsection {\thesection.\arabic{subsection}}
\def\thesubsubsection {\thesubsection.\arabic{subsubsection}}
\def\theparagraph {\thesubsubsection.\arabic{paragraph}}

\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}

\def\tableofcontents{\section*{Table of Contents}
 \@starttoc{toc}}
\def\l@part#1#2{\addpenalty{\@secpenalty}
 \addvspace{2.25em plus 1pt} \begingroup
 \@tempdima 3em \parindent \z@ \rightskip \@pnumwidth \parfillskip
-\@pnumwidth
 {\Large \bf \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}}\par
 \nobreak \endgroup}
%
\def\numberline#1{\advance\hangindent by\@tempdima%
\hbox to\@tempdima{\hss#1\enspace}}
%
\def\bf@dottedtocline#1#2#3#4#5{\ifnum #1>\c@tocdepth \else
  \vskip \z@ plus .2pt
  {\leftskip #2\relax \rightskip \@tocrmarg \parfillskip -\rightskip
    \parindent #2\relax\@afterindenttrue
   \interlinepenalty\@M
   \leavevmode
   \@tempdima #3\relax \advance\leftskip \@tempdima \hbox{}\hskip
   -\leftskip
{\bf#4}\nobreak\leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern \@dotsep
       mu$}\hfill \nobreak \hbox to\@pnumwidth{\hfil\rm #5}\par}\fi}
%
\def\l@section{\vskip2mm\bf@dottedtocline{1}{0em}{1.7em}}
\def\l@subsection{\@dottedtocline{2}{1.7em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{4em}{2em}}
\def\l@paragraph{\@dottedtocline{4}{6em}{2em}}
\def\l@subparagraph{\@dottedtocline{5}{8em}{2em}}
\def\listoffigures{\section*{List of Figures\markboth
 {List of Figures}{List of Figures}}\@starttoc{lof}}
\def\l@figure{\@dottedtocline{1}{1.5em}{2.3em}}
\def\listoftables{\section*{List of Tables\markboth
 {List of Tables}{List of Tables}}\@starttoc{lot}}
\let\l@table\l@figure

\def\endthebibliography{\endlist\normalsize}

%\newif\if@restonecol
\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
\columnseprule \z@
\columnsep 35pt\twocolumn[\section*{Index}]
 \markboth{Index}{Index}\thispagestyle{plain}\parindent\z@
 \parskip\z@ plus .3pt\relax\let\item\@idxitem}
\def\@idxitem{\par\hangindent 40pt}
\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}
\def\indexspace{\par \vskip 10pt plus 5pt minus 3pt\relax}

\def\footnoterule{\kern-3\p@\hrule width 2 true cm\kern 2.6\p@}

\long\def\@makefntext#1{\@setpar{\@@par\@tempdima \hsize
  \advance\@tempdima-1em\parshape \@ne 1em\@tempdima}\par
  \parindent 1em\noindent \hbox to \z@{\hss$^{\@thefnmark}$\ }#1}

\setcounter{topnumber}{2}
\def\topfraction{.9}
\setcounter{bottomnumber}{1}
\def\bottomfraction{.3}
\setcounter{totalnumber}{3}
\def\textfraction{.15}
\def\floatpagefraction{.85}
\setcounter{dbltopnumber}{2}
\def\dbltopfraction{.85}
\def\dblfloatpagefraction{.85}

\long\def\@makecaption#1#2{
 \vskip 10pt
 \setbox\@tempboxa\hbox{{\bf #1} #2}
 \ifdim \wd\@tempboxa >\hsize \unhbox\@tempboxa\par \else \hbox
to\hsize{\box\@tempboxa\hfil}
 \fi\vskip5pt}

\long\def\@caption#1[#2]#3{\addcontentsline{\csname
  ext@#1\endcsname}{#1}{\protect\numberline{\csname
  the#1\endcsname}{\ignorespaces #2}}\par
  \begingroup
    \@parboxrestore
    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
  \endgroup}

%\newcounter{figure}
\def\thefigure{\@arabic\c@figure}

\def\fps@figure{htbp}
\def\ftype@figure{1}
\def\ext@figure{lof}
\def\fnum@figure{Fig.\thinspace\thefigure.}
\def\figure{\@ifnextchar[{\@yfigure}{\@xfigure}}
\def\@xfigure{\@float{figure}\small\rm}
\def\@yfigure[#1]{\@float{figure}[#1]\small\rm}
\def\endfigure{\vskip-5pt\end@float}
\@namedef{figure*}{\@dblfloat{figure}}
\@namedef{endfigure*}{\end@dblfloat}

%\newcounter{table}
\def\thetable{\@arabic\c@table}
\def\fps@table{htbp}
\def\ftype@table{2}
\def\ext@table{lot}
\def\fnum@table{Table \thetable.}
\def\table{\@float{table}\small\rm}
\let\endtable\end@float
\@namedef{table*}{\@dblfloat{table}}
\@namedef{endtable*}{\end@dblfloat}

% LaTeX does not provide a command to enter the authors institute
% addresses. The \institute command is defined here.

\newcounter{@inst}
\newcounter{@auth}

\def\institute#1{\gdef\@institute{#1}}

\def\institutename{\par
 \begingroup
 \parskip=\z@
 \parindent=\z@
 \setcounter{@inst}{1}%
 \def\and{\par\stepcounter{@inst}%
 \noindent$^{\the@inst}$\enspace\ignorespaces}%
 \setbox0=\vbox{\def\thanks##1{}\@institute}%
 \ifnum\c@@inst=1\relax
 \else
   \setcounter{footnote}{\c@@inst}%
   \setcounter{@inst}{1}%
   \noindent$^{\the@inst}$\enspace
 \fi
 \ignorespaces
 \@institute\par
 \endgroup}

\def\@thanks{}

\def\@fnsymbol#1{\ifcase#1\or\star\or{\star\star}\or{\star\star\star}%
   \or \dagger\or \ddagger\or
   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
   \or \ddagger\ddagger\else\@ctrerr\fi\relax}

\def\inst#1{\unskip$^{#1}$}

\def\subtitle#1{\gdef\@subtitle{#1}}
\def\@subtitle{}

\def\maketitle{\par
 \begingroup
 \parindent=\z@
 \def\thefootnote{\fnsymbol{footnote}}
 \if@twocolumn
 \twocolumn[\@maketitle]
 \else \newpage
 \global\@topnum\z@ \@maketitle \fi\thispagestyle{empty}\@thanks
 \endgroup
 \let\maketitle\relax
 \let\@maketitle\relax
 \gdef\@thanks{}\gdef\@author{}\gdef\@title{}\gdef\@subtitle{}%
 \let\thanks\relax}

\def\@maketitle{\newpage
 \begin{center}%
 {\LARGE \bf\boldmath
  \pretolerance=10000
  \@title \par}\vskip .8cm
\if!\@subtitle!\else {\Large \bf\boldmath
  \vskip -.65cm
  \pretolerance=10000
  \@subtitle \par}\vskip .8cm\fi
{\normalsize\rm\lineskip .5em
\@author\vskip.35cm}
 {\small\rm\institutename}
 \end{center}%
 }

\mark{{}{}}

% Define `abstract' environment
\def\abstract{%
\list{}{\advance\topsep by0.35cm\relax\small\rm
 \leftmargin=1cm
 \labelwidth=\z@
 \listparindent=\z@
 \itemindent\listparindent
 \rightmargin\leftmargin}\item[\hskip\labelsep\bf Abstract.]}
\let\endabstract=\endlist
\def\quote{\list{}{\rightmargin\leftmargin}\item[]}
\let\endquote=\endlist

%%% Modified by LL to print page numbers
\def\ps@headings{\def\@evenhead{\makebox[\textwidth]{\hfill 
   \raisebox{2cm}[0pt][0pt]{\fbox{\LARGE\thepage}\hspace{-2cm}}}}%
\let\@oddhead\@evenhead
\def\@evenfoot{}
\let\@oddfoot\@evenfoot
\def\sectionmark##1{}%
\def\subsectionmark##1{}}
\def\ps@myheadings{\let\@mkboth\@gobbletwo
\def\@oddhead{\hbox{}\small\rm\rightmark \hfil\thepage}%
\def\@oddfoot{}\def\@evenhead{\small\rm\thepage\hfil
\leftmark\hbox {}}%
\def\@evenfoot{}\def\sectionmark##1{}\def\subsectionmark##1{}}

\def\today{\ifcase\month\or
 January\or February\or March\or April\or May\or June\or
 July\or August\or September\or October\or November\or December\fi
 \space\number\day, \number\year}

\ps@headings \pagenumbering{arabic} \onecolumn
\if@twoside\else\raggedbottom\fi

% new environments and theorems
% borrowed form the LTMP-style of Springer-Verlag
% designed by Dr. Christoph Ender
%
% define the new theorem like environments
% define a new style of environments where it is possible to define
% the font % used as the theorem name and the fontfamily for the text.
%
% \newstytheorem{name}{thefont}{txtfont}{Text}[Counter]
% \newstytheorem{name}{thefont}{txtfont}[oldname]{Text}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
%
\def\newstytheorem#1#2#3{%
\@ifnextchar[{\che@othm{#1}{#2}{#3}}{\che@nthm{#1}{#2}{#3}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@nthm#1#2#3#4{%
\@ifnextchar[{\che@xnthm{#1}{#2}{#3}{#4}}{\che@ynthm{#1}{#2}{#3}{#4}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
% #5 - add theorem counter to reset list of another counter
%
\def\che@xnthm#1#2#3#4[#5]{\expandafter
\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}\if@envcountreset\@addtoreset{#1}{#5}\fi
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#4}{#2}{#3}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% #1 - name of theorem
% #2 - theorem font
% #3 - text font
% #4 - text string of thorem name
%
\def\che@ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
{\@definecounter{#1}%
\expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
\global\@namedef{#1}{\che@thm{#1}{#2}{#3}{#4}}\global
\@namedef{end#1}{\@endtheorem}}}
%
% change oldthm if oldname in specification is '*'
% then don't use a counter
% #1 - countername
% #2 - theorem font
% #3 - text font
% #4 - counter used
% #5 - string containing theorem name to print
%
\def\che@othm#1#2#3[#4]#5{\expandafter\@ifdefinable
\csname#1\endcsname%
{\@@othm@{#1}{#2}{#3}{#4}{#5}\global\@namedef{end#1}{\@endtheorem}}}
%
\def\@@othm@#1#2#3#4#5{\if *#4{\global\@namedef{the#1}{\relax}
\global\@namedef{#1}{\@bthm@{}{#5}{#2}{#3}}}\else
{\global\@namedef{the#1}{\@nameuse{the#4}}% define the counter
\global\@namedef{#1}{\che@thm{#4}{#5}{#2}{#3}}}\fi}
%
% new defs for theorem environment che 17-MAR-1989
% it improves the option possible
%
% #1 - countername  = theorem name
% #2 - string containing theorem name to print
% #3 - theorem font
% #4 - text font
\def\che@thm#1#2#3#4{\@ifnextchar({\@athm{#1}{#2}{#3}{#4}}{%
\@ifnextchar *{\@bthm{#1}{#2}{#3}{#4}}%
{\@@thm{#1}{#2}{#3}{#4}}}}
%
% \begin{thm}(A.1)[test]      results in:
% \end{thm}                               thm A.1 (test) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - is the new label
% #6 - optional string
%
\def\@athm#1#2#3#4(#5){\@ifnextchar[{%
\@aythm{#1}{#2}{#3}{#4}{#5}}{\@axthm{#1}{#2}{#3}{#4}{#5}}}
\def\@axthm#1#2#3#4#5{\@@locthmlab{#1}{#5}%
\@begintheorem{#2}{#5}{#3}{#4}\ignorespaces}
\def\@aythm#1#2#3#4#5[#6]{\@@locthmlab{#1}{#5}%
\fuh@opargbegintheorem{#2}{#5}{#6}{#3}{#4}\ignorespaces}
%
% \begin{thm}*[xytest]        results in:
% \end{thm}                               thm (xytest) ....
% #1 - theorem
% #2 - string of theorem name
% #3 - font for theorem name and label
% #4 - Text font
% #5 - optional string
%
\def\@bthm@#1#2#3#4{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bthm#1#2#3#4*{\@ifnextchar[{\@bythm{#1}{#2}{#3}{#4}}{%
\@bxthm{#1}{#2}{#3}{#4}}}
\def\@bxthm#1#2#3#4{\if !#1!\relax\else\@@locthmlab{#1}{}\fi
\@@begintheorem{#2}{#3}{#4}\ignorespaces}
\def\@bythm#1#2#3#4[#5]{%
\@@opargbegintheorem{#2}{#3}{#4}{#5}\ignorespaces}
%
% define local label
%   if no number or a user specified label occured
%
\def\@@locthmlab#1#2{\expandafter\def\csname the#1\endcsname{#2}
\let\@chetempa\protect\def\protect{\noexpand\protect\noexpand}%
\edef\@currentlabel{\csname p@#1\endcsname\csname the#1\endcsname}%
\let\protect\@chetempa}
%
% #1 - counter = theorem name
% #2 - string with name
% #3 - font for theorem name and label
% #4 - font for text
\def\@@thm#1#2#3#4{\refstepcounter
    {#1}\@ifnextchar[{\che@ythm{#1}{#2}{#3}{#4}}{%
    \che@xthm{#1}{#2}{#3}{#4}}}
%
\def\che@xthm#1#2#3#4{\che@begintheorem{#2}{\csname
the#1\endcsname}{#3}{#4}\ignorespaces}
\def\che@ythm#1#2#3#4[#5]{\che@opargbegintheorem{#2}{\csname
       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
%
% #1 - name of theorem
% #2 - label string
% #3 - font for name and lable
% #4 - text fomt
%
\def\che@begintheorem#1#2#3#4{#4\trivlist\item[\hskip\labelsep
#3#1\ts #2.]}
%
% #1 - name of theorem
% #2 - label string
% #3 - additonal text
% #4 - font for name and lable
% #5 - text fomt
%
\def\che@opargbegintheorem#1#2#3#4#5{#5\trivlist
\item[\hskip\labelsep#4#1\ts #2\ #3.]}
%
\def\fuh@opargbegintheorem#1#2#3{\it \trivlist
      \item[\hskip \labelsep{\bf #1\ #2\ (#3).}]}
%
\def\@@begintheorem#1#2#3{#3\trivlist\item[\hskip\labelsep
#2#1.]}
\def\@@opargbegintheorem#1#2#3#4{#3\trivlist\item[\hskip\labelsep
#2#1 #4.]}

\newstytheorem{theorem}{\bf}{\it}{Theorem}[section]
\newstytheorem{example}{\it}{\rm}{Example}[section]
\newstytheorem{proposition}{\bf}{\it}[theorem]{Proposition}
\newstytheorem{corollary}{\bf}{\it}[theorem]{Corollary}
\newstytheorem{lemma}{\bf}{\it}[theorem]{Lemma}
\newstytheorem{proof}{\it}{\rm}[*]{Proof}
\newstytheorem{definition}{\bf}{\rm}[theorem]{Definition}
\newstytheorem{remark}{\it}{\rm}[*]{Remark}
\newstytheorem{exercise}{\it}{\rm}[theorem]{Exercise}
\newstytheorem{problem}{\it}{\rm}[theorem]{Problem}
\newstytheorem{solution}{\it}{\rm}[theorem]{Solution}
\newstytheorem{note}{\it}{\rm}[theorem]{Note}
\newstytheorem{question}{\it}{\rm}[theorem]{Question}

\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}

\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
\cr\to\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
\gets\cr\to\cr}}}}}
\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
<\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
\noalign{\vskip1.2pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
\noalign{\vskip1pt}=\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr
\noalign{\vskip0.9pt}=\cr}}}}}
\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
\halign{\hfil
$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
>\cr\noalign{\vskip-1pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.8pt}<\cr}}}
{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
\def\bbbr{{\rm I\!R}} %reelle Zahlen
\def\bbbm{{\rm I\!M}}
\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
\def\bbbf{{\rm I\!F}}
\def\bbbh{{\rm I\!H}}
\def\bbbk{{\rm I\!K}}
\def\bbbp{{\rm I\!P}}
\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
\def\bbbs{{\mathchoice
{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
\def\bbbz{{\mathchoice {\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\textstyle Z\kern-0.4em Z$}}
{\hbox{$\sf\scriptstyle Z\kern-0.3em Z$}}
{\hbox{$\sf\scriptscriptstyle Z\kern-0.2em Z$}}}}
\def\ts{\thinspace}

\def\typeset{\vfill\small\noindent 
% modified by LL to supress LaTeX ack.
%This article was processed using
%the \LaTeX\ macro package with LLNCS style
\par}

\def\enddocument{\par\typeset
\@checkend{document}\clearpage\begingroup
\if@filesw \immediate\closeout\@mainaux
\def\global\@namedef##1##2{}\def\newlabel{\@testdef r}%
\def\bibcite{\@testdef b}\@tempswafalse\makeatletter\input \jobname.aux
\if@tempswa \@warning{Label(s) may have changed. Rerun to get
cross-references right}\fi\fi\endgroup\deadcycles\z@\@@end}


%% one-sided printing
\@twosidefalse
\makeatother

\renewcommand{\textfraction}{.1}
\renewcommand{\floatpagefraction}{.85}
\renewcommand{\topfraction}{.85}
\renewcommand{\bottomfraction}{.85}
\pagestyle{headings}
\newcommand{\TLA}[1]{TLA$^{#1}$}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%               TO GET SUBEQUATION NUMBERS                       %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%

\newcounter{subeqn}
\newcommand{\subeqns}{\renewcommand{\theequation}{\arabic
     {equation}\alph{subeqn}}}
\newcommand{\nosubeqns}{\renewcommand{\theequation}{\arabic
     {equation}}}
\newcommand{\firstlabel}[1]{\setcounter{subeqn}{1}\label{#1}}
\newcommand{\sublabel}[1]{\addtocounter{subeqn}{1}%
         \addtocounter{equation}{-1}\label{#1}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                        NOTATION                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%
% Ordinary Math:
%   \implies  : =>
%   \deq      : equals by definition
%   \vbl{foo} : foo formatted as a variable
%   conj      : environment producing bulleted list of conjuncts
%   disj      : environment producing bulleted list of disjuncts
%
% TLA: 
%   \act{exp} : Formats exp in math mode, with the first character 
%               in \cal style.  Thus, \act{A_1} produces ${\cal A}_1$
%   \sqact{A}{v}  : [A]_v   (formatted like \act)
%   \anact{A}{v}  : <A>_v   (formatted like \act)
%   \unchanged{f} : Unchanged f
%   \enabled{A}   : enabled predicate of A
%   \WF{f}{A}     : WF_f(A)
%   \SF{f}{A}     : SF_f(A)
%   \closure{P}       : The closure of P.
%   \orthogonal{P}{Q} : P _|_ Q
%   \valid{P}     : |= P   
%   \tuple{x}     : <x>
%   \plus{E}      : E^{\oplus}
%   \xlate{F}     : S/R translation of TLA formula F
%   \lang{S}  : Language of S

% Ordinary Math:
\newcommand{\implies}{\Rightarrow}
\newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\Delta}{=}}}
\newcommand{\vbl}[1]{{\it #1\/}}
\newenvironment{conj}{\begin{array}[t]{@{\land\;}l@{}}}{\end{array}}
\newenvironment{disj}{\begin{array}[t]{@{\lor\;}l@{}}}{\end{array}}
% TLA:
\newcommand{\closure}[1]{\mathdef{{\cal C}(#1)}}
\newcommand{\orthogonal}[2]{\mathdef{#1\perp#2}}
\newcommand{\act}[1]{\mathdef{\makecal#1}}
\newcommand{\makecal}[1]{{\cal #1}}
\newcommand{\sqact}[2]{\mathdef{[\act{#1}]_{#2}}}
\newcommand{\anact}[2]{\mathdef{\langle\act{#1}\rangle_{#2}}}
\newcommand{\unchanged}[1]{\mathdef{{\it Unchanged}~#1}}
\newcommand{\enabled}[1]{\mathdef{{\it Enabled}~#1}}
\newcommand{\WF}[2]{\mathdef{{\rm WF}_{#1}(#2)}}
\newcommand{\SF}[2]{\mathdef{{\rm SF}_{#1}(#2)}}
\newcommand{\valid}[1]{\mathdef{\models#1}}
\newcommand{\tuple}[1]{\mathdef{\langle#1\rangle}}
\newcommand{\plus}[1]{\mathdef{#1^{\oplus}}}
\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
   [0pt][l]{$\exists\s{-.517}\exists\s{-.517}\exists$}}\exists\s{-.517}\exists
            \s{-.517}\exists$}}
%\newcommand{\EE}{\makebox{$\raisebox{.05em}{\makebox
%   [0pt][l]{$\exists\!\!\!\exists\!\!\!\exists$}}\exists\!\!\!\exists
%            \!\!\!\exists$}}
\newcommand{\xlate}[1]{\mathdef{\widehat{#1}}}
\newcommand{\lang}[1]{\mathdef{{\cal L}(#1)}}

%\mathdef
\newcommand{\mathdef}[1]{\relax\ifmmode #1\else $#1$\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                      MARGINAL NOTES                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
\newif\iffirstmarginal \firstmarginaltrue
\newcommand{\marginalnote}[1]{\marginpar{\raggedright\small\it #1}%
   \iffirstmarginal\typeout{****************************************}%
                   \typeout{******** MARGINAL NOTES IN TEXT ********}%
                   \typeout{****************************************}%
       \global\firstmarginalfalse\fi}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                      MISCELLANY                                %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    

% theorem environment
% \s{i}      : produces an i em space.
% \kwd{WORD} : WORD formatted as a keyword
% \newtheorem{theorem}{Theorem}      
\newcommand{\s}[1]{\hspace*{#1em}} 
\newcommand{\kwd}[1]{\mbox{\bf \lowercase{#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                           S/R SPECS                            %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%
% \srkwd{word}  : S/R keyword
% \srcomk{text} : S/R comment  (first comment--used to set tab stops)
% \srcom{text}  : S/R comment  (subsequent comments)
\newcommand{\srkwd}[1]{{\bf #1}}
\newcommand{\srcomk}[1]{\= {\rm /* }{\it #1\/} \= {\rm */}}
\newcommand{\srcom}[1]{\> {\rm /* }{\it #1\/}\> {\rm */}}

%%%%%%%%%%%%%%%%%%%%%%%%% THe TLA environment
\makeatletter

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
%                  COMMANDS FROM spec92.sty                      %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
\newlength{\@charwidth}
\settowidth{\@charwidth}{{\small\tt M}}
\newlength{\boxrulewd}\setlength{\boxrulewd}{.4pt}
\newlength{\boxindent}\setlength{\boxindent}{22\@charwidth}
\newlength{\boxlineht}\setlength{\boxlineht}{.5\baselineskip}
\newcommand{\boxsep}{\@charwidth}
\newlength{\boxruleht}
\newlength{\boxruledp}
\newcommand{\@computerule}{%
  \setlength{\boxruleht}{.5ex}%
  \setlength{\boxruledp}{-\boxruleht}%
  \addtolength{\boxruledp}{\boxrulewd}}
\newcommand{\boxrule}{\leaders\hrule height \boxruleht depth \boxruledp
                      \hfill\mbox{}}

\newcommand{\@nmlineraise}{\if@botline -\boxrulewd
    \else-\boxlineht\fi}
\newcommand{\nameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{.5\baselineskip}}
\newif\if@botline

%%%%%%%%%%%%%%%%%%END COMMANDS FROM spec92.sty %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{module}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\/} }\par
        }{\par\tlabotline\end{trivlist}}

\newenvironment{submodule}[1]{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf module} {\it #1\/} }\par
        }{\par\tlabotline\end{list}}

\newenvironment{cmodule}[1]{\begin{trivlist}\flushleft\@computerule
            \item[]\tlanameline{\ {\bf constant module} {\it #1\/} }\par
        }{\par\tlabotline\end{trivlist}}


\newcommand{\tlanameline}[1]{\hspace*{-\boxsep}%
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
    \boxrule
    #1\boxrule
    \raisebox{\@nmlineraise}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

%%%%% Fix to \midline and \botline from spec92

\newcommand{\midbar}{\par\hspace{-\boxsep}%
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-.5\boxlineht}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}\par}

\newcommand{\tlabotline}{\hspace{-\boxsep}%
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}%
     \boxrule
    \raisebox{-\boxrulewd}[0pt][0pt]{\rule[.5ex]{\boxrulewd
               }{\boxlineht}}\hspace{-\boxsep}\vspace{0pt}}

\newcommand{\xtrivlist}{\begin{list}{}{%
       \leftmargin=1em%
       \labelwidth=0pt%
       \labelsep=0pt%
       \parsep=0pt%
       \topsep=0pt%
       \partopsep=0pt%
       \itemsep=0pt}}
\def\endxtrivlist{\end{list}}

\def\xtabbing{\lineskip \z@\let\>\@rtab\let\<\@ltab\let\=\@settab
     \let\+\@tabplus\let\-\@tabminus\let\`\@tabrj\let\'\@tablab
     \let\\=\@tabcr
     \global\@hightab\@firsttab
     \global\@nxttabmar\@firsttab
     \dimen\@firsttab\@totalleftmargin
     \global\@tabpush0 \global\@rjfieldfalse
     \xtrivlist \item[]\if@minipage\else\vskip\parskip\fi
     \setbox\@tabfbox\hbox{\rlap{\indent\hskip\@totalleftmargin
       \the\everypar}}\def\@itemfudge{\box\@tabfbox}\@startline\ignorespaces}

\def\endxtabbing{\@stopline\ifnum\@tabpush > 0 \@badpoptabs \fi\endxtrivlist}

\newenvironment{decls}[1]{\par{\bf #1}\begin{xtabbing}%
  \hspace{1em}\=\+\kill}{\end{xtabbing}}

% \newcommand{\deq}{\mathrel{\stackrel{\scriptscriptstyle\mathchar"7001}{=}}}
\newcommand{\defeq}{\mathdef{\,\;\deq\,\;}}
% \newcommand{\implies}{\Rightarrow}
% \newcommand{\s}[1]{\hspace*{#1em}}
\newcommand{\vs}[1]{\raisebox{-#1em}{\rule{0pt}{.1pt}}}
%%%\newcommand{\tuple}[1]{\mathdef{\langle\,#1\,\rangle}}
%\newcommand{\tuple}[1]{\mathdef{\langle#1\rangle}}
\newcommand{\e}{\Leftrightarrow}         % :e:   == \Leftrightarrow
\newcommand{\X}{\mathdef{\times}}
\newcommand{\lr}{{\speclblb}}
\newcommand{\rr}{{\specrbrb}}
\newcommand{\bs}{\mbox{\tt \symbol{'134}}}
\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Verification of a Multiplier: 64 Bits and Beyond}
%% \protect\marginpar{\normalsize How about:\\ {\it 128 Bits and Beyond\/}?}}

% \author{R. P. Kurshan\\
% \normalsize AT\&T Bell Labs\\
% Murray Hill, NJ 07974\\
% {\tt k@research.att.com}
%  \and 
% \large Leslie Lamport\\
% \normalsize
% Digital Equipment Corporation\\
% 130 Lytton Avenue\\
% Palo Alto, CA 94301\\
% {\tt lamport@src.dec.com}}

\author{R. P. Kurshan\inst{1} and
Leslie Lamport\inst{2}}
\institute{AT\&T Bell Labs\\
Murray Hill, NJ 07974\\
{\tt k@research.att.com}
 \and 
Digital Equipment Corporation\\
%130 Lytton Avenue\\
Palo Alto, CA 94301%\\
%{\tt lamport@src.dec.com}
}

\date{14 April 1993}

\begin{document}
 \thispagestyle{empty}
 \mbox{}
 \vfill
 \begin{center}
 \LARGE
 \bf Verification of a Multiplier: 64 Bits and Beyond
 
 \large
 \vspace{1.5\baselineskip}
 
 \hspace*{-.075\textwidth}
 \begin{minipage}[t]{.45\textwidth}
   \centering
   R. P. Kurshan\\
 AT\&T Bell Labs\\
Murray Hill, NJ 07974\\
{\tt k@research.att.com}
 \end{minipage}%
~% 
 \begin{minipage}[t]{.45\textwidth}
   \centering
    Leslie Lamport\\
Digital Equipment Corporation\\
130 Lytton Avenue\\
Palo Alto, CA 94301\\
{\tt lamport@src.dec.com}
 \end{minipage}
 

\vspace{1.5\baselineskip}
14 April 1993


%\vspace{3\baselineskip}
%\fbox{\begin{minipage}{.75\textwidth}
%\centering
%\LARGE REVISED \\[.75\baselineskip]
%SUPERSEDES 12 April VERSION
%\end{minipage}}

\end{center}
 

 \vspace{7\baselineskip} 
 
 \noindent
To appear in {\em Proceedings of the 
 Fifth International Workshop on Computer-Aided Verification\/}
 \vfill \vfill 
 \newpage

\setcounter{page}{1}
%try 

\maketitle\thispagestyle{empty}
\begin{abstract}
Verifying a 64-bit multiplier has a computational complexity that puts
it beyond the grasp of current finite-state algorithms, including
those based upon homomorphic reduction, the induction principle, and
bdd fixed-point algorithms.  Theorem proving, while not bound by the
same computational constraints, may not be feasible for routinely
coping with the complex, low-level details of a real multiplier.  We
show how to verify such a multiplier by applying COSPAN, a
model-checking algorithm, to verify local properties of the complex
low-level circuit, and using TLP, a theorem prover based on the
Temporal Logic of Actions, to prove that these properties imply the
correctness of the multiplier.  Both verification steps are automated,
and we plan to mechanize the translation between the languages of TLP
and COSPAN\@.
\end{abstract}

%try
\section{Introduction}

For finite-state systems, it is in principle possible to use model
checking to verify properties of a system automatically, with little
human intervention.  
However, computational complexity limits the applicability
of such methods.  Verifying a 64-bit multiplier is beyond the
capability of existing model checkers, even with indirect methods such
as homomorphic reduction~\cite{kurshan:reducibility,kurshan:analysis},
structural induction~\cite{kurshan:structural}, and fixed-point
algorithms using binary decision diagrams~\cite{bryant:graph}.

Mechanical theorem proving provides an alternative to automatic model
checking.  However, it is hard work.  Proving that a system satisfies
even a fairly simple property can be painful.  Although progress is
being made, and there have been some impressive verifications using
theorem provers~\cite{chin:verified}, it is unclear how soon theorem
proving will be feasible for the routine verification of complicated
systems.  In any case, complementing a theorem prover with a model
checker that, when feasible, verifies proof obligations automatically
will surely save work.

We show how to combine theorem proving and model checking to
mechanically verify systems that are more difficult or infeasible to
verify by either method alone.  Our approach applies to systems with a
relatively small number of different high-level components.
Components may be replicated without limit, if they are interconnected
in a fairly regular fashion, and may have an arbitrarily complex
low-level structure.  Model checking is used to verify the individual
components, and theorem proving is used to show that the complete
system satisfies its specification if each component does.

As an example, we verify a $k\cdot2^{m}$-bit multiplier, constructed
from $k$-bit multipliers by recursively applying a method for
implementing a $2N$-bit multiplier with four $N$-bit multipliers.  The
$k$-bit multiplier could implement a complex algorithm such as a
radix-4 modified version of Booth's algorithm~\cite{koren:computer}.
We could choose $k$ as large as~$8$.  The 8-bit multiplier is small
enough to be verified by model checking, but complicated enough to
make its verification with theorem proving very difficult.  For
$k\cdot2^{m}$ equal to 64, the complete multiplier is too complex to
be verified entirely by model checking.  Abstracting components
(homomorphic reduction~\cite{kurshan:reducibility}) cannot help,
because it cannot reduce the complexity below the size of the combined
inputs, which exceeds the limit of tractability for a multiplier.

In this simple example, we have verified not just a 64-bit multiplier,
but an $8\cdot2^{m}$-bit multiplier for all values of $m$.  Real
multipliers are not constructed by such a simple recursive procedure.
However, we expect our approach of combining model checking of local
properties with theorem proving to work for real multipliers.

We combine two existing tools: the TLP theorem
prover~\cite{engberg:mechanical}, which verifies models written in the
Temporal Logic of Actions (TLA)~\cite{lamport:newtla}, and the
automata-theoretic model checker COSPAN~\cite{har-el:software}, which
verifies models written in the language S/R~\cite{katzenelson:s/r}.
We chose to combine TLA and S/R because they are simple and have
similar semantic bases.  Moreover, a tool exists for the automatic
synthesis to hardware of an S/R specification.  In principle, we could
write the models in either language and translate to the other.  We
translate from TLA to S/R both because TLA is more concise, and
because theorem proving requires understanding what one is proving,
which is easier if the theorem to be proved was written by a human
rather than generated by a translator.


Four models are used: $M(N)$, an abstract $N$-bit multiplier, which
essentially asserts that its output is the product of its inputs;
$E(N)$, the multiplier's environment; $\vbl{DM}(N)$, a circuit that
combines four $N$-bit multipliers to implement a $2N$-bit multiplier;
and $B(k)$, the implementation of the $k$-bit multiplier.  Although one
can write $B(k)$ in TLA and translate it to S/R, this is not necessary
because all verification involving $B(k)$ is done with COSPAN, so its TLA
version is not needed.



%try
\section{Decomposition in TLA} \label{sec:decomposition}

We begin with a brief description of TLA; a more complete exposition
appears in~\cite{lamport:newtla}.  We assume an infinite collection of
variables and a suitably large collection of values.  A {\em state\/}
is an assignment of values to variables.  A {\em state function\/} is
an ordinary expression, such as $x+y+1$, built from values and
variables, and a {\em predicate\/} is a Boolean-valued state function,
such as $x>y+1$.  An {\em action\/} is a Boolean-valued expression,
such as $x'>y+1$, containing primed and unprimed variables.  A pair
\tuple{s,\,t} of states satisfies action \act{A} iff (if and only if)
\act{A} is true when unprimed and primed variables are replaced by
their values in $s$ and $t$.  (We let \tuple{\ldots} denote a sequence
or tuple.)  An action represents allowed state transitions---for
example, $x'=x+1$ allows any transition in which the value of $x$ is
incremented by $1$.  We let $v'$ denote the expression obtained by
priming all the variables in the state function $v$---for example
$(x+y+1)'$ equals $x'+y'+1$.  An action \act{A} is {\em enabled\/} in
a state $s$ iff there is some state $t$ such that \tuple{s,\,t}
satisfies~\act{A}.

A {\em behavior\/} is an infinite sequence of states.  A TLA formula
is true or false for a behavior.  We write \valid{F} to denote that
$F$ is true for all behaviors.  A TLA formula $S$ specifies a
system whose correct executions are represented by the behaviors
satisfying $S$.  A system with TLA specification $S$ therefore
satisfies a property $P$ iff $\valid{S\implies P}$.

The basic class of TLA formulas we will use are of the form $I\land
\Box\sqact{N}{v}\land L$, where $I$ is an ``initial state'' predicate,
\act{N} is an action, $v$ is a state function, \sqact{N}{v} denotes
$\act{N}\lor(v'=v)$, and $L$ is a conjunction of formulas of the form
\WF{v}{\act{A}}, defined below.  A behavior satisfies this formula iff
the initial state satisfies $I$, every successive pair of states
satisfies $\sqact{N}{v}$ (representing either an \act{N} transition or
one that leaves $v$ unchanged---a ``stuttering'' step), and the
behavior satisfies~$L$.  A behavior satisfies \WF{v}{\act{A}} iff the
action $\act{A}\land(v'\neq v)$ is satisfied by infinitely many pairs
of successive states, or is disabled in infinitely many states of the
behavior.

Another class of TLA formulas we use have the form $\Box P$, where $P$
is a predicate.  Such a formula is true for a behavior iff $P$ is true
for every state of the behavior.  We also use the TLA operator \EE,
where $\EE\,x:F$ essentially denotes the formula $F$ with $x$
``hidden''.  The precise definition of \EE\ can be found in
\cite{lamport:newtla}.

A finite sequence $\rho$ of states is said to satisfy a TLA formula
$F$ iff $\rho$ is the prefix of a behavior that satisfies
$F$.\footnote{Since TLA formulas are invariant under
stuttering~\cite{lamport:what-good}, the definition of safety that
follows would be the same had we defined $\rho$ to satisfy $F$ iff the
behavior obtained by repeating the last state of $\rho$ satisfies
$F$.} A formula $F$ is said to be a {\em safety property\/} iff the
following condition is satisfied: if every finite prefix of $\sigma$
satisfies $F$, then $\sigma$ satisfies $F$.  The closure \closure{F}
of a formula $F$ is the strongest safety property (conjunction of all
such properties) implied by $F$.  If $L$ is the conjunction of
formulas of the form \WF{v}{\act{A}} where each \act{A} implies
\act{N}, then
\begin{equation}\label{eq:machine-closure}
\closure{I\land\Box\sqact{N}{v}\land L} \;\equiv\; I\land \Box\sqact{N}{v}
\end{equation}
In particular, $I\land\Box\sqact{N}{v}$ is a safety property.  For any
predicate $P$, the formula $\Box P$ is also a safety property.


For any safety property $E$, we define \plus{E} to be the property
that is true ``one step longer than'' $E$ is.  In other words, a
finite sequence of states $\rho$ of length $n$ satisfies \plus{E} iff
either $n=1$, or $n>1$ and the prefix of $\rho$ of length $n-1$
satisfies $E$.  An infinite behavior satisfies \plus{E} iff it
satisfies $E$ or has the form
\tuple{s_{0},\ldots,s_{n},\,s_{n},\,s_{n},\ldots}, where $n=0$ or
\tuple{s_{0},\ldots,s_{n-1}} satisfies $E$.  In general, \plus{E} is
not expressible with the TLA operators $'$, $\Box$, and \EE. For
example, \plus{\vbl{false}} is the conjunction of the formulas
$\Box\sqact{{}\vbl{false}}{x}$ for all variables $x$, and such
an infinite conjunction cannot be expressed in TLA\@.
However,
formulas of the form \plus{E} occur only in hypotheses of the form
\valid{\plus{E}\land P\implies Q}, which can be verified by
substituting for \plus{E} a ``conservative approximation''
$\widetilde{E}$ satisfying \valid{\plus{E}\implies\widetilde{E}}.  A
suitable approximation is obtained by applying
\begin{equation} \label{eq:def-plus}
\valid{\plus{(I \,\land\,\Box\sqact{N}{v})}}
\;\;\implies\;\;
 \EE\,s : 
     \widetilde{I} \;\land\;
     \Box\sqact{{}\widetilde{\act{N}}}{\tuple{s,\,v}}
\end{equation}
where $s$ is a variable that does not occur in $I$, \act{N}, or $v$,
and 
 \[ \begin{array}{@{}l@{\;\;\deq\;\;}l@{}}
    \widetilde{I} &   
      (I\land(s=0) )\,\lor\,(\lnot I\land(s=1))\\[\jot]
    \widetilde{\act{N}} &
     (s=0)\;\,\land\;\,
      (\,(\act{N}\land(s'=s)) \,\lor\,
       (\lnot\act{N}\land(s'=1))\,)
   \end{array}  \vspace{-.4\baselineskip}%%%%%%%%%%%%%%%%
\]
(The symbol $\deq$ means {\em equals by definition}.)  


The key to verifying a complex system is decomposing the proof.  In
TLA, a system is decomposed into components by writing its
specification as the conjunction of its components' specifications.
We represent a system composed of $n$ components by a TLA formula
$E\land B_{1}\land\ldots\land B_{n}$, where $E$ is the environment
specification and $B_{i}$ is the specification of the $i$th component.
We consider only the case of $E$ a safety property.  Our problem is to
prove that, in the presence of a properly functioning environment, the
system satisfies some property $F$. This requires proving
 \valid{E\land B_{1}\land\ldots\land B_{n}\,\implies\,F}.  
We do this by writing a high-level specification $M_{i}$ for each
component $i$, and proving\footnote{In general, one might want to
   replace $E$ by a more abstract environment specification in
   (\ref{eq:refine1}) and in the conclusion of (\ref{eq:refine2}).  This
   generalization is not needed in our example.}
\begin{eqnarray}
& \valid{E\land M_{1}\land\ldots\land M_{n}\;\implies\;F }
  \label{eq:refine1}\\
& \valid{E\land B_{1}\land\ldots\land B_{n}\;\implies\;
  E\land M_{1}\land\ldots\land M_{n}} \label{eq:refine2}
\end{eqnarray}
We prove (\ref{eq:refine1}) by standard TLA reasoning---that is, by
theorem proving.  To prove (\ref{eq:refine2}), we use the
following theorem, which is proved in \cite{abadi:open}.
\begin{trivlist}\item[] \bf Decomposition Theorem \ \it
If $E$ is a safety property and, for $i=1,\ldots\,, n$,
\vspace{-.25\baselineskip}
\begin{enumerate}
\item $E_{i}$ is a safety property.\vspace{\jot}
%
\item \valid{E\land\closure{M_{1}}\land\ldots\land\closure{M_{n}}
      \;\implies\;E_{i}}\vspace{\jot}
%
\item \begin{enumerate}
  \item \valid{E_{i}\land B_{i} \;\implies\; M_{i}}\vspace{.75\jot}
  \item \valid{\plus{E_{i}}\land \closure{B_{i}} \;\implies\; \closure{M_{i}}}
   \end{enumerate}
%
\vspace{\jot}
\item \valid{\closure{M_{1}}\land\ldots\land\closure{M_{n}}\;\equiv\;
             \closure{M_{1}\land\ldots\land M_{n}}}
\end{enumerate}
\vspace{-.15\baselineskip}
%
then \begin{tabular}[t]{@{}l@{ \,}l}
(a) & \valid{E\land B_{1}\land\ldots\land B_{n}\;\implies\;
M_{1}\land\ldots\land M_{n}}, and\\[\jot]
(b) &  \valid{\plus{E}\land \closure{B_{1}\land\ldots\land B_{n}}\;\implies\;
  \closure{M_{1}\land\ldots\land M_{n}}}.
\end{tabular}
\end{trivlist}
Conclusion (a) provides the desired result (\ref{eq:refine2}).
Conclusions (a) and (b) have the same form as hypotheses 3(a) and
3(b);  as we shall see, this permits recursive application of the
theorem.

To apply the Decomposition Theorem, we choose $E_{i}$ to be an
abstract specification of the $i$th component's environment.  The
second hypothesis asserts that $E_{i}$ is implemented by the
composition of the safety properties of the high-level specifications
$M_{i}$ and their environment.  The third hypothesis essentially
asserts that the composition of the low-level specification and its
environment implements the high-level specification.  The fourth
hypothesis is a technical requirement; conclusion (a) remains valid
even if this hypothesis is not satisfied.

In a simple application of the theorem, the three hypotheses are
proved as follows.  The first hypothesis will follow immediately from
(\ref{eq:machine-closure}) and the form of $E$.  The second hypothesis
will be proved by standard TLA reasoning---that is, by theorem
proving, using TLP\@.  The third hypothesis will be proved by model
checking, using COSPAN\@.  The fourth hypothesis is checked with
(\ref{eq:machine-closure}).  Because our multiplier is defined
recursively, it will be verified by recursive application of the
Decomposition Theorem.  As explained in Section~\ref{sec:proof} below,
model checking is needed only for the base-case application of the
theorem.  

Theorem proving is applied only to the specifications $E$, $E_{i}$ and
$M_{i}$.  The specifications $E$ and $E_{i}$ are abstractions of the
environment, describing only as much of the environment's behavior as
is necessary to ensure correct operation of the system or the
individual component.  The specification $M_{i}$ is a high-level
abstraction.  Hence, we are proving theorems only about relatively
simple specifications.  All reasoning about $B_{i}$, the detailed
specification of the component, is done with model checking.  Thus, we
need not even write the TLA formula $B_{i}$.  We translate the TLA
formulas $E_{i}$, $M_{i}$, \closure{M_{i}}, and the approximation to
\plus{E_{i}} into S/R, the language of the COSPAN model checker, and
use COSPAN to verify the S/R formulas corresponding to the TLA
formulas of hypothesis~3.

Note that the Decomposition Theorem would be false if \plus{E_{i}}
were replaced by $E_{i}$ in hypothesis~3(b).  For example, with this
change, the hypotheses would be satisfied by letting all the $E_{i}$
and $M_{i}$ be false, and conclusion (a) would assert
\valid{\lnot(E\land B_{1}\land\ldots\land B_{n})} for arbitrary $E$
and $B_{i}$.  It is trivial to infer the refinement relation
(\ref{eq:refine2}) from \valid{B_{i}\implies M_{i}} for each $i$.
However, in systems such as the multiplier, which have a high degree
of global coordination among components, \valid{B_{i}\implies M_{i}}
is almost never true; in these systems, one can generally prove little
about the behavior of a component $B_{i}$ without knowing something
about the behavior of its environment $E_{i}$.

%try


\section{The Specification of the Multiplier}

We write the specification in a formal language based on TLA 
containing operators for defining data structures; language structures
for making declarations, definitions, and assumptions; and a module
mechanism for encapsulating names and performing renaming.  This
language, which can be translated into S/R, is a subset of a more
general specification language under development called
\TLA+~\cite{lamport:hybrid}.

We assume some conventional mathematical notation for numbers and
sets.  We write $f[x]$ for the application of a function $f$ to a
value $x$ in its domain, and we let $[S\rightarrow T]$ denote the set of
all functions with domain $S$ and range a subset of $T$.  Functions
are explicitly defined with expressions of the form 
 $[x\in S\mapsto e(x)]$, 
which denotes the function $f$ with domain $S$ such that $f[x]=e(x)$
for all $x\in S$.

We define $\vbl{BitVector}(i)$ to be the set of all $i$-bit-wide bit
vectors and $\vbl{Val}(i,\, v)$ to be the value of the $i$-bit vector
$v$ interpreted as a binary number.  They are defined formally as
follows.
%, where $\deq$ means {\em equals by definition.}
 \[ \begin{array}{@{}l@{\;\;\;\deq\;\;\;}l@{}}
      \vbl{BitVector}(i) & [\{0,\, \ldots\,, i-1\} \rightarrow \{0,\,1\}]
    \\[\jot]
      \vbl{Val}(i,\, v) & \sum\limits_{j=0}^{i-1}v[j] \cdot 2^j
     \end{array}
 \]
We let $\vbl{Multiply}(i,\,v,\,w)$ denote the $2i$-bit vector obtained
by multiplying the $i$-bit vectors $v$ and $w$.  Formally,
$\vbl{Multiply}$ is defined by the following axiom, where \vbl{Nat}
denotes the set of natural numbers.  (A list bulleted by $\land$ 
denotes the conjunction of the items.)
 \[ \begin{array}{@{}l@{}}
    \forall\, i \in \vbl{Nat} : \forall\, v,\, w 
        \in \vbl{Bitvector}(i) :\\[.5\jot]
    \s{1}\begin{conj}
          \vbl{Multiply}(i, v, w) \in \vbl{BitVector}(2i)
              \\[.5\jot]              
          \vbl{Val}(2i,\, \vbl{Multiply}(i,\, v,\, w)) 
              = \vbl{Val}(i,\, v) \cdot \vbl{Val}(i,\, w)
      \end{conj}
   \end{array}  
 \]

We specify an asynchronous multiplier circuit with inputs $a$ and $x$
and output \vbl{out} that synchronizes with its environment using a
two-phase handshaking protocol
%~\cite{seitz:system-timing} 
on the bits \vbl{sig} and \vbl{ack}.  The environment can change the
inputs when $\vbl{sig}=\vbl{ack}$; it complements \vbl{sig} when the
inputs are ready.  The multiplier can change the output when
$\vbl{sig}\neq\vbl{ack}$; it complements \vbl{ack} when the output is
ready.  Initially, \vbl{sig} and \vbl{ack} equal $0$ and the
multiplier is ready to receive input.  The TLA formulas $M$ specifying
the multiplier and $E$ specifying its environment are defined in the
\vbl{Mult} module of Figure~\ref{fig:Mult}.  
\begin{figure}[tp]
\small
\begin{module}{Mult}
\begin{decls}{parameters}
  $a$, $x$, \vbl{out}, \vbl{sig}, \vbl{ack} : {\bf variables}\\
  $N$ : \vbl{Nat} {\bf constant}
\end{decls}
\midbar
\begin{decls}{predicates}
\vbl{MInit} \= \defeq\ $(\vbl{out} \in \vbl{BitVector}(2*N)) \;\land\; 
                    (\vbl{ack} = 0)$\\
%
\vbl{EInit} \> \defeq\ $(a \in \vbl{BitVector}(N)) 
                          \;\land\; (x \in \vbl{BitVector}(N))
                          \;\land\; (\vbl{sig} = 0)$ 
\end{decls}
%
\begin{decls}{actions}
\vbl{Think} \= \defeq\ $\begin{conj}
                        \vbl{sig} \neq \vbl{ack}\\
                        \vbl{ack}' = \vbl{ack}\\
                        \vbl{out}' \in \vbl{BitVector}(2*N)
                     \end{conj}$ \\
\vbl{Finish} \> \defeq\  $\begin{conj}
                         \vbl{sig} \neq \vbl{ack}\\
                         \vbl{ack}' = 1 - \vbl{ack}\\
                         \vbl{out}' =  \vbl{Multiply}(N,\, a,\, x)
                      \end{conj}$\\
\vbl{MNext} \> \defeq\ $\vbl{Think} \lor \vbl{Finish}$\\
\vbl{ENext} \> \defeq\  
  $\begin{conj}
       \vbl{sig} = \vbl{ack}\\
       \vbl{sig}' \in \{0,\,1\}\\
       (a' \in \vbl{BitVector}(N)) \;\land\; (x' \in \vbl{BitVector}(N))
       \vs{.5}
   \end{conj}$
\end{decls}
%
\begin{decls}{temporal formulas}
  $M$ \= \defeq\  $\vbl{MInit} \;\land\; 
                 \Box\sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\, \vbl{ack}}}
                     \;\land\; 
                 \WF{\tuple{\vbl{out},\, \vbl{ack}}}{\vbl{Finish}}$\\[.1em]
  $E$ \> \defeq\  
         $\vbl{EInit} \;\land\;
         \Box\sqact{{}\vbl{ENext}}{\tuple{a,\,x,\,\vbl{sig}}}$
\end{decls}
\end{module}
\vspace{-\baselineskip}
\caption{TLA specifications of an $N$-bit multiplier and its environment.
The multiplier's $2N$-bit output \vbl{out} is the product of its
$N$-bit inputs $a$ and $x$.  The variables \vbl{sig} and
\vbl{ack} are used for synchronization.}
\label{fig:Mult}
\end{figure}
The \kwd{PARAMETERS}
section declares all the variables and unspecified constants that may
appear in the module.  The declaration of $N$ asserts the assumption
that $N$ is an element of \vbl{Nat}.  The initial conditions on the
outputs are in \vbl{MInit}, and the initial conditions on the inputs
are in \vbl{EInit}.  A simple logical calculation shows that the
formula $E\land M$ that describes the system consisting of the
multiplier and its environment equals
 \[ (\vbl{MInit} \land \vbl{EInit})
       \;\land\; 
     \Box\sqact{\relax\vbl{MNext} 
         \lor \vbl{ENext}}{v}
       \;\land\; \WF{v}{\vbl{Finish}}
 \]
where $v$ denotes the 5-tuple
\tuple{a,\,x,\,\vbl{sig},\,\vbl{out},\,\vbl{ack}}. Hence, the system has
the expected TLA specification.


\begin{figure}[tp]
\small
\begin{module}{DblMult}
\begin{decls}{parameters}
  $a$, $x$, \vbl{out}, \vbl{sig}, \vbl{ack}, \vbl{outLL}, \vbl{outLH}, 
     \vbl{outHL}, \vbl{outHH},\\
\s{2} \vbl{ackLL}, \vbl{ackLH}, \vbl{ackHL}, 
     \vbl{ackHH} : {\bf variables}\\
  $N$ : \vbl{Nat}
\end{decls}
\midbar
\begin{decls}{state functions}
  \vbl{aH} \= \defeq\ $[i \in \{0,\, \ldots , N-1\} \mapsto a[i+N]\, ]$\\
  \vbl{aL} \> \defeq\ $[i \in \{0,\, \ldots , N-1\} \mapsto a[i]\,   ]$\\
  \vbl{xH} \> \defeq\ $[i \in \{0,\, \ldots , N-1\} \mapsto x[i+N]\, ]$\\
  \vbl{xL} \> \defeq\ $[i \in \{0,\, \ldots , N-1\} \mapsto x[i]\,   ]$\\
  \vbl{acks} \defeq\ \tuple
          {\vbl{ack},\,\vbl{ackLL},\,\vbl{ackLH},\,
            \vbl{ackHL},\,\vbl{ackHH}}
   \vs{.75}
\end{decls}
\newlength{\templen}
\settowidth{\templen}{{\bf include} \vbl{Mult} {\bf as} \vbl{HH}}
\mbox{\makebox[\templen][l]{{\bf include} \vbl{Mult} {\bf as} \vbl{LL}}
       {\bf with} $a         \leftarrow \vbl{aL},\, 
                   x         \leftarrow \vbl{xL},\, 
                   \vbl{out} \leftarrow \vbl{outLL},\, 
                   \vbl{ack} \leftarrow \vbl{ackLL}$}\\
%
\mbox{\makebox[\templen][l]{{\bf include} \vbl{Mult} {\bf as} \vbl{LH}}
      {\bf with} $a         \leftarrow \vbl{aL},\, 
                 x         \leftarrow \vbl{xH},\, 
                 \vbl{out} \leftarrow \vbl{outLH},\, 
                 \vbl{ack} \leftarrow \vbl{ackLH}$}\\
%
\mbox{\makebox[\templen][l]{{\bf include} \vbl{Mult} {\bf as} \vbl{HL}}
      {\bf with} $a         \leftarrow \vbl{aH},\, 
                  x         \leftarrow \vbl{xL},\, 
                  \vbl{out} \leftarrow \vbl{outHL},\, 
                  \vbl{ack} \leftarrow \vbl{ackHL}$}\\
%
\mbox{\makebox[\templen][l]{{\bf include} \vbl{Mult} {\bf as} \vbl{HH}}
{\bf with} $a        \leftarrow aH,\, 
                   x        \leftarrow xH,\, 
                  \vbl{out} \leftarrow \vbl{outHH},\, 
                  \vbl{ack} \leftarrow \vbl{ackHH}$}\\
%
\makebox[\templen][l]{{\bf include} \vbl{Mult} {\bf as} \vbl{Dbl}} 
         {\bf with} $N \leftarrow 2*N$\\[.3em]
%
\begin{decls}{actions}
\vbl{AckNext} \defeq\ $\vbl{ack}'$ = 
 {\bf if} \= $(\vbl{ackLL} = \vbl{sig}) \;\land\; 
                (\vbl{ackLH} = \vbl{sig})$\\
   \>\s{1}$\mbox{}\;\land\; (\vbl{ackHL} = \vbl{sig}) 
                \;\land\; (\vbl{ackHH} = \vbl{sig})$\\
   \> {\bf then} \= \vbl{sig}\\
   \> {\bf else} \> $1 - \vbl{sig}$
\end{decls}
%
\begin{decls}{temporal formulas}
\vbl{ExtAck} \defeq\ $(\vbl{ack}=0)\;\land\;
         \Box\sqact{{}\vbl{AckNext}}{\vbl{acks}}
         \;\land\; \WF{\vbl{acks}}{\vbl{AckNext}}$\\
%
\vbl{Adder} \defeq\ $\Box\;
    \begin{conj}
      \vbl{out} \in \vbl{BitVector}(4*N)\\
        \vbl{Val}(4*N,\, \vbl{out}) = 
       \begin{array}[t]{@{}l@{}l@{}}
         (2^{2*N} * \vbl{Val}(2*N,\, \vbl{outHH})    \\
          \s{.5} +\; 2^N   * (\vbl{Val}(2*N,\, \vbl{outLH})  \\
          \s{4.5} +\; \vbl{Val}(2*N,\,\vbl{outHL}))           \\
          \s{.5} +\; \vbl{Val}(2*N,\, \vbl{outLL}) & )\bmod 2^{4*N}
       \end{array}
     \end{conj}$\\
%
\vbl{DM} \= \defeq\  
             $\vbl{LL.M} \;\land\; \vbl{LH.M} \;\land\; \vbl{HL.M} \;\land\; 
                   \vbl{HH.M} \;\land\; \vbl{ExtAck}\;\land\; \vbl{Adder}$\\
%
\vbl{DE} \> \defeq\  \vbl{Dbl.E}
\end{decls}
\end{module}
\vspace{-\baselineskip} 
\caption{Specification of the $2N$-bit
multiplier and its environment.  Four copies of the $N$-bit
multiplier, operating on half of each input value, are composed, and
their outputs combined to form the output.} 
\label{fig:DblMult}
\end{figure}


Figure~\ref{fig:DblMult} contains the module \vbl{DblMult}, which
defines the specification \vbl{DM} of a $2N$-bit multiplier
implemented with four ``internal'' $N$-bit multipliers and a
combinational four-input adder, and defines the specification \vbl{DE} of its
environment.  The implementation is based on the observation that if
$a=2^{N}\cdot\vbl{aH}+\vbl{aL}$ and $x=2^{N}\cdot\vbl{xH}+\vbl{xL}$, then
 \[ a\cdot x \;=\; 2^{2N}\cdot(\vbl{aH}\cdot\vbl{xH})
                   + 2^{N}\cdot((\vbl{aH}\cdot\vbl{xL}) + 
                                   (\vbl{aL}\cdot\vbl{xH}))
                   + (\vbl{aL}\cdot\vbl{xL})
 \]
The four multiplications are performed by four copies of the $N$-bit
multiplier named \vbl{HH}, \vbl{LH}, \vbl{HL}, and \vbl{LL}.  The
external inputs and outputs of the $2N$-bit multiplier are given the
same names as in the $N$-bit multiplier.  The variables \vbl{outHH},
\ldots, \vbl{ackLL} represent ``internal wires'' that hold the outputs
and \vbl{ack}'s of the four multipliers.  The four multipliers'
\vbl{sig} inputs are taken from the external \vbl{sig} input, and
their $a$ and $x$ inputs are the appropriate $N$-bit subvectors
\vbl{aH}, \vbl{aL}, \vbl{xH}, and \vbl{xL} of the external $a$ and $x$
inputs. 

The first \kwd{INCLUDE} statement effectively defines the \vbl{LL}
multiplier.  Formally, it includes a copy of all the definitions from
the \vbl{Mult} module, with the indicated substitutions for the
parameters, and with the name of the defined symbols changed by
prefacing them with ``\vbl{LL.}''.  Thus the statement adds the
following definition, among others, to module \vbl{DblMult}.
 \[
     \vbl{LL.MInit} \defeq (\vbl{outLL} \in \vbl{BitVector}(2*N))
                    \,\land\, (\vbl{ackLL} = 0)
 \]
The next three \kwd{INCLUDE} statements similarly include the other
three needed copies of the $N$-bit multiplier, and the fourth one
includes the definition of \vbl{Dbl.E}, the specification
of a $2N$-bit multiplier's environment.

The temporal formula \vbl{ExtAck} has the usual form for a
specification of a simple component that takes as input the
multipliers' \vbl{ack} outputs and the external \vbl{sig} input and
generates the external \vbl{ack} output.

The formula \vbl{Adder} specifies the adder.  It has the form $\Box
P$, where $P$ describes the appropriate relation between the adder's
output \vbl{out} and its four inputs, which are the outputs of the
internal multipliers.  The specification is so simple because we are
assuming a combinational adder, whose output is always a function of
its inputs.  In a real multiplier, the addition would be performed by
a separate sequential component.  We have used a combinational circuit
both for simplicity and to illustrate how to represent such circuits.
(The combinational adder makes our implementation so simple that it
could be verified without the Decomposition Theorem.  However, the
theorem would be needed to verify a more realistic implementation in
which a send/acknowledgement protocol is used to transmit the outputs
of the component multipliers to a sequential adder.)


Finally, the specification \vbl{DM} of the $2N$-bit multiplier is
defined to be the conjunction of the specification of its components,
and the specification \vbl{DE} of its environment is defined to be
\vbl{Dbl.E}.  


%try
\section{Translation into S/R}

COSPAN is used to verify hypothesis~3 of the Decomposition Theorem.
This requires S/R versions of $E$, an approximation to \plus{E}, $M$,
\closure{M}, $B(k)$ and \closure{B(k)}, where $B(k)$ is a
specification of the low-level $k$-bit multiplier.  These S/R
specifications could all be obtained by translating TLA formulas.
However, the TLA versions of $B(k)$ and \closure{B(k)} are not needed.
The specification $B(k)$ of the low-level multiplier can be written
directly in S/R\@.  We describe below how the S/R version of
\closure{B(k)} is constructed from the S/R version of $B(k)$.  The S/R
versions of the remaining formulas can be obtained by translation.

Since circuits are synthesized from their S/R specifications, our
translation must guarantee that whatever we prove about a TLA
specification is valid for its S/R translation.  The TLA theorems we
prove have the form \valid{F\implies G} for formulas $F$ and $G$.  Let
\xlate{F} denote the S/R translation of the TLA formula $F$.
Correctness of the translation means that the TLA theorem
\valid{F\implies G} implies the S/R theorem
$\lang{\xlate{F}}\subseteq\lang{\xlate{G}}$, where $\lang{S}$ denotes
the language of the S/R specification $S$.

In S/R, declaring the type of a variable guarantees that the
variable's value is always of that type.  Hence, to infer the validity
of $\lang{\xlate{F}}\subseteq\lang{\xlate{G}}$, it suffices to prove
\valid{F\implies G} assuming type correctness.  This means that we
need only prove \valid{F\land\Box T\,\implies\, G}, where $T$ is the
predicate asserting that the values of all variables have the type
declared in the S/R specification.  All the TLA proof obligations can
thus be weakened by adding the hypothesis $\Box T$.  However, this
hypothesis should not be needed, because a TLA specification should
imply type correctness.

% In S/R, declaring the type of a variable guarantees that the
% variable's values is always of that type.  TLA is untyped; it has
% no type declarations.  In order to deduce the validity of
% $\lang{\xlate{F}}\subseteq\lang{\xlate{G}}$ from 
% \valid{F\implies G}, we must prove
% the TLA theorem \valid{F\implies\Box T}, where $T$ is the predicate
% asserting that the values of all variables appearing in F have the
% correct type.  Such a theorem is generally proved in the course of
% proving \valid{F\implies G}, so this requirement does not introduce a
% new proof step.  

The S/R translation of $M$ appears in Figure~\ref{fig:S/R-M}.  
\begin{figure}[tbp]
\begin{small}
\begin{tabbing}
\srkwd{proctype} M(N : integer; \ a, x : (0 .. 2\verb|^|N-1) ; \ sig : (0, 1))\\
\s{1}\=\+\kill
  \srkwd{import} a, x, sig\\
  \srkwd{locvar} choose : (1, 2, 3) 
           \s{1}\srcomk{encodes \sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\,
                 \vbl{ack}}} choices} \kill
%
  \srkwd{locvar} choose : (1, 2, 3)  \srcom{encodes \sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\, \vbl{ack}}} choices} \\
  \s{.5}\srkwd{asgn} choose := \{1, 2, 3\} 
         \srcom{makes nondeterministic choice}\\
%
  \srkwd{stvar}  ack : (0, 1)         \srcom{ack of output variables}\\
  \srkwd{stvar}  out[2$*$N] : (0, 1)  \srcom{output variables }\\
%  \srkwd{stvar}  sig : (0, 1)         \srcom{signal of input variables}\\
%  \srkwd{stvar}  a[2$*$N] : (0, 1)    \srcom{variables of 1st input}\\
%  \srkwd{stvar}  x[2$*$N] : (0, 1)    \srcom{variables of 2nd input}\\
  \srkwd{stvar}  finish : (0, 1)      
      \srcom{variable to express fairness}\-\\[.2em]
\pushtabs\srcomk{initial conditions}\poptabs\+\\
  \srkwd{init}  ack := 0\\
  \srkwd{init} [i in 0\,.\,.\,2$*$N$-$1]\{ out[i] := \{0, 1\} \}\\
  \srkwd{init} finish := 0 \-\\[.2em]
\pushtabs\srcomk{next-state relation}\poptabs\+\\
  \srkwd{asgn} ack $\rightarrow$\s{1}\=  
                     1 $-$ ack \= ? (choose = 1)$*$(sig $\neq$ ack)\kill
  \srkwd{asgn} ack $\rightarrow$\s{1}\=  
                     ack \> ? (choose = 1) $*$ (sig $\neq$ ack)\\
              \> $|$\' 1 $-$ ack \> ? (choose = 2) $*$ (sig $\neq$ ack)  \\
              \> $|$\' ack \\
%
  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ 
    out[i] $\rightarrow$\s{1}\=   mul[i] \=
                ? (choose = 1)$*$(sig $\neq$ ack) \kill
%
  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ 
    out[i] $\rightarrow$\s{1}\= \{0, 1\}  
                \> ? (choose = 1) $*$ (sig $\neq$ ack) \\
                  \> $|$\' mul[i] \> ? (choose = 2) $*$ (sig $\neq$ ack) \= \\
                  \> $|$\' out[i] \>                                   \> \} \\
%  \srkwd{asgn} sig $\rightarrow$  sig ? 
%                       ($\sim$(choose = 3)) $*$ (sig $\neq$ ack)
%             $|$ \{0, 1\} \\
%  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ 
%          a[i] $\rightarrow$
%                  a[i] ? ($\sim$(choose = 3)) $*$ (sig $\neq$ ack) 
%         $|$ \{0, 1\} \}\\
%  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ 
%    x[i] $\rightarrow$ x[i] ? 
%               ($\sim$(choose = 3)) $*$ (sig $\neq$ ack)
%         $|$ \{0, 1\} \}\\
  \srkwd{asgn} finish $\rightarrow$
                       1 ? (sig $\neq$ ack) $*$ (choose $=$ 2)
             $|$ 0 \-\\[.2em]
\pushtabs
\srcomk{implementation of ``call'' of Multiply in next-state relation}%
\poptabs\+\\
  \srkwd{locvar} mul[2$*$N] : (0, 1)\\
  \s{.5}\srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ mul[i] := \{0, 1\} \}\\
  \srkwd{proc} K : KILL( $\sim$( \= +[i in 0\,.\,.\,2$*$N$-$1](mul[i]$\,*\,$2\verb|^|i) = \\
                    \> \s{1}+[i in 0\,.\,.\,N$-$1](a[i]$\,*\,$2\verb|^|i) $*$ 
                    (+[i in 0\,.\,.\,N$-$1](x[i]$\,*\,$2\verb|^|i))))\-\\
\pushtabs\srcomk{fairness}\poptabs\+\\
  \srkwd{cyset} \{ finish := 0 \}\-\\
 \srkwd{end} M()
\end{tabbing}
\vspace{-\baselineskip} %%% fix vertical spacing problem
\end{small}
\caption{The S/R translation of the TLA formula $M$.}
\label{fig:S/R-M}
\end{figure}
A {\bf
stvar} declaration defines a state variable, which is initialized by
an {\bf init} declaration and assigned values by an {\bf asgn}
declaration.  (The $\rightarrow$ indicates that the value is assumed
in the next step.)  A {\bf locvar} declaration defines a local
(internal) combinational variable, which also is assigned values by an {\bf
asgn}.  (The $:=$ indicates that the value is assumed in the
current step, so no initialization is needed.)  Assigning a set of
values denotes nondeterministic choice, and the expression
\mbox{$e_{1}\,?\,b\,|\,e_{2}$} equals $e_{1}$ if $b$ is true, else
$e_{2}$.  The {\bf cyset} declaration asserts a fairness constraint,
removing all behaviors that eventually remain within the declared set.
The ``\mbox{{\bf proc} K : KILL($p$)}'' statement eliminates all
behaviors that satisfy $p$.

The S/R version of $M$ is obtained from the TLA formula as follows.
The initial predicate \vbl{MInit} yields the {\bf init} statements for
\vbl{ack} and \vbl{out}.  The formula
$\Box\sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\, \vbl{ack}}}$ yields the
{\bf asgn} statements for \vbl{ack} and \vbl{out}.  The nondeterminism
expressed in TLA by writing the next-state relation as a disjunction
is expressed in S/R by introducing a variable \vbl{choose} with as
many values as there are disjuncts.  In the S/R translation of $M$,
the correspondence between values of \vbl{choose} and disjuncts
of \sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\, \vbl{ack}}} is:
 \[ \begin{array}{@{}l@{\;\;\implies\;\;}l@{}}
     (\vbl{choose} = 1) & \vbl{Think}\\
     (\vbl{choose} = 2) & \vbl{Finish}\\
     (\vbl{choose} = 3) & 
          \tuple{\vbl{ack},\,\vbl{out}}'=\tuple{\vbl{ack},\,\vbl{out}}
    \end{array}
\] 
A TLA fairness condition is expressed by adding a variable to record
that the action has occurred and a {\bf cyset} statement to require
its occurrence.  The TLA formula
\WF{\tuple{\vbl{out},\,\vbl{ack}}}{\vbl{Finish}} is represented by the
variable \vbl{finish} and the {\bf cyset} statement.

It follows from (\ref{eq:machine-closure}) that \closure{M} equals
 $\vbl{MInit}\,\land\,\Box\sqact{{}\vbl{MNext}}{\tuple{\vbl{out},\,\vbl{ack}}}$,
so its S/R translation is the same as that of $M$, except with the
{\bf cyset} declaration removed.  This can be deduced directly from
the following result: if, in the state-transition graph, there is an
exit from the set of states defined by each cyset declaration, then
the closure of an S/R specification can be obtained by removing its
{\bf cyset} declarations.  This result allows us to obtain the closure
\closure{B(k)} of a low-level $k$-bit multiplier specification
$B(k)$ written directly in S/R.

The S/R translation of TLA formula $E$ is similar to that of $M$; it
appears in Figure~\ref{fig:S/R-E}.  The translations of \vbl{ExtAck} 
and \vbl{Adder} are straightforward and are omitted.  The S/R version
of the approximation to \plus{E} can be obtained by translating the
TLA formula computed with (\ref{eq:def-plus}).  It can also be
obtained directly from the S/R translation of $E$.




\begin{figure}[t]
\begin{small}
\begin{tabbing}
\srkwd{proctype} E(N : integer; \ out : (0 .. 2\verb|^|(2*N)-1) ; 
   \ ack : (0, 1) )\\
\s{1}\=\+\kill
  \srkwd{import} out, ack\\
  \srkwd{stvar} lastchoice : (1, 2, 3) 
              \s{1}\srcomk{\s{.5}makes non-deterministic choice}\kill
  \srkwd{locvar} choose : (1, 2)      
     \srcom{encodes \sqact{{}\vbl{ENext}}{\tuple{a,\,x,\,\vbl{sig}}} choices}\\
%
  \s{.5}\srkwd{asgn} choose := \{1, 2\}   
       \s{1}\srcom{\s{.5}makes non-deterministic choice}\\
%  \srkwd{stvar} ack : (0, 1)          \srcom{ack of output variables}\\
%  \srkwd{stvar} out[2$*$N] : (0, 1)   \srcom{output variables}\\
  \srkwd{stvar} sig : (0, 1)          \srcom{signal of input variables}\\
  \srkwd{stvar} a[2$*$N] : (0, 1)     \srcom{variables of 1st input}\\
  \srkwd{stvar} x[2$*$N] : (0, 1)     \srcom{variables of 2nd input}\-\\[.2em]
%  \srkwd{stvar} lastchoice : (1, 2, 3) 
%              \srcom{holds {\rm choose} for 1 cycle}\\
%  \srkwd{stvar} lastack : (0, 1)        \srcom{holds {\rm ack} for 1 cycle}\\
%  \srkwd{stvar} lastout[2$*$N] : (0, 1)   
%                      \srcom{holds {\rm out} for 1 cycle}\-\\[.2em]
\pushtabs\srcomk{initial conditions}\poptabs\+\\
  \srkwd{init} sig := 0\\
  \srkwd{init} [i in 0\,.\,.\,2$*$N$-$1]\{a[i] := \{0, 1\}\}\\
  \srkwd{init} [i in 0\,.\,.\,2$*$N$-$1]\{x[i] := \{0, 1\}\}\-\\[.2em]
\pushtabs\srcomk{next-state relation}\poptabs\+\\
%  \srkwd{asgn} lastchoice $\rightarrow$ choose\\
%  \srkwd{asgn} lastack $\rightarrow$ ack\\
%  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{ lastout[i] $\rightarrow$ out[i] \}\\
  \srkwd{asgn} sig $\rightarrow$\s{1}\=  \{0, 1\} \= 
                   ? (choose = 1) $*$ (sig = ack)  % \\ \> 
             $|$ %\' 
         \{sig\}\\
  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{
        a[i] $\rightarrow$\s{1}\=\{0, 1\} ? 
                               (choose = 1) $*$ (sig = ack) %\\ \>     
        $|$ %\' 
          \{a[i]\} \}\\
  \srkwd{asgn} [i in 0\,.\,.\,2$*$N$-$1]\{   
       x[i] $\rightarrow$\s{1}\= \{0, 1\} ? (choose = 1) $*$ (sig = ack) \= 
         %\\ \> 
      $|$ %\' 
         \{x[i]\} %\> 
     \}\\
%  \srkwd{asgn} ack $\rightarrow$ \{0, 1\} ? (choose = 1) $|$ \{ack\}\\
%  \srkwd{asgn} \= [i in 0\,.\,.\,2$*$N$-$1]\{ 
%      out[i] $\rightarrow$ \{0, 1\} ? (choose = 1) $|$ \{out[i]\} \}\\
%
%  \srkwd{proc} K : KILL (\= (lastchoice = 1) $*$ (lastack = ack)\\
%       \>\s{1}$*$ (+[i in 0\,.\,.\,2$*$N$-$1] (lastout[i] = out[i])))\-\\
\srkwd{end} E()
\end{tabbing}
\vspace{-\baselineskip} %%% fix vertical spacing problem
\end{small}
\caption{S/R translation of the TLA formula $E$.}
\label{fig:S/R-E}
\end{figure}

The TLA to S/R translator will have to include directives for
instantiating parameters and subformulas.  For example, the S/R
specification of a $2k$-bit multiplier is obtained from the
translation of the formula \vbl{DM} from the \vbl{DblMult} module by
substituting $k$ for $N$ and substituting copies of the S/R
specification $B(k)$ of a $k$-bit multiplier for \vbl{LL.M},
\vbl{LH.M}, \vbl{HL.M}, and \vbl{HH.M}.

The S/R specification of the complete multiplier, from which an
implementation can be synthesized, is obtained by repeated
instantiation in the S/R version of \vbl{DM}\@.  The translation to
S/R of \vbl{DM} is a simple composition of the translations of its
component multipliers and of the specifications \vbl{ExtAck} and
\vbl{Adder}.  The S/R versions of the component multipliers are
obtained by instantiation of parameters from the S/R translation of
$M$.


%try
\section{The Correctness Proof} \label{sec:proof}

We want to prove that our recursively-defined, low-level
implementation of a $k\cdot2^{m}$-bit multiplier satisfies its
high-level specification.  Let $M(i)$ and $E(i)$ denote the
specifications obtained by substituting $i$ for $N$ in the formulas
$M$ and $E$ of module \vbl{Mult}.  Let $B(k)$ be the low-level
implementation of the $k$-bit multiplier, and recursively define
$B(k\cdot2^{m+1})$ to be the specification obtained by substituting
$k\cdot2^{m}$ for $N$ and $B(k\cdot2^{m})$ for $M$ in the formula
\vbl{DM} of module \vbl{DblMult}.  We want to prove
\valid{E(k\cdot2^{m})\land B(k\cdot2^{m})\implies M(k\cdot2^{m})}, for
all $m\geq0$.  The proof is by induction on $m$.  Letting $N$ equal
$k\cdot2^{m}$, we:
\begin{enumerate}
\item[(i)] Prove 
     \begin{tabular}[t]{@{}l@{ \,}l}
         (a) & \valid{E(k)\land B(k)\implies M(k)} 
    \\[\jot]
         (b) & \valid{\plus{E(k)}\land \closure{B(k)}\implies \closure{M(k)}}
     \end{tabular}\vspace{\jot}
\item[(ii)] Assume      
   \begin{tabular}[t]{@{}l@{ \,}l}
      (a) & \valid{E(N)\land B(N)\implies M(N)} \\[\jot]
      (b) & \valid{\plus{E(N)}\land \closure{B(N)}\implies \closure{M(N)}} 
     \end{tabular}\\[\jot]
and prove 
   \begin{tabular}[t]{@{}l@{ \,}l}
    (a) \valid{E(2N)\land B(2N)\implies M(2N)} \\[\jot]
    (b) \valid{\plus{E(2N)}\land \closure{B(2N)}\implies 
                     \closure{M(2N)}}
     \end{tabular}
\end{enumerate}
Step (i), the base case of the induction, can be done by translating
the formulas to S/R and using COSPAN\@.  However, since one does not
reason about it in TLA, the specification $B(k)$ can be written
directly in S/R\@.  If $B(k)$ implements a complex multiplier, such as
the radix-4 modified version of Booth's
algorithm~\cite{koren:computer}, the COSPAN verification would be
straightforward when $k=8$.


Step~(ii), the induction step, is proved with the Decomposition
Theorem.  We first express the specification $B(2N)$ as a conjunction
of the specification of its components.  Let prefixing by \vbl{LL},
\vbl{LH}, \vbl{HL}, and \vbl{HH} denote substitutions for $a$, $x$,
\vbl{out}, and \vbl{ack} as in the \vbl{DblMult} module.  Making the
parameter $N$ explicit, our recursive procedure for combining
multipliers implies that $B(2N)$ equals
 \[
 \vbl{LL.B}(N) \land\vbl{LH.B}(N) \land\vbl{HL.B}(N) \land\vbl{HH.B}(N)
       \land \vbl{ExtAck}(N) \land  \vbl{Adder}(N) 
 \] 
We can infer the conclusion of (ii) from 
\subeqns
\begin{eqnarray} \firstlabel{eq:xrefine1a}
& \valid{E(2N) \land \vbl{LL.M}(N) \land \ldots \land \vbl{Adder}(N)
   \;\implies\; M(2N)} \\[\jot]
& \valid{\plus{E(2N)} 
\land \closure{\vbl{LL.M}(N) \land \ldots \land \vbl{Adder}(N)}
   \;\implies\; \closure{M(2N)}} \sublabel{eq:xrefine1b} \\[\jot]
& \valid{E(2N) \land B(2N) 
   \;\implies\; \vbl{LL.M}(N) \land \ldots \land \vbl{Adder}(N)} 
\firstlabel{eq:xrefine2a}
 \\[\jot]
& \valid{\plus{E(2N)} \land \closure{B(2N)}
   \;\implies\; \closure{\vbl{LL.M}(N) \land \ldots \land \vbl{Adder}(N)}}
\sublabel{eq:xrefine2b}
\end{eqnarray}
\nosubeqns 
We prove (\ref{eq:xrefine2a}) and (\ref{eq:xrefine2b}) with the
Decomposition Theorem.  Omitting trivial implications, the hypotheses
of the theorem to be verified are:
\begin{enumerate}
\item $E(2N)$, $\vbl{LL.E}(N)$, \ldots\,, 
and $\vbl{HH.E}(N)$ are safety properties.\vspace{\jot}

\item \valid{E(2N)\land \closure{\vbl{LL.M}(N)} \land\ldots
            \closure{\vbl{Adder}(N)} \;\implies\;\\
         \hspace*{3em}\vbl{LL.E}(N) \land \vbl{LH.E}(N)\land
                   \vbl{HL.E}(N)\land\vbl{HH.E}(N)}\vspace{\jot}

\item \begin{tabular}[t]{@{}l@{ \,}l}
    (a) \valid{E(N)\land B(N)\implies M(N)} \\[\jot]
    (b) \valid{\plus{E(N)}\land \closure{B(N)}\implies 
                     \closure{M(N)}}
     \end{tabular}
\vspace{\jot}
\item \valid{\closure{\vbl{LL.M}(N) \land \ldots \land \vbl{Adder}(N)}
             \;\equiv\; 
            \closure{\vbl{LL.M}(N)} \land \ldots \land \closure{\vbl{Adder}(N)}}
\end{enumerate}
Hypothesis~1 follows directly from (\ref{eq:machine-closure}).
Hypothesis~3 is just the induction assumption (the assumption in
step~(ii)).  Hence, to complete the proof, we must prove
(\ref{eq:xrefine1a}), (\ref{eq:xrefine1b}), and hypotheses 2 and 4.  The
formula \vbl{Adder} is a safety property, since it has the form $\Box
P$, so it equals its closure.  Reverting to the notation of the
\vbl{DblMult} module, we can therefore rewrite (\ref{eq:xrefine1a}),
(\ref{eq:xrefine1b}), and hypotheses 2 and 4 as
\begin{eqnarray*}
 & \valid{\vbl{DE}\land\vbl{DM}\;\implies\;\vbl{Dbl.M}}\\
 & \valid{\plus{\vbl{DE}}\land\closure{\vbl{DM}}
        \;\implies\;\closure{\vbl{Dbl.M}}}\\
 & \valid{\begin{array}[t]{@{}l@{}}
     \vbl{DE}\land
  \closure{\vbl{LL.M}}\land\ldots\land\closure{\vbl{HH.M}}
            \land\closure{\vbl{ExtAck}}\land\vbl{Adder}
              \;\implies\;\\
      \hspace*{1.5em}\vbl{LL.E}\land\ldots\land\vbl{HH.E}
\end{array}}\\
 & \valid{\closure{DM}\;\equiv\;
\closure{\vbl{LL.M}}\land\ldots\land\closure{\vbl{HH.M}}
\land\closure{\vbl{ExtAck}}\land\vbl{Adder}}
\end{eqnarray*}
We use (\ref{eq:def-plus}) to substitute for \plus{\vbl{DE}}, and the
closures are computed using (\ref{eq:machine-closure}).  The resulting
TLA formulas can then be verified using TLP\@.  Urban Engberg has
begun the TLP verification; he has encountered no serious difficulties
and we expect the proof to be completed soon.

To complete the proof of an actual multiplier circuit, we must verify
the low-level implementations of the circuits specified by the
formulas \vbl{ExtAck} and \vbl{Adder}.  Because \vbl{Adder} is purely
combinational and \vbl{ExtAck} depends on its inputs in such a simple
way, the implementations of these circuits make no assumptions about
their environment (their environment specifications are identically
true), and their correctness can be verified directly by COSPAN.

\section{Conclusion}

We have shown how two tools, TLP and COSPAN, can be combined to form a
direct path from high-level specification to synthesis.  Together, the
tools can be applied to problems that would be difficult or impossible
to handle with either tool separately.  We can combine these very
different tools because the languages on which they are based, TLA and
S/R, have similar semantics.  TLA is very expressive, but verifying
TLA specifications requires theorem proving.  S/R is less expressive,
but S/R specifications can be verified by automatic model checking.
Theorem proving involves a great deal of human effort.  Model checking
is automatic, but its use is limited by its inherent computational
complexity.  We combine the two approaches to make theorem proving as
simple as possible by proving as much as we can with model checking.

Our approach does involve checking some steps by hand.  For example,
TLP does not verify that we have correctly applied the Decomposition
Theorem.  These steps are few, very simple, and easy to check---even
for a complex problem.  Mechanically verifying these steps is
possible, but it may provide too small a gain in reliability to be
worth the effort.

The work described here is not complete.  We still need to mechanize
the TLA to S/R translation, and to try more demanding examples in
which the low-level specification is not only complex, but is also
replicated in a more complex fashion.

 \clearpage
\bibliographystyle{plain}
%\bibliography{mybib}
\begin{thebibliography}{10}

\bibitem{abadi:open}
Mart\'{\i}n Abadi and Leslie Lamport.
\newblock Open systems.
\newblock To appear in 1993 as a SRC Research Report.

\bibitem{bryant:graph}
Randal~E. Bryant.
\newblock Graph-based algorithms for {B}oolean function manipulation.
\newblock {\em IEEE Transactions On Computers}, C-35(8):677--691, August 1986.

\bibitem{chin:verified}
Shiu-Kai Chin.
\newblock Verified functions for generating signed-binary arithmetic hardware.
\newblock {\em IEEE Transactions on Computer-Aided Design}, 11(12):1529--1558,
  December 1992.

\bibitem{engberg:mechanical}
Urban Engberg, Peter Gr\o{}nning, and Leslie Lamport.
\newblock Mechanical verification of concurrent systems with {TLA}.
\newblock In {\em Computer-Aided Verification}, Lecture Notes in Computer
  Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag.
\newblock Proceedings of the Fourth International Conference, CAV'92.

\bibitem{har-el:software}
Z.~Har'El and R.~P. Kurshan.
\newblock Software for analytical development of communication protocols.
\newblock {\em AT\&T Technical Journal}, 69(1):44--59, 1990.

\bibitem{katzenelson:s/r}
J.~Katzenelson and R.~P. Kurshan.
\newblock {S/R}: A language for specifying protocols and other coordinating
  processes.
\newblock In {\em Proceedings of the 5th Annual International Phoenix
  Conference on Computer Communications}, pages 286--292, Scottsdale, Arizona,
  1986. IEEE Computer Society.

\bibitem{koren:computer}
Israel Koren.
\newblock {\em Computer Arithmetic Algorithms}.
\newblock Prentice Hall, Englewood Cliffs, New Jersey, 1993.

\bibitem{kurshan:reducibility}
R.~P. Kurshan.
\newblock Reducibility in analysis of coordination.
\newblock In P.~Varaiya and A.B. Kurzhanski, editors, {\em Discrete Event
  Systems: Models and Applications}, volume 103 of {\em Lecture Notes in
  Control and Information Sciences}, pages 19--39, Berlin, 1987.
  Springer-Verlag.

\bibitem{kurshan:analysis}
R.~P. Kurshan.
\newblock Analysis of discrete event coordination.
\newblock In J.~W. de~Bakker, W.-P. de~Roever, and G.~Rozenberg, editors, {\em
  Stepwise Refinement of Distributed Systems}, volume 430 of {\em Lecture Notes
  in Computer Science}, pages 414--453. Springer-Verlag, May/June 1989.

\bibitem{kurshan:structural}
R.~P. Kurshan and K.~McMillan.
\newblock A structural induction theorem for processes.
\newblock In {\em Proceedings of the 8th annual ACM Symposium on Principles of
  Distributed Computing}, pages 239--247. ACM Press, 1989.

\bibitem{lamport:what-good}
Leslie Lamport.
\newblock What good is temporal logic?
\newblock In R.~E.~A. Mason, editor, {\em Information Processing 83:
  Proceedings of the IFIP 9th World Congress}, pages 657--668, Paris, September
  1983. IFIP, North-Holland.

\bibitem{lamport:newtla}
Leslie Lamport.
\newblock The temporal logic of actions.
\newblock Research Report~79, Digital Equipment Corporation, Systems Research
  Center, December 1991.

\bibitem{lamport:hybrid}
Leslie Lamport.
\newblock Hybrid systems in {TLA}$^{+}$.
\newblock In Hans Rischel and Anders~P. Ravn, editors, {\em Hybrid Systems},
  Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag.
\newblock Proceedings of a Workshop on Hybrid Systems, to appear.

\end{thebibliography}

\end{document}
