PSL/A Practical Introduction to PSL/Basic Temporal Properties/ru - История изменений

ANA: /* Основные временные свойства While */

2013-11-13T19:50:13Z

‎Основные временные свойства While

Valentin: /* 2.5 eventually! */

2013-11-13T10:16:41Z

‎2.5 eventually!

Valentin: /* 2.4 The until and before operators */

2013-11-13T10:03:10Z

‎2.4 The until and before operators

Valentin: /* 2.3 вариации next, включая next_event */

2013-11-10T15:51:48Z

‎2.3 вариации next, включая next_event

Valentin: /* 2.3 вариации next, включая next_event */

2013-11-08T14:25:46Z

‎2.3 вариации next, включая next_event

ANA: /* 2.4 The until and before operators */

2013-11-02T18:04:28Z

‎2.4 The until and before operators

Valentin: /* 2.3 вариации next, включая next_event */

2013-11-01T17:40:18Z

‎2.3 вариации next, включая next_event

Valentin: /* 2.3 вариации next, включая next_event */

2013-10-31T10:29:34Z

‎2.3 вариации next, включая next_event

Valentin: /* 2.3 Variations on next including next_event */

2013-10-31T09:43:43Z

‎2.3 Variations on next including next_event

Valentin: /* 2.2 Оператор next */

2013-10-31T09:04:30Z

‎2.2 Оператор next

@@ Строка 1: / Строка 1: @@
 {{PSL TOC}}
-==Основные временные свойства While==
+==Основные временные свойства ==
 <!--

@@ Строка 473: / Строка 473: @@
 Что если утверждению <code>ack</code> позволенно выполниться не вместе со следующим утверждением <code>req</code>, но вместе с установленным запросом? Другими словами, что если в дополнение к поведению, показаному в тракте 2.9(i), мы хотим допустить поведение показанное в тракте 2.9(iii)? Как было отмечно ранее, утверждение 2.9b это не ответ. Скорее, мы напишем код утверждения 2.9d.
-===2.5 <code>eventually!</code>===
+===2.5 Оператор <code>eventually!</code>===
-−
 The <code>eventually!</code> operator allows you to specify that something must occur in
 the future without saying exactly when. For example, Assertion 2.10a states
@@ Строка 483: / Строка 483: @@
 requests, thus Assertion 2.10a holds on Trace 2.10(i). We examine the issue
 of specifying a one-to-one correspondence between signals in Section 13.4.2.
 The exclamation point (<code>!</code>) of the <code>eventually!</code> operator indicates that it
 is a strong operator. We discuss weak vs. strong temporal operators in detail
 in Chapter 4.
+-->
 {| align=center
 ! [[Файл:Psl fig 02.10.png|600px]]
 |-
-! (i) Assertion 2.10a holds
+! (i) Утверждение 2.10a выполняется
 |-
 |<pre>
@@ Строка 498: / Строка 502: @@
 </pre>
 |-
-! Fig. 2.10: The <code>eventually!</code> operator
+! Рис. 2.10: Оператор <code>eventually!</code>
 |}

@@ Строка 366: / Строка 366: @@
 |}
-=== 2.4 The <code>until</code> and <code>before</code> operators ===
+=== 2.4 Операторы <code>until</code> и <code>before</code> ===
@@ Строка 372: / Строка 372: @@
 ! [[Файл:Psl fig 02.7.png|400px]]
 |-
-! (i) Assertion 2.7a holds
+! (i) Утверждение 2.7a выполняется
 |-
 |<pre>
@@ Строка 379: / Строка 379: @@
 </pre>
 |-
-! Fig. 2.7: <code>next_event e[i:j]</code>
+! Рис. 2.7: <code>next_event e[i:j]</code>
 |}
+<!--
 The <code>until</code> operator provides another way to move forward, this time while
 putting a requirement on the cycles in which we are moving. For example,
