\documentclass{article}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\usepackage[dvips]{graphicx}
\usepackage[usenames]{color}
\usepackage{amsmath,color}
\usepackage{amsfonts}
\usepackage{amscd}
\usepackage{amsthm}
% \usepackage{mypptaaai}
\usepackage{ulem}
\input{macro2.tex}
%\usepackage{/home/john/work/tex/sty/mypptaaai}
%\input{/home/john/work/tex/macros/macro2.tex}
%\input{accellera_macros.tex}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Example  figure
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\begin{figure}[thb]
%\begin{center}
%\includegraphics[scale=0.45]{near-sym-0.eps}
%\end{center}
%\begin{quote}
%\caption{Illustration of Example 3(a) with $M$ on the left and 
%$M^G$ on the right.  $M$ is strongly virtually 
%symmetric with respect to $G$.}
%\end{quote}
%\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Local defs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\def\bbb{{\mathbb B}}
\def\bbf{{\mathbb F}}
\def\bbn{{\mathbb N}}
\def\bbz{{\mathbb Z}}
\def\meet{\sqcap }
\def\join{\sqcup }
\def\refines{\sqsubseteq }
\def\coarsens{\sqsupseteq }
\def\tprod{{\textstyle \prod}}
\def\tsum{{\textstyle \sum}}
\def\Ra{{\Rightarrow}}
\def\cl{{\rm cl}}

\def\ab{{\rm ab}}

\def\myand{{\rm and}}
\def\myor{{\rm or}}

\def\loc{{\rm loc}}

\def\dep{{\rm dep}}
\def\tran{{\rm tran}}
\def\tdep{{\rm tdep}}
\def\endd{{\it end}}

\def\status{{\it status}}
\def\pass{{\rm pass}}
\def\fail{{\rm fail}}

\def\flash{{\it flash}}
\def\light{{\it light}}
\def\red{{\tt red}}
\def\green{{\tt green}}
\def\neutral{{\tt neutral}}

\def\start{{\rm start}}
\def\look{{\rm look}}
\def\finish{{\rm finish}}

\def\halt{{\rm halt}}
\def\continue{{\rm continue}}
\def\pc{{\it pc}}

\def\base{{\rm base}}
\def\stab{{\rm stab}}
\def\dom{{\rm dom}}
\def\support{{\rm support}}
\def\Sym{{\it Sym}}

\def\ttlp{{\text{\tt(}}}
\def\ttrp{{\text{\tt)}}}
\def\ttlb{{\text{\tt[}}}
\def\ttrb{{\text{\tt]}}}
\def\ttcl{{\text{\tt:}}}
\def\ttcm{{\text{\tt,}}}
\def\ttsc{{\text{\tt;}}}
\def\tteq{{\text{\tt=}}}
\def\ttone{{\text{\tt 1}}}
\def\ttzero{{\text{\tt 0}}}

\def\ttalways{{\text{\tt always}}}
\def\ttinitial{{\text{\tt initial}}}

%\def\ttassert{{\text{\tt assert}}}
\def\ttassert{{\text{\tt assert property}}}

%\def\ttdisable{{\text{\tt accept}}}
\def\ttdisable{{\text{\tt disable iff}}}

\def\ttnot{{\text{\tt not}}}

%\def\ttimp{{\text{\tt=>}}}
\def\ttimp{{\text{\tt|->}}}

\def\ttnonoverlapimp{{\text{\tt|=>}}}

