\documentclass[12pt]{article}
% D2.1c Version 1.5
\usepackage{alltt}
%\usepackage{epsf}
%\usepackage{pstricks}
\newenvironment{greekenumerate}{\begin{enumerate}
\renewcommand{\theenumi}{\roman{enumi}}
\renewcommand{\labelenumi}{(\roman{enumi})}}{\end{enumerate}}
\renewcommand{\t}[1]{\mbox{\tt #1}}
\renewcommand{\u}[1]{\mbox{\tt #1}}
\newcommand{\con}[1]{\mbox{\sf #1}}
\newcommand{\ty}[1]{\mbox{\sl #1}}
\newcommand\fun{{\to}}
\newcommand\prd{{\times}}
\newcommand\bool{\ty{bool}}
\newcommand\num{\ty{num}}
\newcommand\ind{\ty{ind}}
\newcommand\lst{\ty{list}}
\newcommand{\z}[1]{\mbox{\small${\cal #1}$}}
\newcommand{\syn}[1]{\mbox{\small\sl {\tt <}#1{\tt >}}}
\newcommand\MODULE{\mbox{\tt{module}}}
\newcommand\END{\mbox{\tt{end}}}
\newcommand\LOCAL{\mbox{\tt{local}}}
\newcommand\INIT{\mbox{\tt{init}}}
\newcommand\assign{\mbox{\tt{:=}}}
\newcommand\ass{\mbox{$=$}}
\newcommand\nxt{\mbox{\tt{next}}}
\newcommand\thn{\mbox{\tt{?}}}
\newcommand\els{\mbox{\tt{:}}}
\newcommand\switch{\ty{switch}}
\newcommand\posedge{\mbox{\tt{posedge}}}
\newcommand\negedge{\mbox{\tt{negedge}}}
\newcommand\rise{\mbox{\tt{rise}}}
\newcommand\fall{\mbox{\tt{fall}}}
\newcommand\change{\mbox{\tt{change}}}
\newcommand\arr{\mbox{\tt{->}}}
\newcommand\And{\mbox{$\wedge$}}
\newcommand\Imp{\mbox{$\Rightarrow$}}
\newcommand\C{\mbox{$\Rightarrow$}}
\newcommand\Neg{\mbox{$\neg$}}
\newcommand\Math[1]{\mbox{$#1$}}
%\newcommand{\evassign}[3]{{\tt{@}}#1~#2~\assign~#3}
\newcommand{\evassign}[3]{#1~\arr~#2~\assign~#3}
\parindent 0mm
\parskip 1mm
\begin{document}
\title{{\Huge\bf{PROSPER}}\\[2mm]
{\Huge\bf{ESPRIT LTR Project 26241}}\\
{\tt{http://www.dcs.gla.ac.uk/prosper}}\\[10mm]
Deliverable D2.1c\\
Semantics of the Intermediate Language IL\\
{\large\it{Version 1.5}}\\[20mm]
Mike Gordon\\
Thomas Kropf\\
Dirk Hoffmann\\[35mm]
{\it{Date released: February 12, 1999}}\\
{\it{Last modified: \today}}\\
}
\author{Mike Gordon\\[-1mm]
University of Cambridge Computer Laboratory\\[-1mm]
New Museums Site\\[-1mm]
Pembroke Street\\[-1mm]
Cambridge CB2 3QG\\[-1mm]
United Kingdom\\[2mm]
work: (+44) 1223 334627\\[-1mm]
fax: (+44) 1223 334678\\[-1mm]
email: \mbox{\tt mjcg@cl.cam.ac.uk}\\[-1mm]
web: \mbox{\tt http://www.cl.cam.ac.uk/users/mjcg}\\
\ \\
Thomas Kropf\\[-1mm]
University of Karlsruhe\\[-1mm]
Institute for Computer Design and Fault Tolerance\\[-1mm]
D-76128 Karlsruhe\\[-1mm]
Germany\\[2mm]
work: (+49) 721 608 6326\\[-1mm]
fax: (+49) 721 608 3962\\[-1mm]
email: \mbox{\tt kropf@ira.uka.de}\\[-1mm]
web: \mbox{\tt http://goethe.ira.uka.de/\mbox{$\sim$}kropf}\\
\ \\
Dirk Hoffmann\\[-1mm]
University of Karlsruhe\\[-1mm]
Institute for Computer Design and Fault Tolerance\\[-1mm]
D-76128 Karlsruhe\\[-1mm]
Germany\\[2mm]
work: (+49) 721 608-7640\\[-1mm]
fax: (+49) 721 608-3962\\[-1mm]
email: \mbox{\tt hoff@ira.uka.de}\\[-1mm]
web: \mbox{\tt http://goethe.ira.uka.de/\mbox{$\sim$}hoff}\\[3mm]
}
%\date{\begin{tabular}{ll}
%{\it{Date released:}}&{\it{February 12, 1999}}\\
%{\it{Last modified:}}&{\it{\today}}\\
%\end{tabular}}
\maketitle
\newpage
\tableofcontents
\newpage
\section*{Preface to Version 1.1}\addcontentsline{toc}{section}{Preface to Version 1.1}
At the end of December 1998, I started working on an explicit
language, derived from SMV but minus some features and plus a
generalised type system. This was the plan discussed at the November
Prosper workshop and in December with Thomas Kropf in
California.
However, as I wrote the syntax and semantics of IL down I found myself
worrying about trivia like what the keywords should be called,
whether they should be in upper or lower case, whether "{\tt{;}}" should be a
separator or teminator etc.
To avoid these trivial problems, I decided to switch to the approach
used by Ian Page for his Handel HDL at Oxford: no concrete syntax, but
abstract syntax as an ML datatype. This fitted nicely with Dirk
Hoffman's ML abstract syntax datatype for SMV. Handel has a couple of
concrete syntaxes (C-like for industry, ML-like for academics), but
these are regarded as just user-interfaces. However, soon after
starting on the IL abstract syntax datatype, I realised that I was
prematurely fixing details that would need to evolve. In particular, I
have little idea what extra stuff VHDL will require in addition to
what's needed for Verilog.
Since D2.1c is specified to be a semantics, I felt justified in taking
a final leap and eliminated abstract syntax as well as concrete
syntax! The semantics of IL is presented as a set of semantic
constructs, which are explicitly expected to evolve. There is a
syntax for writing down semantic expressions (HOL term notation) so it
isn't the case that by not giving IL an explicit syntax one is
precluding writing and manipulating IL specifications. Furthermore, I
think the approach is `modern' in that it is in harmony with the
SGML-XML philosophy of separating content (semantics) from
presentation (syntax).
D2.1c Version 1.1 differs from Version 1.0$\beta$ by incorporating
suggestions, corrections and expository improvements. In particular,
the treatment and notation for assignments and the representation of
edges (\posedge, \negedge) has been modified. An additional section
has been added giving examples illustrating how IL can be used to
represent the semantics of synthesizable Verilog
\cite{ThomasMoorby,Synopsys,VFE}.
\begin{flushright}
\begin{tabular}{l}
Mike Gordon\\
February 1, 1999
\end{tabular}
\end{flushright}
\newpage
\section*{Preface to Version
1.3}\addcontentsline{toc}{section}{Preface to Version 1.3}
In Version 1.3, the report has been extended with an introduction-section
giving a brief overview over the formalization of HDLs. Besides
mentioning general remarks about how HDLs can be formalized using
logic, a brief summary is given about older research in this area.
Moreover, the report has been extended with a section about
synthesizable VHDL. VHDL-processes are examined in more detail
and the IL semantics of several VHDL programs is explained by giving
examples.
\begin{flushright}
\begin{tabular}{l}
Dirk Hoffmann\\
February 9, 1999
\end{tabular}
\end{flushright}
\section*{Preface to Version
1.5}\addcontentsline{toc}{section}{Preface to Version 1.5}
Version 1.5 reorganises the treatment of assignments
(by putting the various kinds into a single section). Also,
the event control syntax has been replaced
with one less like Verilog.
\medskip
\begin{center}
\begin{tabular}{l|l}
{\bf Old notation} & {\bf New notation} \\ \hline
\t{@(\posedge~clk)}& \t{\rise~clk ->}\\
\t{@(\negedge~clk)}& \t{\fall~clk ->}\\
\t{@(clk)}& \t{\change~clk ->}\\
\t{@(x~or~y~or~z)} & \t{change(x,y,z) ->}
\end{tabular}
\end{center}
\medskip
This notation is still experimental.
\begin{flushright}
\begin{tabular}{l}
Mike Gordon\\
February 12, 1999
\end{tabular}
\end{flushright}
\newpage
\section{Introduction}
The overall aim of circuit design is the development of correct
circuits and systems. This assumes the existence of a
specification of the intended system behaviour. Having created a
circuit implementation, methods of hardware verification may then
be used to formally prove the correctness of the implementation
with respect to the formal specification~\cite{Gupt92}. Hardware
proofs are usually performed in logics. However, the standardized
means of writing down hardware descriptions are languages such
as VHDL~\cite{VHDL87} or Verilog~\cite{Synopsys}.
This hinders the design
of correct circuits in two ways: VHDL and Verilog are known to
have imprecise semantics and there is a major gap
between such HDLs
as design languages and logics as formal systems for performing
proofs in. To be able to carry out correctness proofs of VHDL or
Verilog descriptions, a formal semantics for both languages has to
be developed.
\subsection{Methods for formalizing the semantics of HDL's}
Two ways of formalizing HDLs are:
\begin{itemize}
\item {\em Shallow embedding.}
A compiler is written to translate the given HDL program into
a logic formula. The semantics of the HDL is coded only in the
compiler. % and therefore can not be formally validated by proving
%theorems over it.
\item {\em Deep embedding.}
All constructs of the HDL are defined within a logic by definitions
of formulas for the (usually abstract) syntax and formulas
for the semantics of these constructs.
%Here, the semantics can
%be verified by proving properties of these definitions.
%Furthermore, syntax-directed verification methods are possible
%because syntax is represented as a formula and not eliminated by a compiler.
\end{itemize}
%Table \ref{overviewtable} shows the classification of approaches
%for HDLs in formal hardware verification.
%The most critical point
%of formalizing HDLs is the complexity of the task.
There is
a large semantic gap between HDLs and logic, i.e.
single HDL constructs have large and complex semantics, resulting
in large and complicated logic formulas. Thus, most works (see table
\ref{overviewtable}) have
reduced the complexity by using:
\begin{itemize}
\item the less secure, but simpler,
shallow-embedding method;
\item a subset of the HDL with simplified semantics;
\item expressive logics
(e.g. HOL, LAMBDA, OBJ3, Boyer-Moore);
\item an intermediate formalisation language
between the logic and the HDL.
\end{itemize}
\begin{table}
\begin{center}
\begin{tabular}{|l|c|l|l|c|}
\hline
Language & reference & subset & used logic & embedding \\
\hline
ART & \cite{Marg92} & complete & FOL & s \\
CASCADE & \cite{Pier91} & subset & Boyer-Moore & s \\
PML & \cite{EiSK93a} & complete & HOL & d \\
SILAGE & \cite{BGGH92} & subset & HOL & d \\
SMAX & \cite{Evek91} & complete & FOL & d \\
STRICT & \cite{KiKo92} & ? & Boyer-Moore & s \\
ELLA & \cite{BGHT91} & subset & HOL & s \\
ELLA & \cite{Goos91} & subset & LAMBDA & d \\
% ELLA & \cite{SGSE92} & subset & OBJ3 & s \\
VHDL & \cite{TaHe89} & subset & HOL & s \\
VHDL & \cite{RaHR91} & subset & Boyer-Moore & s \\
VHDL & \cite{WaSt91} & subset & LAMBDA & s \\
% VHDL & \cite{SGSE92} & subset & OBJ3 & s \\
VHDL & \cite{BoPS92} & subset & Boyer-Moore & s \\
VHDL & \cite{BoGM92} & subset & temporal & s \\
VHDL & \cite{LFMM92} & subset & temporal & s \\
VHDL & \cite{Tass92a} & subset & HOL & d \\
VHDL & \cite{OlCo93} & full & net-based & s \\
VHDL & \cite{FeBD94} & subset & Prolog & d \\
VHDL & \cite{Doeh94} & ? & net-based & s \\
VHDL & \cite{Russ94} & subset & Boyer-Moore & d\\
\hline
\end{tabular}
\caption{\label{overviewtable} Classification of approaches
for HDLs in formal hardware verification.}
\end{center}
\end{table}
\section{Design Goals}
The intermediate language IL is intended to supply a common semantic
representation for synthesisable subsets of Verilog and VHDL. It
should be easy to translate from HDL into IL and from IL into the
formal notations used for model checking and theorem proving.
This document describes the semantic concepts underlying IL. It is
expected that IL will evolve during the lifetime of Prosper, so fixing
on a concrete syntax now would be premature. Instead, a preliminary
collection of semantic constructs is presented. These are motivated
by consideration of the synthesisable subsets of Verilog and VHDL and
are designed to interface cleanly with SMV. Future detailed work on
HDL semantics may reveal the need to extend the IL semantics presented
here. Once a robust set of constructs has been identified, then a
particular concrete syntax for IL will be considered. However, it may
turn out that a concrete syntax for IL is never needed, since designs
can be represented directly as higher order logic terms. One
possibility under consideration is to define IL via an XML DTD
\cite{GhoshGordon}.
IL is intended for specifying sequential Mealy-style machines.
Machines in IL can be quite general: e.g.~partially specified,
non-deterministic or infinite state. An important subclass are those
machines that correspond to finite state transition relations. This is
the subset that can be translated to SMV.
The semantics of a system is modelled as the set (represented as a
predicate) of permitted {\it traces\/} of the inputs, states and
outputs. This is a common approach used in theorem proving
\cite{WhyHOL}. Model checking \cite{McMillanBook} takes as input a
transition relation, often represented by a formula involving primed
(next state) and unprimed (current state) variables. Although it
is in general impossible to extract a generating finite transition
relation from a set of traces, it is shown in Section~\ref{transition}
how a transition relation can be extracted from some combinations of
IL semantic constructs. Such combinations of constructs constitute the
subset of IL that supports model checking.
\section{Semantic approach}
The various semantic constructs of IL will be defined in the HOL logic
\cite{HOLbook}.
Informal mnemonic notations for the constructs will be given. This
should not be thought of as an official concrete syntax for IL. A more
formal syntax, expressed as an XML DTD, or otherwise, may be developed
later.
A specification consists of a formula containing variables ranging
over traces. Traces have logical type $\ty{num}\fun\sigma$, where
$\sigma$ is a type representing data (bits, bytes, words etc.) and the
type \ty{num} of natural numbers represents position or {\it time\/}
in the trace. The interpretation of the position depends on the level
of temporal abstraction. It can be the number of clock ticks
(e.g.~rising edges) or a finer grain simulation time, as in HDL event
simulators.
Variables are used to represent inputs and outputs. For
example, a device with input $i$ and output $o$, such that $o$ carries
the value input on $i$ delayed by one time unit, is defined by the
formula:
\medskip
~~$\forall t.~o(t{+}1)~=~i(t)$
\medskip
which is written in IL as $o~\assign~i$. Here the time $t:\ty{num}$
might represent the number of clock ticks since initialization.
At a finer grain of time, suppose $q$ gets the value of $d$ whenever
there is a rising edge on $clk$, and retains its
previous value if there is no rising edge (i.e. a Dtype). Here $t$
represents HDL simulation time. The formula relating the traces of
$d$, $clk$ and $q$ is:
\medskip
~~~$\forall t.~q(t{+}1)~=~{\tt if}~\neg clk(t) \wedge clk(t{+}1)~{\tt then}~d(t)~
{\tt else}~q(t)$
\medskip
In IL this is written as: $\rise~clk~\arr~q~\assign~d$.
Finally, consider an unusual kind of Dtype that latches on the rising
edge of $clk$ if some condition $P$ holds, but latches on the falling
edge if $P$ doesn't hold.
\medskip
~~~$\begin{array}{l}
\forall t.~(P(t)\phantom{\neg}~
~\Imp~~q(t{+}1)~=~
{\tt if}~\neg clk(t) \wedge clk(t{+}1)~{\tt then}~d(t)~{\tt else}~q(t))\\
\phantom{\forall t.~}~\wedge\\
\phantom{\forall t.~}
(\neg P(t)~
~\Imp~~q(t{+}1)~=~
{\tt if}~clk(t) \wedge \neg clk(t{+}1)~{\tt then}~d(t)~{\tt else}~q(t))
\end{array}$
\medskip
In IL, this is written:
\medskip
~~~$\begin{array}{l}
P~~\phantom{\neg}\C~~\rise~clk~\arr~q~\assign~d\t{;}\\
\neg P~~\C~~\fall~clk~\arr~q~\assign~d
\end{array}$
\subsection{Local variables}
A machine may have some internal variables that are local to the
specification.
For example, in:
\medskip
~~$w~\assign~i\t{;}~o~\assign~w$
\medskip
the variable $w$ might be considered local, the whole system just having
input $i$ and output $o$.
The standard logical representation of hiding is
existential quantification, thus in IL:
\medskip
~~~$\LOCAL~v_1~\cdots~v_n\t{.}~B$
\medskip
means:
\medskip
~~~$\exists v_1~\cdots~v_n.~B$
\medskip
\subsection{Modules}
Modules represent named hardware components.
Each module has a {\it name\/}, a number of {\it parameters\/} and
a {\it body\/}.
\medskip
~~~$\begin{array}{l}
\MODULE~{<}{\it{name}}{>} ({<}{\it{parameter}}{>},\ldots,{<}{\it{parameter}}{>})\\
~{<}{\it{body}}{>};\\
\END
\end{array}$
\medskip
A module corresponds to an equation defining its name. Thus:
\medskip
~~~$\begin{array}{l}
\MODULE~M~(V_1,\ldots,V_m)~B~\END
\end{array}$
\medskip
corresponds to the equation:
\medskip
~~~$\begin{array}{l}
M~=~\lambda(V_1,\ldots,V_m).~B
\end{array}$
\medskip
where $V_1$, \ldots, $V_m$ are variables and $B$ is a boolean term
whose free variables are included amongst the parameters (this is
necessary if the equation in HOL corresponding to a module is to be a
valid definition).
The Module name $M$ can either be declared as a constants or, in the
case of submodules, it can be a variables. See
Section~\ref{localvsconsts}. The logical type of a module name is
$\sigma_1\prd\cdots\prd\sigma_n\fun\bool$, where $\sigma_i$ is the
type of the $i$th parameter $V_i$.
Parameters will normally either be numbers representing sizes like
bit-widths, or correspond to inputs or outputs. These two
kinds of parameters are not distinguished.
Typically, the body is an existentially quantified conjunction of
submodule definitions and variable initialization (Section~\ref{init})
and assignments (Section~\ref{assign}). A semicolon will sometimes be
used as a synonym for conjunction. Thus:
\medskip
~~~$B_1;\ldots;B_n$
\medskip
means
\medskip
~~~$B_1~\wedge~\ldots~\wedge~B_n$
\medskip
Note that `\t{;}' is a separator, not a terminator.
Function applications will be written in both the standard mathematical
form $f(x)$ or in the bracketless $\lambda$-calculus form $f~x$.
\subsection{Assignments}\label{assign}
IL has three kinds of assignments: zero-delay assignments,
unit-delay assignments and event-controlled assignments.
\subsubsection{Zero-delay assignments}\label{contassign}
A {\it zero-delay assignment\/} defines the
current value of a variable in terms of other current values.
Zero-delay
assignments are just equations between traces.
\medskip
~~~$V~=~E$
\medskip
Traces are functions, so this is an equation between functions (values
of type $\num\fun\sigma$) and so is equivalent to:
\medskip
~~~$\forall t.~V~t~=~E~t$
\medskip
Zero-delay assignments to local variables can often be eliminated by replacing
occurrences of their left hand side by their right hand side using the
one-point rule ($(\exists x.~x=e~\wedge~P(x))~=~P(e)$); see
Section~\ref{initex} for an example.
\subsubsection{Unit-delay assignments}
The IL operator \nxt{} is defined by:
\medskip
~~~$\forall t.~\nxt~V~t~=~V(t{+}1)$
\medskip
The $V~\assign~E$ abbreviates:
\medskip
~~~$\nxt(V)~=~E$
\medskip
$V$ is a variable of type $\num\fun\sigma$ and $E$ is a term
having the same type. The occurrence of `$=$' here
has type $(\num\fun\sigma)\fun(\num\fun\sigma)\fun\bool$.
Thus $\nxt(V)~=~E$ and $V~\assign~E$ are equivalent and both mean:
\medskip
~~~$\forall t.~V(t{+}1)~=~E~t$
\medskip
Note that in IL the assignment $V~\assign~E$ corresponds to the SMV
assignment $~\nxt(V)~\assign~E$.
An SMV assignment $V~\assign~E$ has no delay, so is like
a zero-delay assignment in IL
(see Section~\ref{contassign}).
I hope this doesn't cause
confusion.
Terms, like $E$, on the right hand side of IL assignments are
built out of variables and `pointwise lifted' constants and
operators. See Section~\ref{operators} for more details.
\subsubsection{Event controlled assignments}\label{evassign}
An event controlled assignment
\medskip
~~~$\evassign{P}{V}{E}$
\medskip
abbreviates:
\medskip
~~~$\nxt(V)~=~P~ \thn ~ E ~ \els ~ V$
\medskip
which has semantics:
\medskip
~~~$\forall t.~V(t{+}1)~=~{\tt{if}}~P(t)~{\tt{then}}~E(t)~{\tt{else}}~V(t)$
\medskip
Common events are clock edges; a rising
edge on \t{clk} is defined by:
\medskip
~~~$\begin{array}{ll}
\rise~clk~t&=~~\neg(clk~t) ~\wedge~ clk(t{+}1)\\[1mm]
\end{array}$
\medskip
then a positive edge-triggered Dtype register is modelled by:
\medskip
~~~$\evassign{\rise~clk}{q}{d}$
\medskip
More generally define:
\medskip
~~~$\begin{array}{ll}
\rise~V~t&=~~\neg V(t) \wedge V(t{+}1)\\
\fall~V~t&=~~ V(t) \wedge \neg V(t{+}1)\\
\change~V~t&=~~\neg(V(t) = V(t{+}1))\\
\change(V_1,\ldots,V_n)~t&=~~\neg(V_1(t) = V_1(t{+}1)) ~\vee~\ldots~\vee~
\neg(V_n(t) = V_n(t{+}1))
\end{array}$
\medskip
Several assignments may be controlled by a single event control:
\medskip
~~~$P~\arr~(v_1 \assign~E_1\t{;}~\ldots~\t{;}~V_n~\assign~E_n)$
\medskip
is equivalent to:
\medskip
~~~$\evassign{P}{v_1}{E_1}\t{;}~\ldots~\t{;}~\evassign{P}{V_n}{E_n}$
\subsection{Operators on traces}\label{operators}
Constants, unary and binary data operators are lifted from values to
traces in the obvious way. For notational economy, the same symbol will
be used for a constant or operator and its lifted counterpart. It
is hoped this overloading doesn't confuse the reader. Disambiguation
is straightforward by considering types.
For example:
\medskip
~~~$\begin{array}{ll}
1&=~~\lambda t.~1\\
\neg&=~~\lambda t.~\lambda b.~ \neg(b~t)\\
+&=~~\lambda t.~\lambda m~n.~(m~t)+(n~t)
\end{array}$
\medskip
where the occurrences of `$1$', `$\neg$' and `$+$' on the left of the
equation are lifted and the corresponding occurrences on the right are not.
As a concrete example of this overloading consider:
\medskip
~~~$X ~\assign~\neg X$
\medskip
The '$\neg$' here is lifted, so has type
$(\num\fun\bool)\fun(\num\fun\bool)$. The semantics of this assignment is:
\medskip
~~~$\forall t.~X(t{+}1) = \neg X(t)$
where the '$\neg$' here is not lifted, so has type $\bool\fun\bool$.
The particular repertoire of operators in IL is not yet fixed. It is
expected that useful libraries of operators will arise during the
duration of Prosper.
An example of a useful operator is the ternary conditional operator:
\medskip
~~~$P \thn X \els Y~=~\lambda t.~ {\tt{if}}~P(t)~{\tt{then}}~X(t)~{\tt{else}}~Y(t)$
\medskip
This notation is similar to that used by C, Verilog and SMV.
It is assumed $-\thn-\els-$ associates to the right, so that:
\medskip
~~~$P \thn X \els Q \thn Y \els Z~~=~~P \thn X \els (Q \thn Y \els Z)$
\medskip
The one-armed conditional $P \thn X$ satisfies:
\medskip
~~~$\forall t.~P(t) ~~ \Imp ~~ (P \thn X) t~=~X~t$
\medskip
When $P$ is false the value of $P \thn X$ is arbitrary
(`don't care' for synthesis).
Other
more complex $n$-ary operators (like {\tt{cases}} and {\tt{switch}} of
SMV) are easily defined semantically.
\subsection{Variable initializations}\label{init}
The initial value is at time $0$ and is specified
by:
\medskip
~~~$\INIT~{<}{\it{variable}}{>}~\ass~{<}{\it{expression}}{>}$
\medskip
The semantics is that the initialization
$\INIT~V~\ass~e$
denotes:
$V~0 = e$.
\section{Examples}\label{examples}
The first three examples illustrate structural hierarchy.
\subsection{$\con{Del}$: a unit-delay}\label{Del}
A unit-delay models a register at the abstract state machine level.
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del}~(i,o)\\
~o~\assign~ i\\
\END
\end{array}$
\medskip
This is equivalent to the definition:
\medskip
~~~$\con{Del}~=~\lambda(i,o).~\forall t.~o(t{+}1) = i~t$
\medskip
\subsection{$\con{Del2}$: two unit-delays in series}
The following module has a local definition
of the unit-delay $\con{Del}$ and also a local variable $x$.
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del2}~(i,o)\\
~\LOCAL~Del~x.\\
~\MODULE~Del~(i,o)\\
~~o~=i\\
~\END;\\
~Del(i,x);\\
~Del(x,o)\\
\END
\end{array}$
\medskip
Note that the typographical convention used here is that italics are
used for variable names (e.g.~$x$ and $Del$) and sans serif for
constants (e.g.~$\con{Del2}$). A top-level module definition defines a
constant, but local submodule names are variables (variables can be
quantified; constants can't).
Unfolding definitions yields:
\medskip
~~~$\begin{array}{lll}
\con{Del2}~=~\lambda(i,o).~\exists Del~x.
& (Del~=~\lambda(i,o).~\forall t.~o(t{+}1) = i~t) & \wedge\\
& Del(i,x) & \wedge\\
& Del(x,o)\\
\end{array}$
\medskip
Simplifying using the one-point rule yields:
\medskip
~~~$\begin{array}{l}
\con{Del2}~=~\lambda(i,o).~\exists x.~(\forall t.~x(t{+}1) = i~t)~\wedge~
(\forall t.~o(t{+}1) = x~t)
\end{array}$
\medskip
Using
$((\forall t.~P~t)~\wedge~(\forall t.~Q~t))~=~(\forall t.~P~t~\wedge~Q~t)$
yields:
\medskip
~~~$\begin{array}{l}
\con{Del2}~=~\lambda(i,o).~\exists x.~\forall t.~x(t{+}1) = i~t~\wedge~o(t{+}1) = x~t
\end{array}$
\medskip
\subsection{$\con{Del4}$: two $\con{Del2}$s in series}
The next example illustrates how confusion between module parameters and
local variables with the same name is taken care of automatically by
the standard logical treatment of free and bound variables.
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del4}~(i,o)\\
~\LOCAL~Del2~x.\\
~\MODULE~Del2~(i,o)\\
~~\LOCAL~Del~x.\\
~~\MODULE~Del~(i,o)\\
~~~o~\assign~i\\
~~\END;\\
~~Del(i,x);\\
~~Del(x,o)\\
~\END\\
~Del2(i,x);\\
~Del2(x,o)\\
\END
\end{array}$
\medskip
Expanding definitions and using the equation derived above for $Del2$ yields:
\medskip
~~~$\begin{array}{lll}
\con{Del4}~=&\lambda(i,o).\\
& ~\exists Del2~x. &\\
& ~~(Del2 = \lambda(i,o).~\exists x.~\forall t.~x(t{+}1) = i~t~\wedge~o(t{+}1) = x~t) &
\wedge\\
& ~~Del2(i,x) & \wedge\\
& ~~Del2(x,o)\\
\end{array}$
\medskip
Simplifying using the one-point rule, and renaming the existentially
quantified bound variables to avoid capture yields:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x. &(\exists x_1.~\forall t.~x_1(t{+}1) = i~t~\wedge~
x(t{+}1) = x_1~t) ~ \wedge\\
& (\exists x_2.~\forall t.~x_2(t{+}1) = x~t~\wedge~o(t{+}1) = x_2~t)
\end{array}$
\medskip
Using
$((\exists x_1.~E_1)~\wedge~E_2)~=~(\exists x_1.~E_1~\wedge~E_2)$
(which holds if $x_1$ desn't occur free in $E_2$)
and
$(E_1~\wedge~(\exists x_2.~E_2))~=~(\exists x_2.~E_1~\wedge~E_2)$
(which holds if $x_2$ desn't occur free in $E_1$)
yields:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x~x_1~x_2. &(\forall t.~x_1(t{+}1) = i~t~\wedge~x(t{+}1) = x_1~t)
~ \wedge\\
& (\forall t.~x_2(t{+}1) = x~t~\wedge~o(t{+}1) = x_2~t)
\end{array}$
\medskip
Moving $\forall$ up through $\wedge$ yields:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x~x_1~x_2.~\forall t.&x_1(t{+}1) = i~t~\wedge~x(t{+}1) = x_1~t
~ \wedge\\
& x_2(t{+}1) = x~t~\wedge~o(t{+}1) = x_2~t
\end{array}$
\medskip
which is equivalent to the flat module definition:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del4}~(i,o)\\
~\LOCAL~x~x_1~x_2.\\
\begin{array}{ll}
x_1\hspace*{-2.5mm}&\assign~~i;\\
x\hspace*{-2.5mm}&\assign~x_1;\\
x_2\hspace*{-2.5mm}&\assign~x;\\
o\hspace*{-2.5mm}&\assign~x_2\\
\end{array}\\
\END
\end{array}$
\medskip
It is clear from this that a transition relation corresponding to $\con{Del4}$ is:
\medskip
~~~$
\begin{array}{l}
\lambda((i,o,x,x_1,x_2),(i',o',x',x_1',x_2')) ~=\\[0.5mm]
~~~x_1'=i~\wedge~x'=x_1~\wedge~x_2'=x~\wedge~o'=x_2
\end{array}$
\subsection{Local variables versus global constants}\label{localvsconsts}
The previous definition of $\con{Del4}$ had a local module $Del2$, which in
turn had a local module $Del$. Local modules are existentially quantified predicate
variables. An alternative style, appropriate for general
components, is to extend the theory by defining modules as constants.
With this approach one would make constant definitions:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del}~(i,o)\\
~o~\assign~ i\\
\END
\end{array}$
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del2}~(i,o)\\
~\LOCAL~x.\\
~\con{Del}(i,x);\\
~\con{Del}(x,o)\\
\END
\end{array}$
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del4}~(i,o)\\
~\LOCAL~x.\\
~\con{Del2}(i,x);\\
~\con{Del2}(x,o)\\
\END
\end{array}$
\medskip
Whether to declare modules as local variables or as global constants
is a matter of style. Clearly with both approaches one ends up with the same semantics
of the top-level module, namely:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x~x_1~x_2.~\forall t.&x_1(t{+}1) = i~t~\wedge~x(t{+}1) = x_1~t
~ \wedge\\
& x_2(t{+}1) = x~t~\wedge~o(t{+}1) = x_2~t
\end{array}$
\subsection{Example with initialisation and combinational logic}\label{initex}
Consider a version of $\con{Del4}$ in which the unit delay $\con{Del}$ is initialized
to $\con{v}_0$ at time $0$ and there is a combinational function $\con{f}$ inserted between
the two $\con{Del2}$s in series:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del}~(i,o)\\
~\INIT~o~\ass~\con{v}_0\\
~o~\assign~ i\\
\END
\end{array}$
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del2}~(i,o)\\
~\LOCAL~x.\\
~\con{Del}(i,x);\\
~\con{Del}(x,o)\\
\END
\end{array}$
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del4}~(i,o)\\
~\LOCAL~x_1~x_2.\\
~\con{Del2}(i,x_1);\\
~x_2~\ass~\con{f}(x_1);\\
~\con{Del2}(x_2,o)\\
\END
\end{array}$
\medskip
With the added initialisation, the semantics of \con{Del} becomes:
\medskip
~~~$\con{Del}~=~\lambda(i,o).~o(0)=\con{v}_0~\wedge~\forall t.~o(t{+}1) = i~t$
\medskip
the semantics of \con{Del2} becomes:
\medskip
~~~$\begin{array}{l}
\con{Del2}~=~\lambda(i,o).~\exists x.~x(0)=\con{v}_0 ~\wedge~o(0)=\con{v}_0 ~\wedge\\
\phantom{Del2~=~\lambda(i,o).~\exists x.~}
\forall t.~x(t{+}1) = i(t)~\wedge~o(t{+}1) = x(t)
\end{array}$
\medskip
and the semantics of \con{Del4} becomes:
\medskip
~~~$\begin{array}{lll}
\con{Del4}~=~\lambda(i,o).~\exists x_1~x_2.
& (\exists x_3.~x_3(0)=\con{v}_0~\wedge~x_1(0)=\con{v}_0~\wedge~ \\
& ~~ \forall t.~x_3(t{+}1) = i~t~\wedge~x_1(t{+}1) = x_3~t) & \wedge\\
& (\forall t.~x_2~t~=\con{f}(x_1~t)) & \wedge\\
& (\exists x_4.~x_4(0)=\con{v}_0~\wedge~o(0)=\con{v}_0~\wedge\\
& ~~ \forall t.~x_4(t{+}1) = x_2~t~\wedge~o(t{+}1) = x_4~t)
\end{array}$
\medskip
which simplifies by eliminating the equation for $x_2~t$ to:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x_1.
& (\exists x_3.~x_3(0)=\con{v}_0~\wedge~x_1(0)=\con{v}_0~\wedge~ \\
& ~~ \forall t.~x_3(t{+}1) = i~t~\wedge~x_1(t{+}1) = x_3~t) ~ \wedge\\
& (\exists x_4.~x_4(0)=\con{v}_0~\wedge~o(0)=\con{v}_0~\wedge\\
& ~~ \forall t.~x_4(t{+}1) = \con{f}(x_1~t)~\wedge~o(t{+}1) = x_4~t)
\end{array}$
\medskip
and then (details left to the reader) to:
\medskip
~~~$\begin{array}{ll}
\con{Del4}~=~\lambda(i,o).~\exists x_1~x_3~x_4.
& x_3(0)=\con{v}_0~\wedge~x_1(0)=\con{v}_0~\wedge~ \\
& x_4(0)=\con{v}_0~\wedge~o(0)=\con{v}_0~\wedge\\
& \forall t.~x_3(t{+}1) = i~t~\wedge~x_1(t{+}1) = x_3~t) ~ \wedge\\
& \phantom{\forall t.~}x_4(t{+}1) = \con{f}(x_1~t)~\wedge~o(t{+}1) = x_4~t
\end{array}$
\medskip
which is equivalent to the flat module definition:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del4}~(i,o)\\
~\LOCAL~x_1~x_3~x_4.\\
\begin{array}{ll}
\INIT~x_3\hspace*{-2.5mm}&\ass~\con{v}_0;\\
\INIT~x_1\hspace*{-2.5mm}&\ass~\con{v}_0;\\
\INIT~x_3\hspace*{-2.5mm}&\ass~\con{v}_0;\\
\INIT~o \hspace*{-2.5mm}&\ass~\con{v}_0;\\
x_3&\hspace*{-8.5mm}\assign~i;\\
x_1&\hspace*{-8.5mm}\assign~x_3;\\
x_4&\hspace*{-8.5mm}\assign~\con{f}~x_1;\\
o &\hspace*{-8.5mm}\assign~x_4\\
\end{array}\\
\END
\end{array}$
\medskip
The state transition system corresponding to this has initial state specified by:
\medskip
~~~$x_1=\con{v}_0~\wedge~x_3=\con{v}_0~\wedge~x_4=\con{v}_0~\wedge~o=\con{v}_0$
\medskip
and transition relation:
\medskip
~~~$
\begin{array}{l}
\lambda((i,o,x_1,x_3,x_4),(i',o',x',x_1',x_3',x_4')) ~=\\[0.5mm]
~~~x_3'=i~\wedge~x_1'=x_3~\wedge~x_4'=\con{f}~x_1~\wedge~o'=x_4
\end{array}$
\subsection{A simple state-machine}
The example below is from 1.2.4 of Kenneth McMillan's book entitled {\it
The SMV Language\/} \cite{SMVdocs}.
The variable $state$ can take one of three values: \con{idle}, \con{cyc1}, \con{cyc2}.
To support this, define a new type:
\medskip
~~~$\ty{state}~=~\con{idle}~\mid~\con{cyc1}~\mid~\con{cyc2}$
\medskip
The variables $start$ and $done$ are boolean (i.e.~of type \ty{bool}).
\medskip
~~~$\begin{array}{l}
\MODULE~\con{StateMachine}~(start,done)\\
~\LOCAL~state.\\
~\INIT~state~\ass~\con{idle};\\
~state~~\assign~~~(state=\con{idle})~~\thn~(start \thn \con{cyc1} \els \con{cyc2})~\els\\
\phantom{~state~~\assign~~~}
(state=\con{cyc1})~\thn~\con{cyc2}~\els\\
\phantom{~state~~\assign~~~}
(state=\con{cyc2})~\thn~\con{idle};\\
~done~\ass~(state = \con{cyc2})\\
\END
\end{array}$
\medskip
{\bf Exercise.} Write down the semantics of \con{StateMachine}
and the derived state transition system (see Section~\ref{transition} below).
\subsection{\con{Dreg}: a clocked Dtype register}\label{Dreg}
A standard positive edge triggered Dtype register that is initilised
to store \con{F} (i.e.~falsity or {\tt{0}}) is defined by:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Dreg}~(clk,d,q,\overline{q})\\
~\INIT~q~\ass~\con{F};\\
~\evassign{\rise~clk}{q}{d};\\
~\overline{q}~\ass~\neg q\\
\END
\end{array}$
\medskip
This means:
\medskip
~~~$\begin{array}{lll}
\con{Dreg}~=&\lambda(clk,d,q,\overline{q}).~\\
& ~~q(0)=\con{F}&\wedge\\
& ~~(\forall t.~
q(t{+}1)~=~{\tt{if}}~\rise~clk~t~{\tt{then}}~d~t~{\tt{else}}~q~t)&\wedge\\
& ~~(\forall t.~\overline{q}~t~=~\neg(q~t))
\end{array}$
\medskip
i.e.
\medskip
~~~$\begin{array}{lll}
\con{Dreg}~=&\lambda(clk,d,q,\overline{q}).\\
& ~~q(0)=\con{F}&\wedge\\
& ~~(\forall t.~
q(t{+}1)~=~{\tt{if}}~\neg(clk~t)\wedge clk(t{+}1)~{\tt{then}}~d~t~{\tt{else}}~q~t)&\wedge\\
& ~~(\forall t.~\overline{q}~t~=~\neg(q~t))
\end{array}$
\medskip
Note that the zero-delay assignment to $\overline{q}$ cannot be
eliminated, since $\overline{q}$ is not a local variable, but is an
output.
The state transition system corresponding to this has initial state specified by:
\medskip
~~~$q~0~=~\con{F}~\wedge~\overline{q}~0~=~\con{T}$
\medskip
and transition relation:
\medskip
~~~$
\begin{array}{l}
\lambda((clk,d,q,\overline{q}),(clk',d',q',\overline{q}')) ~=\\[0.5mm]
~~~(q'~=~{\tt{if}}~\neg clk \wedge clk'~{\tt{then}}~d~{\tt{else}}~q) ~\wedge~
(\overline{q}~=~\neg q) ~\wedge~ (\overline{q}'~=~\neg q')\\
\end{array}$
\section{Extracting transition relations}\label{transition}
As has been illustrated via the examples, many modules can be flattened by logical
manipulation into a form:
\medskip
~~~$\begin{array}{l}
\MODULE~{<}{\it{name}}{>}~({<}{\it{parameters}}{>})\\
~\INIT~{<}{\it{initialisation}}{>};\\
~\LOCAL~{<}{\it{variables}}{>}.\\
~{<}{\it{unit{-}delay~assignments}}{>};\\
~{<}{\it{zero{-}delay~assignments}}{>}\\
\END
\end{array}$
\medskip
whose semantics is, roughly speaking:
\medskip
~~~$\begin{array}{ll}
{<}{\it{name}}{>}~=~\lambda({<}{\it{parameters}}{>}).
& \exists {<}{\it{variables}}{>}.~\\
& ~~{<}{\it{initialisation}}{>}~\wedge\\
& ~~\forall t. ~{<}{\it{unit{-}delay~assignments}}{>}~\wedge\\
& ~~\phantom{\forall t.} ~{<}{\it{zero{-}delay~assignments}}{>}
\end{array}$
\medskip
If all the parameters and variables have finite types, then a formula like this
determines a state transition system. Consider:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{M}~(p_1,\ldots,p_m)\\
~\LOCAL~l_1~\cdots~l_n.\\
~\INIT~v_1~\ass~e_1;~\cdots~;~\INIT~v_r~\ass~e_r;\\
~v_1~\assign~E_1;~\ldots~;~v_p~\assign~E_p;\\
~v_{q}~\ass~E_{q};~\ldots~;~v_r~\ass~E_r\\
\END
\end{array}$
\medskip
In this general form, the variables assigned to $v_1,v_2,\ldots$ are a
subset of the union of the parameters $p_1,\ldots,p_m$ and the local
variables $l_1,\ldots,l_n$. The initialisation expressions
$e_1,\ldots,e_r$ are value expressions not containing parameters
or locals. The assignment right hand sides $E_1,\ldots,E_p$ are
trace-valued expressions that may contain occurrences of the
parameters and locals.
Let $E_q',\ldots,E_r'$ be the expressions
obtained from $E_q,\ldots,E_r$ by replacing occurrences of
$v_1,\ldots,v_r$ by the primed variables $v_1',\ldots,v_r'$,
respectively.
The module above corresponds to the state transition system with
initial set of states defined by:
\medskip
~~~$v_1~0~=~e_1~\wedge~\cdots~\wedge~v_r~0~=~e_r$
and transition relation:
\medskip
~~~$
\begin{array}{l}
\lambda((v_1,\ldots,v_r),(v_1',\ldots,v_r')) ~=\\[0.5mm]
~~~v_1'=E_1~\wedge~\cdots~\wedge~v_p'=E_p~\wedge\\
~~~v_q=E_q~\wedge~\cdots~\wedge~v_r=E_r~\wedge\\
~~~v_q'=E_q'~\wedge~\cdots~\wedge~v_r'=E_r'
\end{array}$
\medskip
Note that the unit-delay assignments specify the next state (primed variables) in
terms of the current state (unprimed variables), but the zero-delay
assignments specify the values of variables in both the current and
next states.
Note that the Dtype register in Section~\ref{Dreg} is not of this form, but
still determines a transition system. Thus the method of extracting
transition systems from IL semantic representation described here can
be extended to cover a wider class of examples. It is expected that
such extensions will be developed during the Prosper project.
{\bf Exercise.} Consider how to generalise the method of extracting
transition systems given here so that the transition system for
\con{Dreg} of Section~\ref{Dreg} can be automatically derived.
\section{Different timescales}\label{timescales}
An important feature of the semantics presented here is
that it supports abstraction and refinement. Modules are predicates
and thus abstraction/refinement can be represented by logical
implication. In the context of theorem proving, this has been worked
out in detail \cite{Herbert88,Melhambook}. Considerable current work
aims to use abstraction as a basis for combining model checking and
theorem proving. The framework described here is intended to
facilitate this.
Recall from ~Section~\ref{Del} the
unit-delay example:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Del}~(i,o)\\
~o~\assign~ i\\
\END
\end{array}$
\medskip
which is equivalent to:
\medskip
~~~$\con{Del}~=~\lambda(i,o).~\forall t.~o(t{+}1) = i~t$
\medskip
The timescale of this example is the `clock tick' scale -- i.e.~the
value of the time variable $t$ is the number of clock ticks since initialisation.
Consider now a version of \con{Dreg} without the $\overline{q}$ output:
\medskip
~~~$\begin{array}{l}
\MODULE~\con{Dtype}~(clk,d,q)\\
~\INIT~q~\ass~\con{F};\\
~\evassign{\rise~clk}{q}{d}\\
\END
\end{array}$
\medskip
which means:
\medskip
~~~$\begin{array}{lll}
\con{Dtype}~=&\lambda(clk,d,q).\\
& ~~q(0)=\con{F} ~ \wedge\\
& ~~(\forall t.~
q(t{+}1)~=~{\tt{if}}~\neg(clk~t)\wedge clk(t{+}1)~{\tt{then}}~d~t~{\tt{else}}~q~t)&
\end{array}$
\medskip
The timescale here is much finer. It is similar to the timescale used
by event simulators for HDLs. The more abstract timescale used for
\con{Del} is the timescale used in cycle-based simulation.
The relation between \con{Del} and \con{Dtype} is one of {\it temporal abstraction}:
\medskip
~~~$\begin{array}{l}
\forall clk.~ \con{Inf}(\con{Rise}~clk) ~\Rightarrow\\[1mm]
\phantom{\forall clk.~ }
\forall d~q.~ \con{Dtype}(clk,d,q)~\Rightarrow~\con{Del}(d~\con{when}~(\con{Rise}~clk), q~\con{when}~(\con{Rise}~clk))
\end{array}$
\medskip
The various operators used here are explained in
Melham's book \cite[p.~104]{Melhambook}; they
are similar to ones found in LUSTRE
\cite{LUSTRE}.
\section{Semantics of synthesizable Verilog}\label{verilog}
In this section, a semantics for a reasonably large
subset of synthesizable Verilog is outlined via examples.
The semantics reflects a synthesis interpretation
of Verilog: HDL text is viewed as specifying
a collection of state machines (one for each
Verilog \t{always}-block).
This should be contrasted with a simulation interpretation, in which
HDL is interpreted by an event scheduling algorithm. It is a hard unsolved
problem to ensure that the synthesis and simulations views
coincide. Solving this is important if one is to have complete
confidence that synthesised hardware will have properties
predicted by simulation. This problem is not addressed here (but a
start has been made elsewhere \cite{EventCycle}).
The semantics of Verilog splits into three largely orthogonal aspects:
expression evaluation, statement interpretation and
module elaboration.
\subsection{Expression evaluation}\label{expressions}
Expression evaluation concerns the detailed semantics of the Verilog
operators on the various datatypes. There are many subtleties arising
out of the way operators can truncate or pad bitstrings to meet
declared size specifications. Also, the values {\tt{x}} and {\tt{z}}
are tricky and tend to be interpreted differently by simulation and
synthesis. The value {\tt{x}} is an undefined value for simulation and
a don't care value for synthesis. Certain occurrences of the value
{\tt{z}} cause tri-state logic to be synthesized, but it is not clear
that this always corresponds to how simulators treat {\tt{z}}.
Verilog's expression evaluation is not considered here,
but a detailed analysis can be found in a report by Myra Van Inwegen
\cite{MyraVerilog}. It is assumed that HOL
datatypes corresponding to Verilog types will be defined, together with
appropriate operators on the values.
\subsection{Statement interpretation}\label{statements}
The semantics of statements in IL will be illustrated via examples.
These are adapted from an unpublished report \cite{EventCycle},
where a general procedure for interpreting statements is given.
Statements occur in Verilog modules as \t{always}-blocks of the form
\t{always}~\z{S}.
The following examples show the IL semantics of a number of such
\t{always}-blocks. When there is more than one event control in a
statement, a local program counter \t{pc} is used to encode which
event control is active. Other ways of encoding control state are
possible (e.g.~one-hot).
\subsubsection*{Example 1}
%\vspace{-3mm}
The example below sets \t{a} to \t{0} on the first edge and then sets
\t{b} to \t{a} on the second edge. Thereafter \t{a} and \t{b} are
updated with \t{0} on each cycle.
{\baselineskip13pt\begin{alltt}
always @(posedge clk) begin a=0; @(posedge clk) b=a; end
\end{alltt}}
A semantics in IL is:
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc = 0;
pc = 0 \C rise clk -> (pc \assign 1; a \assign 0; b \assign b);
pc = 1 \C rise clk -> (pc \assign 0; a \assign a; b \assign a)
\end{alltt}}
{\bf{N.B.:}} do not confuse Verilog's semantics of `\t{;}' inside
\t{begin}--\t{end}
blocks (sequencing) from IL's use of `\t{;}' (conjunction).
\subsubsection*{Example 2}
\vspace{-1.5mm}
The following example is a state machine described in an implicit
style. It is Example~8-16 from the Synopsys HDL Compiler
for Verilog Reference Manual \cite{Synopsys}.
{\baselineskip13pt\begin{alltt}
always
begin
@(posedge clk) total = data;
@(posedge clk) total = total + data;
@(posedge clk) total = total + data;
end
\end{alltt}}
A semantics in IL:
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc = 0;
pc = 0 \C rise clk -> (pc \assign 1; total \assign data);
pc = 1 \C rise clk -> (pc \assign 2; total \assign total+data);
pc = 2 \C rise clk -> (pc \assign 0; total \assign total+data)
\end{alltt}}
\vspace{-3mm}
\subsubsection*{Example 3}
\vspace{-1.5mm}
An explicit style of description of the machine in Example~2
is given next.
This is Example~8-17 from the Synopsys HDL Compiler
for Verilog Reference Manual \cite{Synopsys}.
{\baselineskip13pt\begin{alltt}
always
@(posedge clk)
begin
case (state)
0: begin total = data;
state = 1;
end
1: begin total = total + data;
state = 2;
end
default:
begin total = total + data;
state = 0;
end
endcase
end
\end{alltt}}
Semantics in IL:
{\baselineskip13pt\begin{alltt}
rise clk -> (total \assign (state = 0) ? data : total+data;
state \assign (state = 0) ? 1 : (state = 1) ? 2 : 0)
\end{alltt}}
The explicit states style of state machine
eliminates the need for a program counter.
\subsubsection*{Example 4}
%\vspace{-3mm}
Another example not requiring a program counter is:
{\baselineskip13pt\begin{alltt}
always @(posedge clk)
if (p) begin a=b; b=a; end
else begin a<=b; b<=a; end
\end{alltt}}
Here \t{<=} is Verilog's non-blocking assignment. The semantics is:
{\baselineskip13pt\begin{alltt}
rise clk -> (a \assign b;
b \assign p ? b : a)
\end{alltt}}
\subsubsection*{Example 5}
%\vspace{-3mm}
Asynchronous (combinational) always blocks also don't need
program counters. For example:
{\baselineskip13pt\begin{alltt}
always @(b or c) a = b + c
\end{alltt}}
has semantics:
{\baselineskip13pt\begin{alltt}
change(b,c) -> a \assign b+c
\end{alltt}}
Whenever \t{b} and \t{c} change, \t{a} is updated, hence it follows
(induction over time) that
the equation $\forall t.~\t{a}(t)~=~\t{b}(t)+\t{c}(t)$ is an invariant.
Thus {\tt{change(b,c)~->~a~\assign~b+c}} is equivalent to the zero-delay
assignment {\tt{a~=~b+c}}.
However consider instead:
{\baselineskip13pt\begin{alltt}
always @(b) a = b+c;
\end{alltt}}
This has semantics:
{\baselineskip13pt\begin{alltt}
change b -> a \assign b+c
\end{alltt}}
Suppose \t{a} equals \t{b+c}. If \t{c} changes,
then the event control {\tt{change~b}} is not triggered, so \t{a} won't be updated
and may become different from \t{b+c}. Thus
\t{a}'s value must be latched, so this does not define combinational logic.
This illustrates the need for synthesizers to do
latch inference (and/or warn about suspected incomplete sensitivity lists).
\subsubsection*{Example 6}
%\vspace{-3mm}
Here is a combinational example that doesn't lead to any latch
inference.
{\baselineskip13pt\begin{alltt}
always
@(a or b or c or d)
begin
f = a;
if (b)
begin
if (c) f = d; else f = !d;
end
end
\end{alltt}}
Semantics:
{\baselineskip13pt\begin{alltt}
change(a,b,c,d) -> f \assign b ? (c ? d : \(\neg\)d) : a
\end{alltt}}
\subsubsection*{Example 7}
%\vspace{-3mm}
This example is unlikely to arise in practice:
{\baselineskip13pt\begin{alltt}
always if (p) begin
a=1;
@(posedge clk) b=2;
@(negedge clk) c=3;
end
else begin
a=5;
@(clk) b=6;
end
\end{alltt}}
The semantics is:
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc \ass p ? 1 : 3;
\INIT a \ass p ? 1 : 5;
pc = 1 \C rise clk -> (pc \assign 2;
c \assign c;
a \assign a;
b \assign 2);
pc = 2 \C fall clk -> (pc \assign p ? 1 : 3;
c \assign 3;
a \assign a;
b \assign 2);
pc = 3 \C change clk -> (pc \assign p ? 1 : 3;
c \assign 3;
a \assign p ? 1 : 5;
b \assign b)
\end{alltt}}
\newpage
\subsubsection*{Example 8}
{\baselineskip13pt\begin{alltt}
always @(posedge clk)
begin
X = Inp1; Y = X+Inp2;
@(posedge clk)
OUT = X+Y;
end
\end{alltt}}
has semantics:
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc = 0;
pc = 0 \C rise clk -> (pc = 1;
X = Inp1;
Y = Inp1+Inp2;
OUT = OUT);
pc = 1 \C rise clk -> (pc = 0;
X = X ;
Y = Y;
OUT = X+Y)
\end{alltt}}
\subsubsection*{Example 9}
\vspace{-1.5mm}
{\baselineskip13pt\begin{alltt}
always @(posedge clk)
begin
if (Choose) X = In1; else X = In2;
@(posedge clk)
OUT = X + 1;
end
\end{alltt}}
\vspace{-1.5mm}
has semantics:
\vspace{-1.5mm}
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc = 0;
pc = 0 \C rise clk -> (pc = 1;
X = Choose ? In1 : In2;
OUT = OUT);
pc = 1 \C rise clk -> (pc = 0;
X = X;
OUT = X + 1)
\end{alltt}}
\vspace{-3mm}
\subsubsection*{Example 10}
\vspace{-1.5mm}
{\baselineskip13pt\begin{alltt}
always @(posedge clk)
begin
X = Inp1; Y = Inp2; OUT=X;
while (Y > 1)
begin
@(posedge clk)
OUT = OUT+X; Y = Y-1;
end
end
\end{alltt}}
\vspace{-1.5mm}
is a naive multiplier and has semantics:
\vspace{-1.5mm}
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
\INIT pc = 0;
pc = 0 rise clk -> (pc = Inp2 > 1 ? 1 : 0;
X = Inp1;
OUT = Inp1;
Y = Inp2);
pc = 1 rise clk -> (pc = Y-1 > 1 ? 1 : 0;
X = X;
OUT = OUT+X;
Y = Y-1)
\end{alltt}}
A systematic treatment of a reasonably large class of Verilog
statements is considered in an unpublished report \cite{EventCycle},
including block disables, \t{while}-statements, \t{for}-statements
and \t{case}-statements.
It is hoped to develop a more compositional semantic treatment than
the one described there, but it does at least provide a
reassuring fall-back position.
\subsection{Module elaboration}\label{modules}
The elaboration of Verilog modules will be handled using
IL module constructs, as illustrated in Section~\ref{examples}.
A Verilog specification consists of a collection of modules. Modules
cannot have local submodules, so the approach described in
Section~\ref{localvsconsts}, in which each module defines a constant,
is appropriate.
Modules can have local {\it functions\/}, {\it tasks\/}, {\it wires\/}
and {\it registers\/}. Functions define abbreviations for
combinational logic, whereas tasks are abbreviations for state
machines. Wires are driven continuously, whereas registers hold
persistent state which is modified by a programming-like assignment
statement.
Because types are being glossed over here, type-related information
will be ignored. This includes bit-widths, input/output/inout
declarations and the distinction between wires and registers. Also,
functions and tasks are given explicit parameter lists, rather than
(as is the case in Verilog proper) parameters being declared
inside function and task bodies using input/output declarations.
A typical Verilog module declaration will be taken to have the
form shown below.
\bigskip
$\begin{array}{l}
\t{module}\ \syn{name}
\ \t{(}\syn{name}\t{,} \ldots \t{,}\syn{name}\t{)}\t{;}\\[-2mm]
\\[-2mm]
~~~~\vdots\\[2mm]
~\t{function}~\syn{name}\t{(}\syn{name}\t{,} \ldots \t{,}\syn{name}\t{)}\t{;}\\[-1.5mm]
~~~ \syn{statement}\\[-1.5mm]
~\t{endfunction} \\
~~~~\vdots\\[2mm]
~\t{task}~\syn{name}\t{;}\t{(}\syn{name}\t{,} \ldots \t{,}\syn{name}\t{)}\\[-1.5mm]
~~~ \syn{statement}\\[-1.5mm]
~\t{endfunction} \\
~~~~\vdots\\[2mm]
~\t{wire}~\syn{name}\t{;}\\
~~~~\vdots\\[2mm]
~\t{reg}~\syn{name}\t{;}\\
~~~~\vdots\\[2mm]
~\t{assign}~\syn{name}~\t{=}\ \syn{expression}\t{;}\\
~~~~\vdots\\[2mm]
~\t{always}~\syn{statement}\t{;}\\
~~~~\vdots\\[2mm]
~\syn{name}
\ \t{(}\syn{expression}\t{,} \ldots \t{,}\syn{expression}\t{)}\t{;}\\
~~~~\vdots\\[2mm]
\t{endmodule}
\end{array}$
\bigskip
The semantics of such a module is an IL module with the same name and parameters.
The \t{wire} and \t{reg} declarations become \LOCAL{} declarations.
Functions are converted to IL initialised local variables. For example:
{\baselineskip13pt\begin{alltt}
function f(a,b,c,d);
begin
f = a;
if (b)
begin
if (c) f = d; else f = !d;
end
end
\end{alltt}}
generates:
{\baselineskip13pt\begin{alltt}
\LOCAL f.
\INIT f = \(\lambda\)(a,b,c,d). b ? (c ? d : \(\neg\)d) : a
\end{alltt}}
Tasks are elaborated by replacing each invocation by the appropriate instance
of the body (i.e.~call-by-name).
Continuous assignments are converted to zero-delay assignments,
i.e.~equations, as described in Section~\ref{contassign}.
\t{always}-blocks are converted to IL; see the examples in
Section~\ref{statements}.
\subsubsection*{Examples}
The examples in this section were partially done by hand and
could contain errors.
The first example has a continuous assignment, and illustrates
a situation when simulation and synthesis can disagree.
{\baselineskip12pt\begin{alltt}
module BadXL(clk, in, out);
input clk, in;
output out;
reg out, r;
wire w; \(\vspace{0mm}\)
assign w = r; \(\vspace{0mm}\)
always @ (posedge clk) begin
r = in;
out = w;
end \(\vspace{0mm}\)
endmodule
\end{alltt}}
This has semantics:
\vspace{-1mm}
{\baselineskip12pt\begin{alltt}
\MODULE \(\con{BadXL}\) (clk,in,out); \(\vspace{0mm}\)
\LOCAL r w. \(\vspace{0mm}\)
w = r; \(\vspace{0mm}\)
rise clk -> (r \assign in; out = w) \(\vspace{0mm}\)
\END
\end{alltt}}
\vspace{-1mm}
which is semantically equivalent to:
\vspace{-1mm}
{\baselineskip12pt\begin{alltt}
\MODULE \(\con{BadXL}\) (clk,in,out); \(\vspace{0mm}\)
rise clk -> out \assign in \(\vspace{0mm}\)
\END
\end{alltt}}
\vspace{-1mm}
An example using tasks is the following (unrealistic) device to
naively compute
the factorial function.
This uses a task {\tt{Mult}} to perform multiplication by adding the
first argument (\t{InOut}) to itself the second argument (\t{In})
number of times. The result is thus returned in the first argument.
\vspace{-1mm}
{\baselineskip12pt\begin{alltt}
module Fact (Start,Inp,clk,FACT,BUSY); \(\vspace{0mm}\)
reg N; \(\vspace{0mm}\)
task Mult(InOut,In);
reg X Y;
always @(posedge clk)
begin
X = InOut; Y = In;
while (Y > 1)
begin
@(posedge clk)
InOut = InOut+X; Y = Y-1;
end
end
endtask; \(\vspace{0mm}\)
always @(posedge clk)
if (Start)
begin N = Inp;
FACT = 1; BUSY = 1;
while (N>1)
begin
Mult(FACT,N);
N = N-1;
end
BUSY = 0;
end \(\vspace{0mm}\)
endmodule
\end{alltt}}
This has semantics:
{\baselineskip13pt\begin{alltt}
\MODULE \(\con{Fact}\) (Start,Inp,clk,FACT,BUSY);
\LOCAL pc X Y N.
\INIT pc = 0;
pc = 0 \C rise clk -> (pc \assign Start ? (Inp>1?1:0) : 0;
X \assign X;
FACT \assign Start ? 1 : FACT;
Y \assign Y;
N \assign Start ? Inp : N;
BUSY \assign Start ? (Inp>1?1:0) : BUSY);
pc = 1 \C rise clk -> (pc \assign N>1 ? 2 : (N-1>1?1:0);
X \assign FACT;
FACT \assign FACT;
Y \assign N;
N \assign N>1 ? N : N-1;
BUSY \assign N>1 ? BUSY : (N-1>1?BUSY:0));
pc = 2 \C rise clk -> (pc \assign Y-1>1 ? 2 : (N-1>1?1:0)
X \assign X;
FACT \assign FACT+X;
Y \assign Y-1;
N \assign Y-1>1 ? N : N-1;
BUSY \assign Y-1>1 ? BUSY : (N-1>1?BUSY:0))
\END
\end{alltt}}
The examples here are intended to illustrate how IL is used to give
the synthesis semantics of Verilog. A more systematic presentation
will be given as a later deliverable.
\section{Semantics of synthesizable VHDL}
\subsection{VHDL processes}
In VHDL, the primary elements to model a state based system are
{\em processes}. The body of a process roughly consists of a
{\em process declarative part} and a
{\em sequential statement part}. Using a BNF style grammar,
processes are defined as
\bigskip
$\begin{array}{ccll}
\mbox{\em process} & {\rm ::=} & [ \mbox{\ process\_label\ } :\mbox{\ } ] \mbox{\tt
\ process\ } [ (\mbox{\em \ sensitivity\_list\ }) ]
\\
& & \mbox{\ \ \ \ \ }\mbox{process\_declarative\_part} \\
& & \mbox{\tt begin} \\
& & \mbox{\ \ \ \ \ }\mbox{process\_statement\_part} \\
& & \mbox{\tt end process\ } [ \mbox{\ process\_label\ } ];\\
\mbox{\em sensitivity\_list} & {\rm ::=} & \mbox{list of signal names}
\end{array}$
\bigskip
\noindent In the process delarative part, local items such as variables
and constants can be defined.
The sequential statement part is a list of statements and
is activated in response to changes in state.
Processes that are activated at the same time run concurrently.
A process in VHDL is the counterpart to an {\tt always} construct in
Verilog. Roughly speaking, the Verilog program
{\baselineskip13pt\begin{alltt}
always
begin
\Math{P};
end
\end{alltt}}
\noindent is equivalent to the VHDL program
{\baselineskip13pt\begin{alltt}
p0 : process
begin
\Math{P};
end process p0
\end{alltt}}
\noindent While in Verilog, timing controls are always expressed with the {\tt @}
operator, VHDL provides two different ways to control time.
\begin{itemize}
\item Control by {\em sensitivity lists}
\item Control by {\em wait statements}
\end{itemize}
\noindent In VHDL, a sensitivity list can be attached to each process and
consists of one or more signal names. Whenever a change occurs in some
signal belonging to the sensitivity list of a process $p$, the
sequential statement part of $p$ is executed.
VHDL processes with no or empty sensitivity lists are treated in a
special way: They are always executed
and can only be suspended by a wait statement.
A process $p$ with sensitivity list $(V_1,\ldots,V_n)$ has the same
functionality as Verilog's
\begin{center}
{\tt always@ ($V_1$ or $\ldots$ or $V_n$)}
\end{center}
\noindent construct,
where $V_1,\ldots,V_n$ are restricted to be {\em change of value} event
expressions, i.e., $V_1,\ldots,V_n$ specify the names of signals.
Thus sensitivity lists in VHDL are less expressive as
event expressions in Verilog. For example, it is not possible
to express {\tt @posedge} or {\tt @negedge} timing controls.
Wait statements are the second
possibility to express timing control in VHDL and are more expressive
than sensitivity lists.
A wait statement is defined as
\bigskip
$\begin{array}{ccll}
\mbox{\em wait\_statement} & {\rm ::=} & \mbox{\tt wait\ } [
\mbox{\em sensitivity\_clause} ] [ \mbox{\em condition\_clause} ] \\ % [
% \mbox{\em timeout_clause} ] ; \\
\mbox{\em sensitivity\_clause} & {\rm ::=} & \mbox{\tt on\ } \mbox{\em sensitivity\_list}
\\
\mbox{\em sensitivity\_list} & {\rm ::=} & \mbox{list of signal names}
\\
\mbox{\em condition\_clause} & {\rm ::=} & \mbox{\tt until\ } \mbox{condition}
\end{array}$
\bigskip
\noindent Whenever a process $p$ is executed and a wait statement is
processed, $p$ will be
suspended. The sensitivity list of the wait statement specifies a set
of signals to which the process is sensitive while being inactive.
Whenever a signal in the sensitivity list gets changes, the {\em
condition clause} is evaluated. If the condition is true, the
execution of the process is continued. Otherwise, the process
resuspends.
Using conditional wait statements, all event controls of
Verilog can be expressed.
The event control {\tt @posedge clk} can be written as
{\baselineskip13pt\begin{alltt}
process
begin
wait on clk until clk = '0';
wait on clk until clk = '1';
...
end process;
\end{alltt}}
The two wait statements can only be passed if the value of clock
switches from zero to one. Another possibility to detect rising
edges is
{\baselineskip13pt\begin{alltt}
process (clk)
begin
wait on clk until clk = '1';
...
end process;
\end{alltt}}
Here, a sensitivity list is combined and a wait statement are
combined.
Unlike in the first program fragment, the sensitivity list is not
empty and therefore the process is invoked if and only if a signal
change occured on \t{clk}.
The wait statement then forces the process to wait until \t{clk}
rises.
The next possibility is probably the most common way for detecting
edges (especially in synthesizable VHDL) and makes use of the predefined
function \t{RISING\_EDGE}:
{\baselineskip13pt\begin{alltt}
process
begin
wait on clk until RISING\_EDGE(clk);
...
end process;
\end{alltt}}
\noindent Similar to \t{@posedge clk}, the Verilog event control
{\tt @negedge clk} can be expressed as
{\baselineskip13pt\begin{alltt}
process
begin
wait on clk until clk = '1';
wait on clk until clk = '0';
...
end process;
\end{alltt}}
\noindent or
{\baselineskip13pt\begin{alltt}
process (clk)
begin
wait on clk until clk = '0';
...
end process;
\end{alltt}}
\noindent or
{\baselineskip13pt\begin{alltt}
process
begin
wait on clk until FALLING\_EDGE;
...
end process;
\end{alltt}}
\noindent \t{RISING\_EDGE}$(s)$ and \t{FALLING\_EDGE}$(s)$
are predefined functions evaluating to true iff $s$ is currently
rising or falling, respectively.
In terms of expressiveness, wait statements in VHDL subsume a
sensitivity lists. Each VHDL program of the form
{\baselineskip13pt\begin{alltt}
p0 : process (x,y,z)
begin
\Math{P}
end process p0
\end{alltt}}
can be rewritten as
{\baselineskip13pt\begin{alltt}
p0 : process
begin
wait on (x,y,z) until ( x'EVENT or y'EVENT or z'EVENT);
\Math{P}
end
\end{alltt}}
\t{EVENT} is another predefined VHDL construct. \t{x'EVENT} is true if
and only if an event (signal change) occured on \t{x}.
Using the \t{EVENT} construct, the functions
\t{RISING\_EDGE} and \t{FALLING\_EDGE} can be expressed naturally as
\begin{eqnarray*}
\mbox{\t{RISING\_EDGE}\ } s & = & s'\mbox{\t{EVENT}}\mbox{\ \t{and}\ } s = \mbox{'1'}\\
\mbox{\t{FALLING\_EDGE}\ } s & = & s'\mbox{\t{EVENT}}\mbox{\ \t{and}\ } s = \mbox{'0'}
\end{eqnarray*}
\noindent In the synthesizable subset of VHDL, wait-statements can
only be used in a very restricted way.
Each process is only allowed to
have one single wait-statement which has to occur as the first command
in the sequential statement part.
No local sensitivity lists are allowed for wait statements.
Thus, edge detection must be realized with functions
\t{RISING\_EDGE} and \t{FALLING\_EDGE}, or the corresponding
counterparts based on the \t{EVENT} expression.
As a result, the expressiveness of the wait
construct is cut down to roughly the same expressiveness as provided by
Verilog's timing controls.
\subsection{VHDL semantics by example}
\label{examplesection}
Similar to Section \ref{verilog}, a sematics for synthesizable VHDL is
outlined by example.
\subsubsection*{Example 1}
As an introductory example, let us first consider the following
VHDL program:
{\baselineskip13pt\begin{alltt}
signal a,b : bit;
signal pc : bit := 0;
p0 : process
begin
wait on clk until RISING_EDGE clk;
case pc of
when 0 =>
pc <= 1;
a <= 0;
when 1 =>
pc <= 0;
b <= a;
end case;
end process p0;
\end{alltt}}
\noindent Expressing the {\em case}-statement as a nested
construct of if-then-else operators $( X ? Y : Z)$,
the program has the IL sematics
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
init pc = 0;
rise clk -> (pc = 0 ? (pc \assign 1; a \assign 0; b \assign b)
: (pc = 1 ? (pc \assign 0; a \assign a; b \assign a)
: 0))
\end{alltt}}
Exploiting the equivalence
{\baselineskip13pt\begin{alltt}
rise \Math{x} -> (\Math{A} ? \Math{B} : \Math{C}) = \Math{A} ? (rise \Math{x} -> \Math{B}) : (rise \Math{x} -> \Math{C})
\end{alltt}}
\noindent this is equivalent to
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
init pc = 0;
pc = 0 ? rise clk -> (pc \assign 1; a \assign 0; b \assign b)
: (pc = 1 ? rise clk -> (pc \assign 0; a \assign a; b \assign a)
: 0)
\end{alltt}}
\noindent Using the rule
{\baselineskip13pt\begin{alltt}
(\Math{A} ? \Math{B} : \Math{C}) = (\Math{A} \C \Math{B} ; \Neg \Math{A} \C \Math{C}))
\end{alltt}}
\noindent for rewriting the {\em if-then-else}
construct with {\em conjuction} (\t{;}) and {\em implication} (\C),
the program can be written as
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
init pc = 0;
(pc = 0) \C rise clk -> (pc \assign 1; a \assign 0; b \assign b);
\Neg(pc = 0) \C
( (pc = 1) \C rise clk -> (pc \assign 0; a \assign a; b \assign a);
\Neg(pc = 1) \C 0)
\end{alltt}}
\noindent Since pc has type {\em bit}, we can conclude
{\baselineskip13pt\begin{alltt}
\Neg(pc = 0) = (pc = 1)
\Neg(pc = 1) = (pc = 0)
\end{alltt}}
\noindent and rewriting these equations result in
{\baselineskip13pt\begin{alltt}
local pc.
init pc = 0;
pc = 0 \C rise clk -> (pc \assign 1; a \assign 0; b \assign b);
pc = 1 \C
((pc = 1) \C rise clk -> (pc \assign 0; a \assign a; b \assign a);
(pc = 0) \C 0)
\end{alltt}}
which is equivalent to
{\baselineskip13pt\begin{alltt}
local pc.
init pc = 0;
pc = 0 \C rise clk -> (pc \assign 1; a \assign 0; b \assign b);
pc = 1 \C rise clk -> (pc \assign 0; a \assign a; b \assign a)
\end{alltt}}
\noindent This is exactly the result we got for the Verilog example
{\baselineskip13pt\begin{alltt}
always @(posedge clk) begin a = 0; @(posedge clk) b = a; end
\end{alltt}}
\noindent presented in Section \ref{examplesection}. Thus, both programs are
equivalent.
\subsubsection*{Example 2}
The next example is the VHDL equivalent to Verilog-example 3:
{\baselineskip13pt\begin{alltt}
signal pc : [0..2];
signal total, data : integer;
p0 : process
begin
wait until RISING_EDGE(clk);
case pc of
when 0 =>
pc <= 1;
total <= data;
when 1 =>
pc <= 2;
total <= total+data;
when 2 =>
pc <= 0;
total <= total+data;
end case;
end process p0;
\end{alltt}}
which has semantics
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
rise clk ->
(pc = 0 \C (pc \assign 1; total \assign data);
pc = 1 \C (pc \assign 2; total \assign total+data);
pc = 2 \C (pc \assign 0; total \assign total+data))
\end{alltt}}
or
{\baselineskip13pt\begin{alltt}
\LOCAL pc.
pc = 0 \C rise clk -> (pc \assign 1; total \assign data);
pc = 1 \C rise clk -> (pc \assign 2; total \assign total+data);
pc = 2 \C rise clk -> (pc \assign 0; total \assign total+data)
\end{alltt}}
which is equivalent.
\subsubsection*{Example 3}
{\baselineskip13pt\begin{alltt}
signal a,b,c : integer;
p0 : process (b,c)
begin
a <= b+c;
end process p0;
\end{alltt}}
\noindent has semantics
{\baselineskip13pt\begin{alltt}
@((edge b) or (edge c)) (a \assign b+c)
\end{alltt}}
or
{\baselineskip13pt\begin{alltt}
a = b+c
\end{alltt}}
\noindent Here, a zero-delay assignment can be chosen
since the sensitivity list covers all
signals occuring on a right side of a signal
assignment.
\subsubsection*{Example 4}
{\baselineskip13pt\begin{alltt}
signal a,b,c : integer;
p0 : process (b)
begin
a <= b+c;
end process p0;
\end{alltt}}
The only difference to Example 3 is the sensitivity list
where signal {\tt c} has been removed.
Both programs are not equivalent as it was the case for the
corresonding Verilog examples presented in Section \ref{examplesection}.
The IL semantics is given by
{\baselineskip13pt\begin{alltt}
@(edge b) (a \assign b+c)
\end{alltt}}
We now give three examples of concurrent processes:
\subsubsection*{Example 5}
{\baselineskip13pt\begin{alltt}
signal a,b,c;
p0 : process
begin
wait on clk until RISING_EDGE(clk)
a <= c;
end process p0;
p1 : process
begin
wait on clk until FALLING_EDGE(clk)
b <= a;
end process p0;
\end{alltt}}
\noindent This VHDL program assigns the value of \t{c} to \t{a} at each
rising edge. On the next falling edge, the value of \t{a} is then
assigned to \t{b}. Since \t{p0} and \t{p1} cannot pass their
wait statements simultaniously, the IL representation can be
written as
{\baselineskip13pt\begin{alltt}
rise clk -> a \assign c;
fall clk -> b \assign a
\end{alltt}}
\subsubsection*{Example 6}
\noindent In this example, both wait statements are passed simultaniously
and the semantics can only be given with respect to a resolution
function.
{\baselineskip13pt\begin{alltt}
signal a,b,c;
p0 : process
begin
wait on clk until clk = '1'
a <= c;
end process p0;
p1 : process
begin
wait on clk until cls = '1'
a <= b;
end process p0;
\end{alltt}}
\noindent In this example, signal \t{a} has two drivers, namely \t{c}
(from process \t{p0}) and \t{b} (from process \t{p1}).
In VHDL, a resolution function has to be provided, giving priority
to one of all possible drivers.
Assuming a resolution function that executes \t{a <= b} after
\t{a <= c}, the IL semantics is given as
{\baselineskip13pt\begin{alltt}
@(clk) (a \assign b)
\end{alltt}}
\subsubsection*{Example 7}
\noindent Now, delta-delay comes into play:
{\baselineskip13pt\begin{alltt}
signal a,b,c;
p0 : process (clk)
begin
wait on clk until clk = '1'
a <= c;
end process p0;
p1 : process (clk)
begin
wait on clk until cls = '1'
b <= a;
end process p0;
\end{alltt}}
\noindent Whenever \t{clk} changes to \t{1}, \t{a} is assigned the value
of \t{c} and \t{b} is assigned the value of \t{a}.
As the asignment strategy of VHDL is based on delta delays,
the values of the signals on the right-hand sides
remain constant until all assignments have been processed. Only then,
the signal values are updated simultaniously.
Thus, the semantics of this program is
{\baselineskip13pt\begin{alltt}
rise clk -> (a \assign c);
rise clk -> (b \assign a)
\end{alltt}}
\noindent Note that the VHDL program above is {\em not} equivalent to the
Verilog program
{\baselineskip13pt\begin{alltt}
always @(posedge clk) begin a = c; b = a; end
\end{alltt}}
\noindent since in Verilog, \t{a} is updated before processing the second
assignment and therefore has semantics
{\baselineskip13pt\begin{alltt}
rise clk -> (a \assign c; b \assign c)
\end{alltt}}
\noindent However, the Verilog program
{\baselineskip13pt\begin{alltt}
always @(posedge clk) a = c; b = a; end
\end{alltt}}
\noindent has a counterpart in VHDL when defining \t{a} of type
{\em variable} instead of type {\em signal}:
{\baselineskip13pt\begin{alltt}
signal b,c;
p0 : process (clk)
variable a;
begin
wait on clk until clk = '1'
a = c;
b <= a;
end process p0;
\end{alltt}}
\noindent Here, variable \t{a} is immediately assigned the value of signal
{\tt c} and therefore, signal \t{b} will also become equal to
\t{c}. Thus, the semantics in IL also is
{\baselineskip13pt\begin{alltt}
rise clk -> (a \assign c; b \assign c)
\end{alltt}}
\newpage
\addcontentsline{toc}{section}{References}
\bibliographystyle{plain}
\bibliography{IL,crossref,literatur}
\end{document}