@@ Строка 397: / Строка 397: @@
 Assertion 2.8a does not prohibit the assertion of busy at cycles 4 and 10 – it
 just does not require it.
 If signal done is asserted the cycle after signal <code>req</code> is asserted, Assertion 2.8a does not require that signal <code>busy</code> be asserted at all, while Assertion 2.8b does. That is, Assertion 2.8a holds on Trace 2.8(iii) – the fact that
 done happens immediately after <code>req</code> leaves no cycles on which busy needs to
 be asserted. Assertion 2.8b does not hold on Trace 2.8(iii) because of a missing
 assertion of <code>busy</code> in the cycle in which <code>done</code> is asserted.
+-->
 {| align=center
@@ Строка 414: / Строка 418: @@
 </pre>
 |-
-! Fig. 2.8: The <code>until</code> and <code>until_</code> operators
+! Рис. 2.8: Операторы <code>until</code> и <code>until_</code>
 |}
+<!--
 The <code>before</code> family of operators provides an easy way to state that we
 require some signal to be asserted before some other signal. For example, suppose that we have a pulsed signal called <code>req</code>, and we have the requirement that
@@ Строка 433: / Строка 437: @@
 Starting at cycle 2 and looking forward, we first see an assertion of <code>ack</code> (at
 cycle 3), and only afterwards an assertion of <code>req</code> (at cycle 6).
+-->
 {| align=center
@@ Строка 445: / Строка 450: @@
 </pre>
 |-
-! Fig. 2.9 The <code>before</code> and <code>before_</code> operators
+! Рис. 2.9 Операторы <code>before</code> и <code>before_</code>
 |}
+<!--
 The <code>before</code> operator requires that its first operand happen strictly before
 its second. In order to specify that something must happen before or at the
@@ Строка 456: / Строка 461: @@
 in Trace 2.9(i) is allowed, and that in addition behavior like that shown in
 Trace 2.9(ii) is allowed, use Assertion 2.9c.
 What if the assertion of <code>ack</code> is allowed to come, not together with the next
 assertion of <code>req</code>, but rather together with the request being acknowledged?
@@ Строка 462: / Строка 470: @@
 want to allow the behavior shown in Trace 2.9(iii)? As we have seen previously,
 Assertion 2.9b is not the answer. Rather, we can code Assertion 2.9d.
 ===2.5 <code>eventually!</code>===

@@ Строка 282: / Строка 282: @@
 |}
 Just as we can use <code>next[i]</code> to indicate the ''i<sup>th</sup>'' next cycle, we can use
 <code>next_event(b)[i]</code> to indicate the ''i<sup>th</sup>'' occurrence of <code>b</code>. For example, in order
@@ Строка 294: / Строка 295: @@
 that in both cases, signal <code>last_ready</code> is asserted on the fourth assertion of
 <code>ready</code>, thus Assertion 2.5a holds on Trace 2.5(i).
+-->
 {| align=center
 ! [[Файл:Psl fig 02.5.png]]
 |-
-! (i) Assertion 2.5a holds
+! (i) Утверждение 2.5a выполняется
 |-
 |<pre>
@@ Строка 306: / Строка 308: @@
 </pre>
 |-
-! Fig. 2.5: next event[n]
+! Рис. 2.5: next event[n]
 |}
 As with <code>next_a[i:j]</code> and <code>next_e[i:j]</code>, the <code>next_event</code> operator also
 comes in forms that allow it to indicate ''all'' of a range of future cycles, or the ''existence''
@@ Строка 325: / Строка 328: @@
 signal <code>read_request</code>, where <code>tag[2:0]</code> has the value 5, the value of <code>tag[2:0]</code>
 is also 5 on the next four assertions of signal <code>data</code> (at cycles 17 through 20).
 In order to indicate that we expect something to happen on one of the next
 ''i<sup>th</sup>'' to ''j<sup>th</sup>'' cycles, we can use the <code>next_event_e(b)[i:j](f)</code> operator, which
@@ Строка 335: / Строка 341: @@
 holds on Trace 2.7(i) because every time that signal <code>high_pri_req</code> is asserted,
 signal <code>high_pri_ack</code> is asserted on one of the next two assertions of <code>gnt</code>.
 The syntax of the range specification for all operators – including those
 we have not yet seen – is flavor dependent. In the Verilog, SystemVerilog and
 SystemC flavors, it is <code>[i:j]</code>. In the VHDL flavor it is <code>[i to j]</code>. In the GDL
 flavor it is <code>[i..j]</code>.