\def\ttat{{\text{\tt @(}}}

%\def\ttconcat{{\text{\tt;}}}
\def\ttconcat{{\text{\tt \#\#1}}}

%\def\ttmulticlockconcat{{\text{\tt;}}}
\def\ttmulticlockconcat{{\text{\tt \#\#}}}

%\def\ttfuse{{\text{\tt;[0]}}}
\def\ttfuse{{\text{\tt \#\#0}}}

%\def\ttor{{\text{\tt||}}}
\def\ttor{{\text{\tt or}}}

%\def\ttand{{\text{\tt\&\&}}}
\def\ttand{{\text{\tt and}}}

\def\ttfirstmatch{{\text{\tt first\_match}}}

%\def\ttnullrep{{\text{\tt *[0]}}}
\def\ttnullrep{{\text{\tt [*0]}}}

%\def\ttrep{{\text{\tt *[1:inf]}}}
\def\ttrep{{\text{\tt [*1:\$]}}}

%\def\ttnullorrep{{\text{\tt *[0:inf]}}}
\def\ttnullorrep{{\text{\tt [*0:\$]}}}

%\def\ttlrep{{\text{\tt *[}}}
\def\ttlrep{{\text{\tt [*}}}

%\def\ttinf{{\text{\tt inf}}}
\def\ttinf{{\text{\tt \$}}}

%\def\ttludelay{{\text{\tt [}}}
\def\ttludelay{{\text{\tt \#\#[}}}

%\def\ttlbdelay{{\text{\tt ;[}}}
\def\ttlbdelay{{\text{\tt \#\#[}}}

%\def\ttlcount{{\text{\tt *=[}}}
\def\ttlcount{{\text{\tt [*=}}}

%\def\ttlnthevent{{\text{\tt *->[}}}
\def\ttlnthevent{{\text{\tt [*->}}}

\def\ttintersect{{\text{\tt intersect}}}
\def\ttwithin{{\text{\tt within}}}
\def\ttthroughout{{\text{\tt throughout}}}



\def\ttnext{{\text{\tt +(1)}}}
\def\ttif{{\text{\tt if }\ttlp}}


\def\tight{{| \hspace{-0.06in} \equiv}}

\def\bft{{{\bf t}}}
\def\bff{{{\bf f}}}

\def\sample{{\it sample\/}}
\def\block{{\it block\/}}
\def\flow{{\it flow\/}}

\def\ttended{{\text{\tt .ended}}}
\def\ttmatched{{\text{\tt .matched}}}
\def\ttpast{{\text{\tt \$past}}}
\def\ttrose{{\text{\tt \$rose}}}
\def\ttfell{{\text{\tt \$fell}}}
\def\ttstable{{\text{\tt \$stable}}}

\def\myspace{{\,}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\title{Proposal for formal semantics for property and sequence instances}

\author{SV-AC}


\maketitle

% \begin{abstract}
% \begin{quote}
% \end{quote}
% \end{abstract}

%\noindent{\bf Keywords:}

\renewcommand{\thefootnote}{\fnsymbol{footnote}}
\renewcommand{\thefootnote}{\arabic{footnote}}
\setcounter{footnote}{0}


%-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=--

Replace at section F.1\\\\\\
%%
%%
\begin{description}
\item[c)]
The abstract syntax simplifies the assertion language by eliminating some features that tend to
encumber the definition of the formal semantics.
\begin{description}
\item[1)]
    The abstract syntax eliminates local variable declarations. The semantics of local variables is 
    written with implicit types.
\item[2)]
    The abstract syntax eliminates instantiation of sequences and properties. The semantics of an
    assertion with an instance of a sequence or nonrecursive property is the same as the semantics
    of a related assertion obtained by replacing the sequence or nonrecursive property instance with
    an explicitly written sequence or property. The explicit sequence or property is obtained from
    the body of the associated declaration by substituting actual arguments for formal arguments. A
    separate subclause defines the semantics of instances of recursive properties in terms of the
    semantics of instances of nonrecursive properties.
\item[3]
    The abstract syntax does not allow implicit clocks. Clocking event controls must be applied
    explicitly in the abstract syntax.
\item[4]
    The abstract syntax does not allow explicit procedural enabling conditions for assertions. Procedural
    enabling conditions are utilized in the semantics definition (see 4.3.1), but the method
    for extracting such conditions is not defined in this annex.
\end{description}
\end{description}
In order to use this annex to determine the semantics of a SystemVerilog assertion, the assertion must first
be transformed into an enabling condition together with an assertion in the abstract syntax. For assertions
that do not involve recursive properties, this transformation involves eliminating sequence and nonrecursive
property instances by substitution, eliminating local variable declarations, introducing parentheses, determining
the enabling condition, determining implicit or inferred clocking event controls, and eliminating
redundant clocking event controls. For example, the following SystemVerilog assertion\\\\
%
{\sf
\hspace*{12mm}sequence {\it s(x,y); x \#\#1 y;} endsequence\\
\hspace*{12mm}sequence {\it t(z); @(c) z[*1:2] \#\#1 B;} endsequence\\
\hspace*{12mm}always {\it @(c) if (b)} assert property {\it (s(A,B) $|=>$ t(A));}
}\\\\
%
is transformed into the enabling condition ``{\it b}'' together with the assertion\\\\
%
{\sf
\hspace*{12mm}always @(c) assert property {\it ((A \#\#1 B) $|=>$ (A[*1:2] \#\#1 B))}
}\\\\
%
%
in the abstract syntax.
If the SystemVerilog assertion involves instances of recursive properties, then the transformation replaces
these instances with placeholder functions of the actual arguments. The semantics of an instance of a recursive
property is defined in terms of associated nonrecursive properties in F.5. Once the semantics of the
recursive property instances is understood, the placeholder functions are treated as properties with this
semantics. Then the ordinary definitions can be applied to the transformed assertion in the abstract syntax
together with placeholder functions.
\ \\\\with\\\\\\
\begin{description}
\item[c)]
The abstract syntax simplifies the assertion language by eliminating some features that tend to
encumber the definition of the formal semantics.
\begin{description}
\item[1)]
    The abstract syntax eliminates local variable declarations. The semantics of local variables is 
    written with implicit types.
\item[2)] The abstract syntax eliminates instantiation of sequences
    and properties. The semantics of an assertion with {\color{red}\sout{an}} instance{\color{blue}s} of
    a sequence or nonrecursive property is the same as the semantics
    of a related assertion obtained by replacing the sequence or
    nonrecursive property instance with an explicitly written sequence
    or property. {\color{red} \sout{The explicit sequence or property is
    obtained from the body of the associated declaration by
    substituting actual arguments for formal arguments. A separate
    subclause defines the semantics of instances of recursive
    properties in terms of the semantics of instances of nonrecursive
    properties.}} {\color{blue} The definition of rewriting an assertion without 
    property and sequence instances is given in clause .%\ref{sect:rewrite_sub}
    {\color{green}[Note to the editor: add link to the new sub section, which
    is described in the next item]}.}
{\color{blue}
%
    The semantics of an assertion that have recursive properties
    instances is defined in clause {\bf F.5} in terms of an infinite
    series of assertions with no instances of recursive properties,
    but possibly with instances of nonrecursive properties and
    sequences.  The semantics of each assertion in the series is
    defined as the semantics for other assertions with no instances of
    recursive properties.}
%
%
%
%    An Instance
%    of a recursive property shall be considered as Boolean
%    propositions whose truth value is {\bf true} at a specific letter
%    at a specific computation, iff the truth values of all of the
%    nonrecursive properties described in {\bf F.5}. is {\bf true} at
%    these letter and computation. }
%
\item[3]
    The abstract syntax does not allow implicit clocks. Clocking event controls must be applied
    explicitly in the abstract syntax.
\item[4]
    The abstract syntax does not allow explicit procedural enabling conditions for assertions. Procedural
    enabling conditions are utilized in the semantics definition (see 4.3.1), but the method
    for extracting such conditions is not defined in this annex.
\end{description}
\end{description}
In order to use this annex to determine the semantics of a
SystemVerilog assertion, the assertion must first be transformed into
an enabling condition together with an assertion in the abstract
syntax. For assertions that do not involve recursive properties, this
transformation involves eliminating sequence and nonrecursive property
instances 
{\color{blue} using the rewrite algorithm}
{\color{red}\sout{by substitution, eliminating local
variable declarations, introducing parentheses}}, 
determining the
enabling condition, determining implicit or inferred clocking event
controls, and eliminating redundant clocking event controls. For
example, the following SystemVerilog assertion\\\\
%
{\color{blue}
{\sf
\hspace*{8mm}property p1({\it logic [0:2] a1, property a2}); {\it (a1 == 3'b010) $|=>$ a2;}endproperty\\
\hspace*{8mm}property p2({\it a1, logic [1:3] a2});{\it  a1 \#\#1 (a2 == 3'b010);} endproperty\\
\hspace*{8mm}always {\it @(c) if (b)} assert property ({\it p1(g1, p2(g2, g3))});\\\\
}
%
is transformed into the enabling condition ``{\it b}'' together with the assertion\\\\
%
{\sf
always @(c) assert property  ({\it (\$var((logic [2:0])'g1) == 3'b010) $|=>$\\\hspace*{42mm} \$var({\it g1}) \#\#1 (\$var((logic [1:3])'g3) == 3'b010)});\\\\
}}
{\color{red}\sout{
\hspace*{12mm}sequence {\it s(x,y); x \#\#1 y;} endsequence\\
\hspace*{12mm}sequence {\it t(z); @(c) z[*1:2] \#\#1 B;} endsequence\\
\hspace*{12mm}always {\it @(c) if (b)} assert property {\it (s(A,B) $|=>$ t(A));}
\\\\
%
is transformed into the enabling condition ``{\it b}'' together with the assertion\\\\
%
{\sf
\hspace*{12mm}always @(c) assert property {\it ((A \#\#1 B) $|=>$ (A[*1:2] \#\#1 B))}
}\\\\
}}
%
%
{\color{red}\sout{in the abstract syntax.  If the SystemVerilog assertion involves
instances of recursive properties, then the transformation replaces
these instances with placeholder functions of the actual
arguments. The semantics of an instance of a recursive property is
defined in terms of associated nonrecursive properties in
F.5.
% {\color{blue}The truth\footnote{The truth value is reflected by
%the $\models$ relation}.value of a nonrecursive property associated
%with the recursive property is the truth value of the sub {\tt
%property\_expr} resulted from flattening an instance of the
%nonrecursive property in the place of the recursive one}. 
Once the
semantics of the recursive property instances is understood, the
placeholder functions are treated as properties with this
semantics. Then the ordinary definitions can be applied to the
transformed assertion in the abstract syntax together with placeholder
functions.}}



{\color{green}Note to the editor: Add the following section after F.3.1}

\appendix

\subsubsection{Rewriting property and sequence instances}
\label{sect:rewrite_sub}
%
This section describes an algorithm for rewriting a property\_spec
that contains property and/or sequence instances. The result of the
algorithm is an assertion with one ``flat'' property expression. The
semantics of a hierarchical property expression is then defined to be
the semantics of the flat property\_spec resulting from the
rewriting algorithm. In particular, if the result is illegal, then so
is the source.

For the rewriting algorithm, an auxiliary function {\it\$var()} is
defined as follows. The function {\tt \$var} may be applied on every
system verilog expression. For every system verilog expression {\it
e}, \$var({\tt e}) is the expression {\tt e} with the exception that
every operation that is allowed on a variable with the same type of
{\it e} is allowed on {\tt \$var({\it e})}.

In particular, any operation that is allowed on a declared property or
declared sequence, is allowed on {\it \$var} applied on a property
expression or a sequence expression respectively. Note that for some
expressions {\it e}, there are operations that are allowed on
variables {\it v} with the same type but not on {\it e}. For example,
let {\tt a, b} be variables of type {\tt logic [0:1]}, let {\tt v} be
a variable of type {\tt logic [0:3]}, and {\it e} the expression {\tt
(logic [0:3])'\{a,b\}}. Then, the result of applying a bit select
operation on {\tt v} {\tt v[1:2]} is a valid expression, but {\tt
(logic [3:0])'\{a,b\}[0:1]} is not. Introducing the \$var function
enables usage of the form {\tt\$var((logic [3:0])'\{a,b\})[1:2]}. For
expressions with undefined type, \$var does not enable additional
operations.  \$var is not a system verilog function and its only use
is in the rewriting algorithm.\\\\
%
%---------------------------------------------------------------
{\bf The rewrite algorithm}\\
Given a property\_spec expression inside an assertion declaration:\\\\
% 
{\sf
While there are property instances in the property\_spec do:\\
begin\\
\hspace*{6mm} Select an arbitrary property instance {\tt P}\\
\hspace*{6mm} flatten\_property({\tt P})\\
end\\\\
%
While there are sequence instances in the property\_spec do:\\
begin\\
\hspace*{6mm} Select an arbitrary sequence instance {\tt R}\\
\hspace*{6mm} flatten\_sequence({\tt R})\\
end\\\\
%
%
%
flatten\_property({\tt P})\\
begin
\begin{enumerate}
\item
    Create a copy {\tt P'} of the declaration of {\tt P}.
%
\item
For every local variable declared in {\tt P'}, make its identifier 
unique.
% with respect to the names of the local variables declared in
%the property\_exper of the assertion.
%
%
%b. If f is on the left hand side of an assignment, replace the
%   expression e, that is on the right hand side of the assignment
%   with "t'(e)" (cast e to type t).
%
%%%In case that the casting is illegal, report an error.
%
\item
Replace every formal argument {\tt f} in the  property\_expr
of {\tt P'} that is not on the left hand side of an assignment, with
{\tt \$var(f)}.

\item
For every occurrence of a typed formal argument {\tt f} of {\tt P'}
 %with a simple type {\tt t}[see A.2.2.1] 
in the body of {\tt P'},
replace {\tt f} with {\tt (t)'f} (cast {\tt f} to type {\tt t}). See
cast definition at ({\color{blue} 4.14}).
%Occurrences of formal
%arguments that are not on the left hand side of an assignment, are
%wrapped in parenthesis.
%

\item
Replace every formal argument {\tt f} in the  property\_expr
of {\tt P'}, with {\tt (a)} where {\tt a} is the corresponding actual argument
expressions in the instance of {\tt P}.

\item
%The third step includes the following steps:
%
%1. copy all declarations of local variables of p2 to an appropriate
%   place in p1.
%
In the property\_expr of the assertion, replace the instance of {\tt P} with
   property\_expr of {\tt P'} wrapped in parenthesis.
\end{enumerate}
end\\\\\\
%
%
flatten\_sequence({\tt R})\\
begin
\begin{enumerate}
\item
    Create a copy {\tt R'} of the declaration of {\tt R}.
%
%b. If f is on the left hand side of an assignment, replace the
%   expression e, that is on the right hand side of the assignment
%   with "t'(e)" (cast e to type t).
%
%In case that the casting is illegal, report an error.
%
\item
For every local variable declared in {\tt R'}, make its identifier
unique.
% with respect to the names of the local variables declared in
%the property\_expr of the assertion.
%
%
\item
Replace every formal argument {\tt f} in the sequence\_expr
of {\tt R'} that is not on the left hand side of an assignment, with
{\tt \$var(f)}.
%
\item
For every occurrence of a typed formal argument {\tt f} of {\tt R'}
%with a simple type {\tt t}[see A.2.2.1] 
in the sequence\_expr of {\tt R'},
replace {\tt f} with {\tt (t)'f} (cast {\tt f} to type {\tt t}). See
cast definition at ({\color{blue} 4.14}).

%
%
%Occurrences of formal
%arguments that are not on the left hand side of an assignment, are
%wrapped in parenthesis.
%
\item
Replace every formal argument {\tt f} in the  sequence\_expr
of {\tt R'}, with {\tt (a)} where {\tt a} is the corresponding actual argument
expressions in the instance of {\tt R'}.

\item
%The third step includes the following steps:
%
%1. copy all declarations of local variables of p2 to an appropriate
%   place in p1.
%
In the property\_expr of the assertion, replace the instance of {\tt R} with
   sequence\_expr of {\tt R'} wrapped in parenthesis.
\end{enumerate}
end\\\\\\
%
%
%----------------------------------------------------------------------------------------
Clause F.5:\\\\\\

replace\\\\

This subclause defines the neutral semantics of instances of recursive properties in terms of the neutral
semantics of instances of nonrecursive properties. The latter can be expanded to properties in the abstract
syntax by appropriate substitutions; therefore, their semantics is assumed to be understood.\\\\


with\\\\

This subclause defines the neutral semantics of
{\color{blue}assertions with} instances of recursive properties in
terms of the neutral semantics of {\color{blue}assertions with}
instances of nonrecursive properties. The latter can be expanded to
properties in the abstract syntax by {\color{red}\sout{appropriate
substitutions}}{\color{blue}applying the rewrite
algorithm{\color{green}[Note to the editor: add link to the new sub
section, which is described in the previous item]}}; therefore, their
semantics is assumed to be understood.  \\\\\\

replace\\\\\\
%
Let $p(X)$ be an instance of a recursive named property p, where $X$ denotes the actual arguments of the
instance. For $k\geq  0$, the k-fold approximation to $p(X)$, denoted $p[k](X)$, is an instance of a non-recursive property
$p[k]$ defined inductively as follows:
\begin{itemize}
\item
    The declaration of $p[0]$ is obtained from the declaration of $p$ by replacing the body {\tt property\_expr}
    with the literal {\tt 1\'{}b1}.
\item
    For $k > 0$, the declaration of $p[k]$ is obtained from the declaration of $p$ by replacing each instance of
    a recursive property by its $(k - 1)$-fold approximation.
    The semantics of the instance $p(X)$ is then defined as follows: for any word w over $\Sigma$ and local variable context
    L, w, L$\models p(X)$ iff for all $k \geq 0$, w, L $\models p[k](X)$.
\end{itemize}
\ \\\\

with\\\\
%
{\color{blue}Let $A$ be an assertion with instances of a recursive
properties.} Let $p(X)$ be
{\color{red}\sout{an instance}}{\color{blue}a declaration} of a
{\color{red}\sout{recursive}} property p, where $X$ denotes the
{\color{red}\sout{actual}}{\color{blue}formal} arguments of {\color{red}\sout{the instance }}
{\color{blue}$p$}. For $k \geq 0$, the k-fold approximation to {\color{blue}$A$
and} $p(X)$, denoted {\color{blue}$A[k]$ and} $p[k](X)$
{\color{blue}respectively}, is {\color{red}\sout{an instance of}} a
non-recursive property {\color{blue} declaration} $p[k]${\color{blue} ($A[k]$)} defined
inductively as follows:
\begin{itemize}
\item
    The declaration of $p[0]$ {\color{blue}($A[0]$)} is obtained from
    the declaration of $p$ {\color{blue}($A$)} by replacing the body {\tt property\_expr}
    with the literal {\tt 1\'{}b1}.
\item
    For $k > 0$, the declaration of $p[k]$ {\color{blue}($A[k]$)} is
    obtained from the declaration of $p$ {\color{blue}($A$)} by
    replacing each instance of a {\color{red}\sout{recursive}}
    property by its $(k - 1)$-fold approximation. 
\end{itemize}
 The semantics of {\color{red}\sout{the instance $p(X)$}}
    {\color{blue}$A$} is then defined as follows: for any word w over
    $\Sigma$ and local variable context L, {\color{red}\sout{w,
    L$\models$ $p(X)$} {\color{blue}w,L $\models A$}} iff for all $k
    \geq 0$, {\color{red}\sout{w, L $\models p[k](X)$}}
    {\color{blue}w,L $\models A[k]$}. Since {\color{blue} $A[k]$ do
    not have instances of recursive properties, its semantics is
    obtained using the rewrite algorithm{\color{green}[Note to the
    editor: add link to the new sub section, which is described in the
    previous item]}}.}

\end{document}










