Subject: [sv-ac] preliminary draft of semantics
From: John Havlicek (john.havlicek@motorola.com)
Date: Tue Mar 18 2003 - 15:00:23 PST
All:
Below is the current working draft of the SVA semantics.
It is by no means final. I am sending it as a heads up for
anyone in SV-AC who is interested in a preview.
I will be forwarding this draft to FVTC since the interplay
of SVA semantics with PSL semantics is on the agenda for
tomorrow's FVTC meeting.
Best regards,
John Havlicek
===================================================================
The semantics below assumes that there will be defined rules to
determine when a clock operator "@(c)" is at the top level of an
assertion. Loosely speaking, top-level clock operators are weak,
while lower level clock operators are strong.
As directed by DWG, there is not a distinguishing operator syntax
for a clock operator at the top level.
This semantics assumes that DWG will change the syntax so that a
top-level clock operator appears outside of top-level negation.
This semantics does not address local variables, the "ended" operator,
or operators such as "rose" and "fell".
============================================================================
Semantics:
---------
Semantics are defined over empty, finite, and infinite words from the
alphabet {2^P} \union {\top, \bot}.
Assume boolean satisfaction over a letter is defined, in the
obvious way if the letter is in {2^P}, and as follows for \top and \bot:
For any boolean expression b,
\top |= b
not(\bot |= b)
Define \bar{w} to be obtained from w by interchanging \top with \bot.
We use % as a special notation for clock operators, and define the following
rewrite rules:
%(clk) b \eqdef b
%(clk) (s) \eqdef %(clk) s
%(clk) r1 ; r2 \eqdef
(%(clk) r1) ; ( (!clk*[0:inf]; clk ;[0] (%(clk) r2))
|| (1*[0] intersect (%(clk) r2)) )
%(clk) r1 ;[0] r2 \eqdef (%(clk) r1) ;[0] (%(clk) r2)
%(clk) r1 || r2 \eqdef (%(clk) r1) || (%(clk) r2)
%(clk) r1 intersect r2 \eqdef (%(clk) r1) intersect (%(clk) r2)
%(clk) first_match(s) \eqdef first_match(%(clk) s)
%(clk) s *[0] \eqdef (%(clk) s) *[0]
%(clk) s *[1:inf] \eqdef (%(clk) s) *[1:inf]
%(clk) not p \eqdef not %(clk) p
%(clk) r => p \eqdef (%(clk) r1) => (%(clk) p)
%(clk) r |=> p \eqdef (%(clk) (r1 ; true)) => (%(clk) p)
We define tight satisfaction for sequences as follows.
* w |== b iff |w| = 1 and w |= b.
* w |== (s) iff w |== s.
* w |== s ; t iff there exist u, v such that w = uv and
u |== s and v |== t.
* w |== s ;[0] t iff there exist u,x,v such that w = uxv and
|x| = 1 and ux |== s and xv |== t.
* w |== s || t iff either w |== s or w |== t.
* w |== s intersect t iff both w |== s and w |== t.
* w |== first_match(s) iff
both
- w |== s
and
- if there exist u, v such that w = uv and u |== s, then v is
empty.
* w |== s *[0] iff |w| = 0.
* w |== s *[1:inf] iff there exist w_1, w_2, ..., w_j (j >= 1)
such that w = w_1 w_2 ... w_j and for every i s.t. 1 <= i <= j, w_i |== s.
* If "@(b)" is not a top-level clock operator in "@(b) r" then
w |== @(b) r iff w |== (!b*[0:inf]; b ;[0] (%(b) r)).
Define the semantics over infinite words as follows, where b is a boolean
expression, p is a property, and r, r1 and r2 are sequences.
* If "@(b)" is a top-level clock operator in "@(b) p", then w |= @(b) p iff
(if there exists i >= 0 s.t. w^i |= b, then for the first such i, w^i |= %(b) p).
* w |= not p iff not(\bar{w} |= p).
* w |= r iff there exists j >= 0 s.t. w^{0,j} |== r.
* w |= r => p iff for every j >= 0 s.t. \bar{w}^{0,j} |== r, w^{j..} |= p.
* w |= r |=> p iff for every j >= 0 s.t. \bar{w}^{0,j} |== r, w^{j+1..} |= p.
* w |= accept (b) p iff either w |= p or there exists k, 0 <= k < |w|,
such that (w^{k,k} |= b and w^{0,k-1} \top^\omega |= p). Here, w^{0,-1}
denotes the empty trace.
* w |= initial p iff w |= p.
* w |= always p iff for every i >= 0, w^{i..} |= p.
Now, define weak and strong satisfaction as follows:
For a finite word w:
w |=(-) p <==> w \top^\omega |= p
w |=(+) p <==> w \bot^\omega |= p
For an infinite word w:
w |=(-) p <==> w |=(+) p <==> w |= p
And finally, the tools return:
true if w |=(+) p
false if not(w |=(-) p)
unknown otherwise
DERIVED OPERATORS
=================
* w |== s @@ t iff w |== s ; t.
Derived Consecutive Repetition Operators
----------------------------------------
* Let m > 0. s *[m] \eqdef s ; s ; ... ; s // m copies of s
* s *[0:inf] \eqdef s *[0] or s *[1:inf].
* Let m <= n. s *[m:n] \eqdef s *[m] or s *[m+1] or ... or s *[n].
* Let m > 0. s *[m:inf] \eqdef s *[m]; s *[0:inf].
Derived Range Operators
-----------------------
Let m <= n.
* ([m:n] t) \eqdef (1*[m:n]; t).
* ([m:inf] t) \eqdef (1*[m:inf]; t).
* ([m] t) \eqdef (1*[m]; t).
* s ;[0:n] t \eqdef s ;[0] ([0:n] t).
* s ;[0:inf] t \eqdef s ;[0] ([0:inf] t).
* Let m > 0. s ;[m:n] t \eqdef s; 1*[m-1:n-1]; t.
* Let m > 0. s ;[m:inf] t \eqdef s; 1*[m-1:inf]; t.
* Let m > 0. s ;[m] t \eqdef s ; 1*[m-1]; t.
Derived Non-consecutive Repetition Operators
--------------------------------------------
* w |== b *=[m:n] iff w |== (!b*[0:inf];b)*[m:n].
// This follows the discussion on pp. 48-49 of Rev0.80. I expected
// the righthand side to be "w |== (!b*[0:inf];b)*[m:n];!b*[0:inf]".
* w |== b *=[m:inf] iff w |== (!b*[0:inf];b)*[m:inf].
// Same comment as preceding.
Other Derived Operators
-----------------------
* s and t \eqdef ((s;1*[0:inf]) intersect t) or (s intersect (t;1*[0:inf])).
* b throughout s \eqdef b*[0:inf] intersect s.
This archive was generated by hypermail 2b28 : Tue Mar 18 2003 - 15:03:38 PST