+-->
 {| align=center
 ! [[Файл:Psl fig 02.6.png|600px]]
 |-
-! (i) Assertion 2.6a holds
+! (i) Утверждение 2.6a выполняется
 |-
 |<pre>
@@ Строка 353: / Строка 363: @@
 </pre>
 |-
-! Fig. 2.6 <code>next_event a[i:j]</code>
+! Рис. 2.6 <code>next_event a[i:j]</code>
 |}

@@ Строка 219: / Строка 219: @@
 Свойство next_e[i:j] выполняется, если ''существует'' цикл со следующего <code>i</code> до следующих <code>j</code> циклов, в которых выполняются операнды. Например, утверждение 2.3с показывает, что когда бы сигнал <code>a</code> не выполнялся, сигнал <code>b</code> выполняется тремя, четырьмя или пятью циклами позже. Нету ничего в утверждении 2.3с, что предотвращает единичное утверждение сигнала <code>b</code> из выполнения многочисленных утверждений сигнала <code>a</code>, таким образом это выполняется в тракте 2.3(vi), потому что утверждение сигнала <code>b</code>, в цикле 7, появляется через 5 циклов после утверждения сигнала <code>a</code> в цикле 2, и через три цикла после утверждения сигнала <code>a</code> в цикле 4.
 Assertion 2.3c also holds on Traces 2.3(i), 2.3(iii), 2.3(iv), and 2.3(v),
 since there are enough assertions of signal <code>b</code> at the appropriate times. In
@@ Строка 226: / Строка 227: @@
 , and three cycles after the assertion of <code>a</code> at cycle 4). In Trace 2.3(v) there
 are just enough assertions of <code>b</code> to satisfy the requirements of Assertion 2.3c.
 The <code>next_event</code> operator is a conceptual extension of the <code>next</code> operator.
 While next refers to the next cycle, <code>next_event</code> refers to the next
@@ Строка 237: / Строка 241: @@
 assertions of <code>gnt</code> occur at cycles 4 and 11, respectively, and <code>high_pri_ack</code>
 holds in these cycles.
 The <code>next_event</code> operator includes the current cycle. That is, an assertion
 of <code>b</code> in the current cycle will be considered the next assertion of <code>b</code> in the
@@ Строка 252: / Строка 259: @@
 and 11 for Assertion 2.4a to cycles 4, 9 and 11 for Assertion 2.4b, and at cycle
 there is no assertion of <code>high_pri_ack</code> in Trace 2.4(ii).
+-->
 {| align=center
@@ Строка 261: / Строка 269: @@
 ! [[Файл:Psl fig 02.4ii.png]]
 |-
-! (ii) Assertion 2.4a holds, but 2.4b does not
+! (ii) Утверждение 2.4a выполняется, а 2.4b нет
 |-
 |<pre>
@@ Строка 271: / Строка 279: @@
 </pre>
 |-
-! Fig. 2.4: <code>next_event</code>
+! Рис. 2.4: <code>next_event</code>
 |}

