%%%
%%% WARNING:   `"' (double quote) expands to verbatim
%%%
\documentstyle[verbatimfiles]{article}
\input{psfig}
\setlength{\fboxsep}{.25in}
\begin{document}
\begin{center}
{\LARGE\bf DRAFT MATERIAL\\}
\today
\end{center}

Appendix material for
``Studies of the Single-pulser in
Various Reasoning Systems,'' by
Steven D. Johnson, Paul S. Miner, and Shyam Pullela.


\appendix
\section*{DDD derivation of the single pulser}

The file called {\tt sp.ss}, shown in Figure \ref{fig:sp.ss}, contains
three Scheme function definitions.
The first of these, \verb"SP", is a representation of the Single-pulser
state machine with states \verb"READY" and \verb"WAIT".
The \verb"let"-bindings \verb"X" and \verb"I" illustrate
one way that DDD specifications are interfaced to the
Scheme I/O system for execution of the specification.
In the body of \verb"SP", the binary \verb"IN"put value is coerced 
to a truth value, \verb"I".  This is an expedient way to deal with
the coercion from binary to truth-value,
 but in other circumstances might not be appropriate for modeling.

Again in \verb"SP", the preamble
\[\begin{minipage}{2.5in}
\begin{verbatim}
(lambda (O)
  (let ((X (out O))
        (I (= (inp IN) 1)))...
\end{verbatim}
\end{minipage}
\]
Could have been suppressed by a syntax extension to give a more succinct
way of writing down the state machine.  It is omitted here because,
even with the extended syntax, the user must still understand how DDD is
operating on the more primitive syntax.

Figure \ref{fig:sp.fr} shows an execution of \verb"SP".

\subsection*{The derivation}

As we will see, much of the derivation has to do with isolating
the I/O interface from the part of the specification actually intended
for hardware.  The advantage of including the I/O is that each
transformation yields a program with which we can interact.  Thus,
it is very common to see I/O modeling in DDD specifications.
This section contains an annotated copy of a derivation script.
In practice, the user would develop this script interactively,
stopping occasionally to consolidate the relevant commands
as a Scheme source file.

Figure \ref{fig:derivation} is a chart of the derivation that
we are about to explain.
The first page of the figure, Fig. \ref{fig:derivation}(a)
shows those steps that isolate the circuit description.
After this phase, the guided work of the
dervivation is essentially finished.
The second page shows the tedious but entirely routine process of
reducing the design into a form that can be project to layout by
logic synthesis tools.  This second phase consists of syntax transduction,
instantiation of constants, and logic optimization.

Each rectangle in the figure represents set of Scheme {\tt define} expression.
The names appearing inside the rectangls are those which are thereby
defined.  The figure also shows that many of the boxes have names,
which are shown as attached to the boxes.  A dotted boundary indicates
a data structure that is either implicitly built, for example, by a global
definition.

We now enter DDD and read in the file {\tt sp.ss}

\begin{itemize}\item[]
\begin{verbatim}
;; Load DDD system & partitioning software
;; ---------------------------------------
(load "/u/bose/DDD/V1/ddd.so")
(load "/u/psm/ddd/sync/patch.ss")

;; Initial specification and sequential system
;; -------------------------------------------
(define spbeh     (read-file "sp.ss"))
(define SEQSYS    (itrsys->seqsys spbeh))
(define SELECT    (seqsys.select SEQSYS))
(define SYSTEM    (seqsys.system SEQSYS))
(define BASE      (seqsys.base   SEQSYS))
\end{verbatim}
\end{itemize}

\noindent
Next, a construction is performed translating \verb"SP"
into an equivalent network of streams.  This step
represents the transition between a behavioral mode of
description and a structural mode.
Construction \verb"itrsys->seqsys" produces a triple,
\[\mbox{\tt SEQSYS} = \mbox{\tt (SELECT\ SYSTEM\ BASE)}\]
as shown in Figure \ref{fig:SEQSYS}.
The decision combinator \verb"select" represents the interface
between a control automaton and the data path of the resulting
sequential system; it abstracts the control structure of \verb"spbeh".
The \verb"lambda*" in \verb"select"'s definition is not the standard
Scheme \verb"lambda"; it permits the nested formal parameter structure
seen in the definition.  This definition gives the discrete version
of \verb"select", which operates on individual values.  The function
\verb"SELECT", defined in a moment, is the extension of \verb"select" to
streams.

The function \verb"SP" in Figure \ref{fig:SEQSYS}
is the system itself, and it consists mainly of stream definitions
representing traces of the individual variables \verb"x", \verb"i",
and \verb"o" in \verb"spbeh".  In addition, there is a signal
\verb"STATE" implementing the control automaton, and a group of
predicate signals called \verb"STATUS" which feed back instances of
\verb"SELECT".

The function \verb"XPS" in the defining expression of \verb"STATUS"
coerces the pair of streams, \verb"(STATE I)" into a stream of pairs:
\[\mbox{\tt
((STATE$_0$\ I$_0$)\ \ (STATE$_1$\ I$_1$)\ \ (STATE$_2$\ I$_2$)\ \ $\ldots$)
}\]
This is a very commonplace coercion in DDD expressions.  \verb"XPS" is
actually a syntax extension, a generic function that, in a more strongly
typed system, would have to be instantiated for each $n$-tuple.

The third component of \verb"SEQSYS" is a collection of base definitions
generated by the \verb"itrsys->seqsys" construction.  As mentioned
earlier, \verb"SELECT" is the extension of \verb"select" to streams;
two symbolic tokens, \verb"ready" and \verb"wait", are needed to
implement the \verb"STATE" machine; finally, \verb"READY" and \verb"WAIT"
are the stream versions of these new tokens.

In the next derivation step, the goal is to isolate the modeling interface
and at the same time simplify the \verb"SELECT" expressions:
\begin{itemize}\item[]
\begin{verbatim}
(define SYSTEM.1
  (let* ((SYSTEM.1a (expand-stream 'O SYSTEM))
         (SYSTEM.1b (identify-stream 'O
                      '(SELECT STATUS ZERO ZERO ONE) SYSTEM.1a))
         ;; The previous two steps isolate the O register and move it into
         ;; the modelling interface
         (SYSTEM.1c (remove-useless-selects SYSTEM.1b))
         ;; Flatten nested selects
         )
    SYSTEM.1c))
\end{verbatim}
\end{itemize}

\noindent
The \verb"let*" is a standard Scheme expression for cascaded
\verb"let"-binding.  In the first step, \verb"SYSTEM.1a" all
occurances of \verb"O" are expanded according to \verb"O"'s
defining expression in system \verb"SP" (Figure \ref{fig:SEQSYS}).
Next all occurances of \verb"(SELECT STATUS ZERO ZERO ONE)"
are identified as \verb"O".  The affect is that subexpressions
\verb"(OUT O)" have been replaced by \verb"(OUT (! zero O))",
which will later be factored out of the design as part of the modeling
interface.  The transformation \verb"remove-useless-selects" eliminates
applications of \verb"SELECT" in which all the alternatives are indentical.
The resulting system, called \verb"SYSTEM.1"
\marginpar{\footnotesize\it Why is there an {\tt XPS} in {\tt SYSTEM.1}?}
is shown in Figure \ref{fig:SYSTEM.1}.

The next step of the derivation is to segregate that portion of
the design that will be realized in hardware.  As the commentary
states, two derivation paths were explored at this point.
We shall follow the first all the way to hardware.

\begin{itemize}\item[]
\begin{verbatim}
;; Now we have two alternatives to partition the system
;; 1) First, partition out the interface (X,I) and then the STATE
;; 2) First, partition out the interface along with the STATE
;;    (X,I,STATE) and then partition STATE from the resulting system.

;; Alternative #1
;; --------------
(define PARTITION1 (partition '(X I) (list SELECT SYSTEM.1 BASE)))
(define PARTITION1.1 (partition '(STATE) (partition.1 PARTITION1)))

(define SYSTEM.2 (seqsys.system (partition.1 PARTITION1.1)))
(define SELECT.2 (seqsys.select (partition.1 PARTITION1.1)))

(define SEQSYS.3 (optimize-seqsys SELECT.2 SYSTEM.2))
(define SYSTEM.3 (seqsys.system SEQSYS.3))
(define SELECT.3 (seqsys.select SEQSYS.3))

(define STATE-STREAM (extract-stream 'STATE
                       (seqsys.system (partition.2 PARTITION1.1))))
;; ------------------
;; End Alternative #1
\end{verbatim}
\end{itemize}

\noindent
The \verb"partition" construction decomposes one system object---%
recall that a system object is a triple consisting of a decision
combination, a sequential system description, and a collection of
base definitions---into two subsystems.  We construct \verb"PARTITION1"
by extracting streams \verb"X" and \verb"I" from \verb"SYSTEM.1" (Figure
\ref{fig:SYSTEM.1}.  The resulting subsystems are shown in Figure
\ref{fig:PARTITION1}.
The subsystem \verb"SP.1" in the figure contains that portion of the
design intended for hardware.  The residual system, \verb"SP.2"
contains those constructs that derive from the modeling interface.
Although \verb"select" is a component of the second subsystem
it is not used in the system \verb"SP.2".

\verb"SP.1" is further partitioned in order to isolate the \verb"STATE"
signal.  The result is shown in Figure \ref{fig:PARTITION1.1}.
\verb"SYSTEM.2", \verb"SELECT.2", and later, \verb"SYSTEM.3" and SELECT.3",
are simply fields of subsystem objects.  \verb"SEQSYS.3" is a refinement
of \verb"SEQSYS.2" in which applied instances of the \verb"select"
combination are simplified.  In this case, partial evaluation of the
expression \verb"(SELECT STATUS ZERO ZERO ONE)" reveals that this
instance of the underlying \verb"select" can be reduced.
The result is shown in Figure \ref{fig:SEQSYS.3}
Extraction of the \verb"STATE-STREAM" signal marks the beginning step
of projecting the design into a realizable boolean system.
\begin{itemize}\item[]
\begin{verbatim}
;; Now derive nextstate combinator
;; -------------------------------
(define NEXT-STATE
  (optimize-sel
   (partial-eval STATE-STREAM SELECT)))

;; Load the representation mappings
;; --------------------------------
(load "rep.ss")

;; Map nextstate to binary representation.
;; ---------------------------------------
(define NEXTSTATE.BIN.1
  (rename-sel 'next-state 'K NEXT-STATE))
(define NEXTSTATE.BIN.2
  (project-sel state.map NEXTSTATE.BIN.1))
(define NEXTSTATE.BIN
  (map optimize-sel
       NEXTSTATE.BIN.2))
\end{verbatim}
\end{itemize}
\noindent
The file \verb"rep.ss", is shown in Figure \ref{fig:rep.ss}
contains the declarative part of the design specification.
\marginpar{\footnotesize\it Why/how is {\tt READY} equated with {\tt STATE}
here?}
The unusual form of the definitions is an artifact of a
project to compute type translations by a nonstandard interpretation of
the source expression.
A switchover to a more conventional syntax---probably that of the Infer
type system---is planned.
The \verb"NEXT-STATE" definition, at the beginning of Figure
\ref{fig:NEXT-STATE}, is obtained by symbolically expanding
\verb"SELECT" according to its definition.
After a sequence of four elementary steps,
\marginpar{\footnotesize \it How can {\tt I} be free in the definition of
{\tt STATE}?}
we get a simplifiable defining expression for the \verb"STATE" signal:
\begin{center}
\begin{minipage}{2in}\begin{verbatim}
(case s
  [ready (if I 1 0)]
  [wait  (if I 1 0)]))
\end{verbatim}
\end{minipage}
\end{center}
\noindent
Returning to the derivation script, we make a similar projection
of the remaining \verb"select" expression in \verb"SEQSYS.3"
\begin{itemize}\item[]
\begin{verbatim}
;; Map select to binary representation.
;; ------------------------------------

(define ENCODE.BIN1 (rename-sel 'select 'CMD SELECT.3))
(define ENCODE.BIN
  (map optimize-sel
       (project-sel CMD.MAP ENCODE.BIN1)))

;; Project the datapath
;; --------------------
(define DATAPATH.BIN
  (sort-streqns
    (project-streqns streqn.map (system.streams SYSTEM.3) 1)))
\end{verbatim}
\end{itemize}
The results of these transformations are shown in Figure \ref{ENCODE}.
From this point on, the expressions resulting from the derivation are
massaged for input into logic-synthesis optimizers and layout generators.
The intermediate expressions are shown in Figure \ref{fig:DDDtoOCT}.
Details about this phase can be found in \cite{DDDmanual}.
\begin{itemize}\item[]
\begin{verbatim}
;; Logic Synthesis
;; ---------------
(define OUTPUT.BOOL (streqns->booleqns DATAPATH.BIN 'd))

(define NEXTSTATE.BOOL
  (symbolic->bit
    (map sel->booleqns NEXTSTATE.BIN) STATE.SYMMAP))

(define ENCODE.BOOL
  (symbolic->bit
    (map sel->booleqns ENCODE.BIN) STATE.SYMMAP))

(define NEXTSTATE.MIN
  (espresso NEXTSTATE.BOOL 'booleqns 'NEXT-STATE))

(define ENCODE.MIN
  (espresso ENCODE.BOOL 'booleqns 'ENCODE))

;; Final output of the system (registers, control and data-path)
;; -------------------------------------------------------------
(define REGISTER NEXTSTATE.MIN)
(define CONTROL  ENCODE.MIN)
(define OUTPUT   (espresso OUTPUT.BOOL 'booleqns 'SP))
\end{verbatim}
\end{itemize}

The last three definitions, specifying \verb"STATE", \verb"CONTROL",
 and \verb"OUTPUT" give the reduced implementation of the single pulser,
consisting of a single register and a negated-input {\it and}\/-gate.
In DDD syntax, the final definitions specify the desired network
for implementing the single pulser.

\begin{figure}[p]\label{fig:sp.ss}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{sp.ss}
\end{minipage}}
\end{center}
\caption{The source file {\tt sp.ss}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:sp.fr}
\newcommand{\emphasize}[1]{\makebox[.5pt][l]{\tt#1}#1}
\[\fbox{\begin{minipage}{.90\textwidth}
{\tt
Script started on Thu Jun 23 13:17:03 1994\\
\% \emphasize{scheme}\\
Chez Scheme Version 4.1b\\
Copyright (c) 1991 Cadence Research Systems\\
  \\
> \emphasize{(load "sp.ss")}\\
> \emphasize{(SP ())}\\
o=0\\
i=\emphasize{1}\\
o=0\\
i=\emphasize{1}\\
o=0\\
i=\emphasize{0}\\
o=1\\
i=\emphasize{0}\\
o=0\\
i=\emphasize{0}\\
o=0\\
i=\emphasize{1}\\
o=0\\
i=\emphasize{0}\\
o=1\\
i=\emphasize{\^C\^C}\\
debug> \emphasize{a}\\
 \\
\%\\
script done on Thu Jun 23 13:18:09 1994\\
}\end{minipage}}\]
\caption{Animation of {\tt SP}}
\end{figure}

\begin{figure}[p]\label{fig:derivation}
\[\psfig{figure=derivation-1a.ps}\]
\centerline{(a)}

\vspace*{2\baselineskip}
\caption{Chart of the derivation}
\end{figure}

\addtocounter{figure}{-1}

\begin{figure}[p]
\[\psfig{figure=derivation-1b.ps}\]
\centerline{(b)}

\vspace*{2\baselineskip}
\caption{Chart of the derivation (continued)}
\end{figure}

\begin{figure}[p]\label{fig:SEQSYS}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{SEQSYS}
\end{minipage}}
\end{center}
\caption{Result of command {\tt (itrsys->seqsys spbeh)}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:SYSTEM.1}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{SYSTEM.1}
\end{minipage}}
\end{center}
\caption{{\tt SYSTEM.1}, a refinement to {\tt SEQSYS.SYSTEM}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:PARTITION1}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{PARTITION1}
\vspace{\baselineskip}\noindent
{\em N.B.  The {\tt select} combinators and base definitions
 in this partitioning are the same as in Figure \ref{fig:SEQSYS}
 and have been manually removed.}

\end{minipage}}

\end{center}
\caption{A partitioning applied to {\tt SYSTEM.1}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:PARTITION1.1}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{PARTITION1.1}
\vspace{\baselineskip}\noindent
{\em N.B.  The {\tt select} combinators and base definitions
 in this partitioning are the same as in Figure \ref{fig:SEQSYS}
 and have been manually removed.}

\end{minipage}}

\end{center}
\caption{Further partitioning of {\tt SP.1}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:SEQSYS.3}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{SEQSYS.3}
\vspace{\baselineskip}\noindent
{\em N.B.  In this version of DDD, the {\tt optimize-seqsys}
 transformation does not produce a triple including base
 definitions.  These would be the same as in Figure \ref{fig:SEQSYS}.}

\end{minipage}}

\end{center}
\caption{Further partitioning of {\tt SP.1}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:rep.ss}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{rep.ss}
\vspace{\baselineskip}\noindent
\end{minipage}}
\end{center}
\caption{The file {\tt rep.ss}}
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:NEXT-STATE}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{NEXT-STATE}
\vspace{\baselineskip}\noindent
\end{minipage}}

\end{center}
\caption{Specialization of the {\tt next-state} signal}.
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:ENCODE}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{ENCODE}
\vspace{\baselineskip}\noindent
\end{minipage}}

\end{center}
\caption{Specialization of the {\tt O} signal}.
\vspace*{2\baselineskip}
\end{figure}

\begin{figure}[p]\label{fig:DDDtoOCT}
\begin{center}
\fbox{\begin{minipage}{.90\textwidth}
  \verbatimfile{DDDtoOCT}
\vspace{\baselineskip}\noindent
\end{minipage}}
\end{center}
\caption{Injection of derived implementation into logic synthesis.}
\vspace*{2\baselineskip}
\end{figure}
\end{document}