← Предыдущая		Версия 18:04, 2 ноября 2013
Строка 349:		Строка 349:

	=== 2.4 The <code>until</code> and <code>before</code> operators ===		=== 2.4 The <code>until</code> and <code>before</code> operators ===
		+
		+
		+	{\| align=center
		+	! [[Файл:Psl fig 02.7.png\|400px]]
		+	\|-
		+	! (i) Assertion 2.7a holds
		+	\|-
		+	\|<pre>
		+	assert always (high_pri_req -> (2.7a)
		+	next_event_e(gnt)[1:2](high_pri_ack));
		+	</pre>
		+	\|-
		+	! Fig. 2.7: <code>next_event e[i:j]</code>
		+	\|}
		+
		+
		+	The <code>until</code> operator provides another way to move forward, this time while
		+	putting a requirement on the cycles in which we are moving. For example,
		+	Assertion 2.8a states that whenever signal <code>req</code> is asserted, then, starting at
		+	the next cycle, signal <code>busy</code> must be asserted up until signal <code>done is</code> asserted.
		+	Assertion 2.8a requires that <code>busy</code> will be asserted up to, but not necessarily
		+	including, the cycle where <code>done</code> is asserted. In order to include the cycle where
		+	<code>done</code> is asserted, use the operator <code>until_</code>. The underscore (<code>_</code>) is intended to
		+	represent the extra cycle in which we require that <code>busy</code> should stay asserted,
		+	so Assertion 2.8b states that whenever signal <code>req</code> is asserted, then starting
		+	from the next cycle, <code>busy</code> must be asserted and must stay asserted up until
		+	and including the cycle where done is asserted. For example, Assertion 2.8a
		+	holds on Trace 2.8(i), but Assertion 2.8b does not, because <code>busy</code> is not asserted at cycles 4 and 10. Both Assertions 2.8a and 2.8b hold on Trace 2.8(ii):
		+	Assertion 2.8a does not prohibit the assertion of busy at cycles 4 and 10 – it
		+	just does not require it.
		+
		+	If signal done is asserted the cycle after signal <code>req</code> is asserted, Assertion 2.8a does not require that signal <code>busy</code> be asserted at all, while Assertion 2.8b does. That is, Assertion 2.8a holds on Trace 2.8(iii) – the fact that
		+	done happens immediately after <code>req</code> leaves no cycles on which busy needs to
		+	be asserted. Assertion 2.8b does not hold on Trace 2.8(iii) because of a missing
		+	assertion of <code>busy</code> in the cycle in which <code>done</code> is asserted.
		+
		+
		+	{\| align=center
		+	! [[Файл:Psl fig 02.8.png\|600px]]
		+	\|-
		+	!
		+	\|-
		+	\|<pre>
		+	assert always (req -> next (busy until done)); (2.8a)
		+	assert always (req -> next(busy until_ done)); (2.8b)
		+	</pre>
		+	\|-
		+	! Fig. 2.8: The <code>until</code> and <code>until_</code> operators
		+	\|}
		+
		+
		+	The <code>before</code> family of operators provides an easy way to state that we
		+	require some signal to be asserted before some other signal. For example, suppose that we have a pulsed signal called <code>req</code>, and we have the requirement that
		+	before we can make a second request, the first must be acknowledged. We can
		+	express this in PSL using Assertion 2.9a. We need the <code>next</code> to take us forward
		+	one cycle so that the <code>req</code> in (<code>ack before req</code>) is sure to refer to some other
		+	<code>req</code>, and not the one we have just seen. To understand this, let us examine a
		+	flawed version of the same specification. Consider Assertion 2.9b. It requires
		+	that (<code>ack before req</code>) hold at every cycle in which <code>req</code> holds. Consider,
		+	for example, cycle 1 of Trace 2.9(i). Signal <code>req</code> is asserted. Therefore, (<code>ack before req</code>) must hold at cycle 1. However, it does not, because starting at
		+	cycle 1 and looking forward, we first see an assertion of signal <code>req</code> (at cycle 1),
		+	and only afterwards an assertion of signal <code>ack</code> (at cycle 3) – so <code>req</code> is asserted
		+	before <code>ack</code>, and not the other way around. Assertion 2.9a, on the other hand,
		+	states what we want: at cycle 1, for example, we require <code>next</code> (<code>ack before req</code>) to hold. Therefore, we require that (<code>ack before req</code>) hold at cycle 2.
		+	Starting at cycle 2 and looking forward, we first see an assertion of <code>ack</code> (at
		+	cycle 3), and only afterwards an assertion of <code>req</code> (at cycle 6).
		+
		+
		+	{\| align=center
		+	! [[Файл:Psl fig 02.9.png\|600px]]
		+	\|-
		+	\|<pre>
		+	assert always (req -> next (ack before req)); (2.9a)
		+	assert always (req -> (ack before req)); (2.9b)
		+	assert always (req -> next (ack before_ req)); (2.9c)
		+	assert always (req -> (ack \|\| next (ack before req))); (2.9d)
		+	</pre>
		+	\|-
		+	! Fig. 2.9 The <code>before</code> and <code>before_</code> operators
		+	\|}
		+
		+
		+	The <code>before</code> operator requires that its first operand happen strictly before
		+	its second. In order to specify that something must happen before or at the
		+	same cycle as something else, use <code>before_</code>. The underscore (<code>_</code>) is intended
		+	to represent the cycle in which we allow an overlap between the left and
		+	right sides. For example, in order to specify that behavior like that shown
		+	in Trace 2.9(i) is allowed, and that in addition behavior like that shown in
		+	Trace 2.9(ii) is allowed, use Assertion 2.9c.
		+
		+	What if the assertion of <code>ack</code> is allowed to come, not together with the next
		+	assertion of <code>req</code>, but rather together with the request being acknowledged?
		+	In other words, what if in addition to the behavior shown in Trace 2.9(i), we
		+	want to allow the behavior shown in Trace 2.9(iii)? As we have seen previously,
		+	Assertion 2.9b is not the answer. Rather, we can code Assertion 2.9d.
		+
		+	===2.5 <code>eventually!</code>===
		+
		+
		+	The <code>eventually!</code> operator allows you to specify that something must occur in
		+	the future without saying exactly when. For example, Assertion 2.10a states
		+	that every request (assertion of <code>req</code>) must be followed at some time with
		+	an acknowledge (assertion of <code>ack</code>). There is nothing in Assertion 2.10a to
		+	prevent a single acknowledge from satisfying the requirement for multiple
		+	requests, thus Assertion 2.10a holds on Trace 2.10(i). We examine the issue
		+	of specifying a one-to-one correspondence between signals in Section 13.4.2.
		+
		+	The exclamation point (<code>!</code>) of the <code>eventually!</code> operator indicates that it
		+	is a strong operator. We discuss weak vs. strong temporal operators in detail
		+	in Chapter 4.
		+
		+
		+	{\| align=center
		+	! [[Файл:Psl fig 02.10.png\|600px]]
		+	\|-
		+	! (i) Assertion 2.10a holds
		+	\|-
		+	\|<pre>
		+	assert always (req -> eventually! ack); (2.10a)
		+	</pre>
		+	\|-
		+	! Fig. 2.10: The <code>eventually!</code> operator
		+	\|}

@@ Строка 196: / Строка 196: @@
 .3(ii), 2.3(iv), 2.3(v) или 2.3(vi).
 Previously we discussed the fact that the cycles involved in satisfying one
 assertion of signal a may overlap those involved in satisfying another assertion
@@ Строка 202: / Строка 203: @@
 because of the assertion of a at cycle 2, and must be asserted in cycles 7
 through 9 (marked as “2”) because of the assertion of a at cycle 4.
 A next_e[i:j] property holds if there ''exists'' a cycle from the next <code>i</code>
 through the next <code>j</code> cycles in which its operand holds. For example, Assertion
@@ Строка 212: / Строка 216: @@
 of signal <code>a</code> at cycle 4. We examine the issue of specifying a one-to-one
 correspondence between signals in Section 13.4.2.
 Assertion 2.3c also holds on Traces 2.3(i), 2.3(iii), 2.3(iv), and 2.3(v),

@@ Строка 186: / Строка 186: @@
 |}
+<!--
 A next_a[i:j] property holds if its operand holds in ''all'' of the cycles from
 the ''i<sup>th</sup>'' next cycle through the ''j<sup>th</sup>'' next cycle, inclusive. For example, Assertion
@@ Строка 192: / Строка 192: @@
 five cycles later. It holds on Trace 2.3(iii) and does not hold on Traces 2.3(i),
 .3(ii), 2.3(iv), 2.3(v), or 2.3(vi).
 Previously we discussed the fact that the cycles involved in satisfying one

@@ Строка 158: / Строка 158: @@
 |}
-=== 2.3 Variations on <code>next</code> including <code>next_event</code> ===
+=== 2.3 вариации <code>next</code>, включая <code>next_event</code> ===
 A <code>next</code> property holds if its operand holds in the next cycle. Variations on the
 <code>next</code> operator allow you to specify the ''n<sup>th</sup>'' next cycle, and ranges of future
@@ Строка 168: / Строка 169: @@
 of signal <code>b</code> at cycle 7, and does not hold on Trace 2.3(vi) because of <code>a</code> missing
 assertion of signal <code>b</code> at cycle 5.
+-->
 {| align=center
@@ Строка 181: / Строка 183: @@
 </pre>
 |-
-! Fig. 2.3: Операторы <code>next[n]</code>, <code>next_a[i:j]</code> и <code>next_e[i:j]</code>
+! Рис. 2.3: Операторы <code>next[n]</code>, <code>next_a[i:j]</code> и <code>next_e[i:j]</code>
 |}

@@ Строка 117: / Строка 117: @@
 holds. By adding an always operator, we get a property that holds if the
 sub-property <code>a -> next b</code> holds at every cycle. Thus, Assertion 2.2a states
-that whenever <code>a</code> holds, <code>b</code> must hold at the next cycle. Assertion 2.2a holds on
+that whenever <code>a</code> holds, <code>a</code> must hold at the next cycle. Assertion 2.2a holds on
 Trace 2.2(i) because every assertion of signal <code>a</code> is followed by an assertion of
 signal <code>b</code>. This is shown in the “if” and “then” annotations on Trace 2.2(ii).
@@ Строка 124: / Строка 124: @@
 those following an assertion of <code>a</code>.
 -->
-Другой временной оператор - это оператор <code>next</code>. Он показывает, что свойство свойство должно выполняться, если его операнд выполняется в следующем цикле. Например, утверждение 2.2a показывает, что когда бы a не выполнялось, b должно выполниться в следующем цикле. Утверждение 2.2a использует другой важный оператор, логический оператор импликации (<code>-></code>). В то время как оператор логической импликации Булевый, а не временной (он не свяжет два подсвойства по времени), это играет очень важную роль во многих временных свойствах.
+Другой временной оператор - это оператор <code>next</code>. Он показывает, что свойство свойство должно выполняться, если его операнд выполняется в следующем цикле. Например, утверждение 2.2a показывает, что когда бы a не выполнялось, b должно выполниться в следующем цикле. Утверждение 2.2a использует другой важный оператор, логический оператор импликации (<code>-></code>). В то время как оператор логической импликации Булевый, а не временной (он не свяжет два подсвойства по времени), это играет очень важную роль во многих временных свойствах. Логическая импликация <code>prop1 -> prop2</code> выполняется, если prop1 не выполняется или prop2 выполняется. Это хорошо представляется, если принять это, как выражение вида if-then, с частью else. <code>prop1 -> prop2</code> можно понимать, как если prop1, то далее следует prop2, иначе возвращается значение правда. Таким образом, под-свойство <code>a -> next b</code>, в нашем примере, выполняется, если a не выполняется (потому что свойство по умолчание имеет значение правда) или, если a выполняется, а также и next b выполняется. Добавляя оператор always, мы получаем свойство, которое выполняется, если под-свойство <code>a -> next b</code> выполняется в каждом цикле. Таким образом, утверждение 2.2а показывает, что когда бы ни выполнялось <code>a</code>, <code>b</code> должно выполняться в следующем цикле. Утверждение 2.2а выполняется по сигналу <code>b</code>. Это показано в “if” и “then” примечании на тракте 2.2(ii). “Дополнительные” утверждения сигнала <code>b</code> на циклах 1 и 10, спровоцированы утверждение 2.2а, потому что в нем ничего не сказано о значениях b в цикле, кроме того, что следует из из утверждения <code>a</code>.
 Note that the cycles involved in satisfying one assertion of signal a may
 overlap with those involved in satisfying another assertion. For example, consider
@@ Строка 138: / Строка 139: @@
 cycle 5 in order to satisfy the assertion of <code>a</code> at cycle 4, we see an additional
 assertion of signal <code>a</code> that must be considered.
 Assertion 2.2a does not hold on Trace 2.2(iv) because the third assertion
 of signal <code>a</code>, at cycle 5, is missing an assertion of signal <code>b</code> at the following cycle.
+-->
 {| align=center
@@ Строка 150: / Строка 155: @@
 </pre>
 |-
-! Fig. 2.2: The next and logical implication operators
+! Рис.2.2: Операторы next и логическая импликация
 |}