PSL/A Practical Introduction to PSL/SERE Style - История изменений

Valentin: /* 5.4 Операторы повторения SERE ([n], [=n], и [->n]) /

2014-02-17T08:22:58Z

‎5.4 Операторы повторения SERE ([*n], [=n], и [->n])

Valentin: /* 5.4 Операторы повторения SERE ([n], [=n], и [->n]) /

2014-02-07T11:07:50Z

‎5.4 Операторы повторения SERE ([*n], [=n], и [->n])

Valentin: /* 5.4 SERE repetition operators ([n], [=n], and [->n]) /

2014-01-30T10:57:28Z

‎5.4 SERE repetition operators ([*n], [=n], and [->n])

Valentin: /* 5.3 The never operator applied to a SERE */

2014-01-30T09:42:20Z

‎5.3 The never operator applied to a SERE

Valentin: /* 5.2 Слабый и сильный SERE */

2014-01-30T09:26:46Z

‎5.2 Слабый и сильный SERE

Valentin: /* 5.2 Weak and strong SEREs */

2014-01-30T09:05:08Z

‎5.2 Weak and strong SEREs

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

2014-01-30T08:37:42Z

‎5.1 Суффиксная импликация (|-> и |=>)

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

2014-01-27T10:27:51Z

‎5.1 Суффиксная импликация (|-> и |=>)

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

2014-01-24T12:42:00Z

‎5.1 Суффиксная импликация (|-> и |=>)

Valentin: /* Стиль SERE */

2014-01-09T16:22:01Z

‎Стиль SERE

@@ Строка 402: / Строка 402: @@
 -->
 Непоследовательный оператор повторения (<code>[=n]</code>) предоставляет возможность описания повторений, которые происходят на непоследовательных циклах. Это может применять только для Булевых выражений. Например, для описания требования, что после запроса (утверждения сигнала <code>req</code>), мы ожидаем увидеть подтверждение (утверждение сигнала <code>ack</code>) в сопровождении некоторого количества циклов, включая три необязательно последовательных утверждения сигнала <code>busy</code>, в сопровождении  утверждения сигнала <code>done</code>, утверждение 5.13a. Утверждение 5.13a выполняется на тракте Trace 5.13(i). Обратите внимания на циклы отмеченные “<code>busy[=3]</code>” в тракте 5.13(i). Они не начинаются с утверждением сигнала <code>busy</code> , при этом они не заканчиваются после одного. Непоследовательный оператор повторения <code>[=n]</code> определяет последовательность циклов, в которой <code>n</code> необязательно последовательное повторение Булевого выражения, включая последовательности циклов, в которых “padding” вначале и/или в конце. Другими словами, он определяет любую  последовательность циклов, в которой число утверждений  Булевого выражения повторится <code>n</code> раз.
+<!--
-If you want to disallow the padding at the end, use the goto repetition op-
+If you want at the end, use the goto repetition op-
 erator [->n]. The goto repetition operator [->n] is similar to the nonconsec-
 utive repetition operator, except that the sequence of cycles being described
@@ Строка 413: / Строка 413: @@
 Trace 5.13(ii) because the third busy is immediately followed by an assertion
 of signal done.
 The n can be omitted for the goto repetition operator, in which case n
 defaults to 1. In other words, b[->] is equivalent to b[->1].
@@ Строка 425: / Строка 428: @@
 sertion 5.14a holds on Traces 5.14(i) and 5.14(ii), while Assertion 5.14b holds
 on Trace 5.14(ii) but not on Trace 5.14(i).
 ==5.5 Concatenation (;) and fusion (:)==

@@ Строка 353: / Строка 353: @@
 Мы можем повторять не только Булевы выражения, но и SERE. Например, свойство 5.11а выполняется, если после предопределенного запроса (утверждение сигнала <code>req</code> последует утверждение сигнала <code>ack</code>), мы видим три передачи данных, с последующим утверждение сигнала <code>d_end</code>, где передача данных это утверждение сигнала <code>start</code>, с последующим утверждение сигнала <code>busy</code>, с полседующим утверждением сигнала <code>done</code>. Тракт 5.11(i) это пример тракта, в котором выполняется свойство 5.11a.
 If we omit the <code>n</code>, the resulting SERE matches any number of repetitions of
 the Boolean expression or SERE that is being repeated. For example, asserting
@@ Строка 358: / Строка 359: @@
 any number of data transfers followed by an assertion of <code>done</code>. Property 5.11b
 holds on Trace 5.11(i), as well as on Traces 5.11(ii) and 5.11(iii).
 A <code>[*]</code> repetition matches any number of repetitions, including none. Thus,
 Property 5.11b holds on Trace 5.11(iv) as well. If you want to specify any
@@ Строка 365: / Строка 369: @@
 is asserted. Thus, Property 5.11c does not hold on Trace 5.11(iv), but it does
 hold on Traces 5.11(i), 5.11(ii) and 5.11(iii).
 Instead of omitting the n, we can omit the Boolean expression or SERE
 and let the repetition <code>[*n]</code> stand alone. A stand-alone <code>[*n]</code> is equivalent
@@ Строка 374: / Строка 381: @@
 request (assertion of signal <code>req</code>), it comes four cycles later. Property 5.12a
 holds on Trace 5.12(i).
 The nonconsecutive repetition operator (<code>[=n]</code>) provides a way to describe
 repetitions that happen on not necessarily consecutive cycles. It can be ap-
@@ Строка 390: / Строка 400: @@
 of cycles in which the number of assertions of the Boolean expression being
 repeated is ''equal to'' <code>n</code> (thus the use of the equals sign in <code>[=n]</code>).
 If you want to disallow the padding at the end, use the goto repetition op-

@@ Строка 289: / Строка 289: @@
 |}
-==5.4 SERE repetition operators (<code>[*n]</code>, <code>[=n]</code>, and <code>[->n]</code>)==
+==5.4 Операторы повторения SERE  (<code>[*n]</code>, <code>[=n]</code>, и <code>[->n]</code>)==
 Up until now, we have seen basic SEREs composed of (possibly repeated)
 Boolean expressions separated by semi-colons. In this section, we examine
 SERE operators that allow you to build more sophisticated SEREs, using
 variations on the SERE repetition operators <code>[*n]</code>, <code>[=n]</code>, and <code>[->n]</code>.
 Consecutive repetition operators provide a shortcut to typing the same
 sub-SERE a number of times. The <code>[*n]</code> operator is an abbreviation for
@@ Строка 305: / Строка 309: @@
 an assertion of signal <code>done</code>. Trace 5.10(i) is an example of a trace on which
 Assertions 5.10a and 5.10b hold.
+-->
 {| align=center
@@ Строка 316: / Строка 321: @@
 </pre>
 |-
-! Fig. 5.10: The <code>[*n]</code> and <code>[*i:j]</code> operators
+! Рис. 5.10: Операторы <code>[*n]</code> и <code>[*i:j]</code>
 |}
 Instead of a specific number of repetitions, we can specify a range, i
 through <code>j</code>, like this: <code>[*i:j]</code>. Thus, Assertion 5.10c is similar to Asser-
@@ Строка 325: / Строка 331: @@
 we require between three and five. Assertion 5.10c holds on Trace 5.10(i) as
 well as on Trace 5.10(ii).
 The upper bound of a range can be infinity, which is indicated by a <code>$</code> in
 the SystemVerilog flavor, by ''null'' in the GDL flavor, and by inf in the Verilog,
 VHDL, and SystemC flavors. For instance, the SERE <code>{b[*5:inf]}</code> matches
 five or more repetitions of <code>b</code>.
 We can repeat not only a Boolean expression, but a SERE as well. For
 example, Property 5.11a holds if after an acknowledged request (an assertion
@@ Строка 338: / Строка 350: @@
 of signal <code>done</code>. Trace 5.11(i) is an example of a trace on which Property 5.11a
 holds.
 If we omit the <code>n</code>, the resulting SERE matches any number of repetitions of
@@ Строка 399: / Строка 413: @@
 sertion 5.14a holds on Traces 5.14(i) and 5.14(ii), while Assertion 5.14b holds
 on Trace 5.14(ii) but not on Trace 5.14(i).
 ==5.5 Concatenation (;) and fusion (:)==

@@ Строка 247: / Строка 247: @@
 |}
-==5.3 The <code>never</code> operator applied to a SERE==
+==5.3 Оператор <code>never</code> применимый в SERE==
 Another way to use a SERE is in describing sequences of events that should
 never happen. For example, Assertion 5.8a states that signal <code>req</code> should never
 be asserted for two consecutive cycles, and thus does not hold on Trace 5.8(i).
 As another example, consider Assertion 5.9a. It states that an acknowl-
 edged high priority request (assertion of <code>req</code> together with <code>high_pri</code>, followed
 a cycle later by <code>ack</code>) cannot be canceled (assertion of <code>cancel</code> the cycle after
 <code>ack</code>). Thus it holds on Trace 5.9(i), but not on Trace 5.9(ii).
+-->
 {| align=center
 ! [[Файл:Psl fig5.8.png]]
 |-
-| (i) Assertion 5.8a does not hold
+| (i) Утверждение 5.8a не выполняется
 |-
 |<pre>
@@ Строка 268: / Строка 273: @@
 </pre>
 |-
-! Fig. 5.8: The never operator
+! Рис. 5.8: Оператор never
 |}
@@ Строка 275: / Строка 280: @@
 ! [[Файл:Psl fig5.9.png]]
 |-
-| (i) Assertion 5.8a does not hold
+| (i) Утверждение 5.8a не выполняется
 |-
 |<pre>
@@ Строка 281: / Строка 286: @@
 </pre>
 |-
-! Fig. 5.9: More about the never operator
+! Рис. 5.9: Еще об опрераторе never
 |}
 ==5.4 SERE repetition operators (<code>[*n]</code>, <code>[=n]</code>, and <code>[->n]</code>)==

@@ Строка 231: / Строка 231: @@
 strong version, holds on Trace 5.7(ii) but not on Trace 5.7(i).
 -->
-Как и временные операторы, SERE могут быть слабыми и сильными, и как и временные операторы, сильные версии SERE обозначаются восклицательным знаком (<code>!</code>). Таким образом, свойство 5.7а, правая сторона которого
+Как и временные операторы, SERE могут быть слабыми и сильными, и как и временные операторы, сильные версии SERE обозначаются восклицательным знаком (<code>!</code>). Таким образом, свойство 5.7а, правая сторона которого - сильный SERE, выполняется только, если будет достигнут цикл, в котором встречается <code>ack</code>. Другими словами, слабая версия SERE позволяет нам принимать тракт, который является “слишком коротким”, в то время как сильная версия предполагает, что мы должны добраться до конца SERE. Таким образом, в то время как свойство 5.7a выполняется на тракте 5.7(i), также как и на тракте 5.7(ii), свойство 5.7b, сильная версия, выполняется в тракте 5.7(ii), но не в тракте 5.7(i).
 {| align=center
@@ Строка 243: / Строка 243: @@
 </pre>
 |-
-! Fig. 5.7: A weak SERE holds even if the trace is “too short”, while a strong SERE
+! Рис. 5.7: Слабый SERE выполняется даже, если тракт “слишком короткий”, в то время как сильный SERE,
-must “reach the end”
+должен “достигать конца”
 |}

@@ Строка 217: / Строка 217: @@
 |}
-==5.2 Weak and strong SEREs==
+==5.2 Слабый и сильный SERE==
 Like temporal operators, SEREs come in weak and strong versions, and like
 temporal operators, the strong version of a SERE is indicated by an exclama-
@@ Строка 229: / Строка 230: @@
 Property 5.7a holds on Trace 5.7(i) as well as Trace 5.7(ii), Property 5.7b, the
 strong version, holds on Trace 5.7(ii) but not on Trace 5.7(i).
+-->
 {| align=center
@@ Строка 244: / Строка 246: @@
 must “reach the end”
 |}
 ==5.3 The <code>never</code> operator applied to a SERE==

@@ Строка 194: / Строка 194: @@
 phenomenon, see Section 13.4.2.
 -->
-В трактах 5.4(i) и 5.4(ii) присутствует единичное утверждение сигнала <code>req_in</code>. Если бы здесь было множественные утверждения <code>req_in</code>, то, конечно же, мы должны были бы идентифицировать множественные if-then пары, как показано в тракте 5.5(i). Отметим, что if-часть другой if-then пары может начинаться, перед завершение выполнения if-части или  then-части предыдущей if-then пары. Например, вторая if-then пара начинается в седьмом цикле, перед тем, как выполнится then-часть первой пары. Третья if-then прара начинается в цикле 8, перед тем как выполнятся then-часть первой пары и if-часть второй пары. Мы могли видеть такой вид перекрытия ранее, в трактах 2.2(ii) и 2.3(iii).
+В трактах 5.4(i) и 5.4(ii) присутствует единичное утверждение сигнала <code>req_in</code>. Если бы здесь было множественные утверждения <code>req_in</code>, то, конечно же, мы должны были бы идентифицировать множественные if-then пары, как показано в тракте 5.5(i). Отметим, что if-часть другой if-then пары может начинаться, перед завершение выполнения if-части или  then-части предыдущей if-then пары. Например, вторая if-then пара начинается в седьмом цикле, перед тем, как выполнится then-часть первой пары. Третья if-then прара начинается в цикле 8, перед тем как выполнятся then-часть первой пары и if-часть второй пары. Мы могли видеть такой вид перекрытия ранее, в трактах 2.2(ii) и 2.3(iii). Отметим, что в тракте 5.5(i) утверждение <code>ack</code> в цикле 16 завершает then-часть второй и третьей if-then пары. Для более глубокого объяснения этого феномена,смотрите раздел 13.4.2.
+<!--
 Properties 5.6a and 5.6b hold on Trace 5.6(i) because there is no sequence
 of cycles matching the left-hand side, thus the else-parts default to true at
 every cycle.
+-->
 {| align=center
 ! [[Файл:Psl fig5.6.png]]
 |-
-! (i) Properties 5.6a and 5.6b both hold
+! (i) Свойства 5.6a и 5.6b выполняются
 |-
 |<pre>
@@ Строка 213: / Строка 214: @@
 </pre>
 |-
-! Fig. 5.6: The else-part of a suffix implication defaults to true
+! Рис. 5.6: else-часть суффиксной импликации по-умолчанию утверждена
 |}

@@ Строка 151: / Строка 151: @@
 |}
+<!--
 Recall that the logical implication operator (<code>-></code>) can be understood as an
 if-then expression, with the else-part being implicitly true. The suffix implica-
@@ Строка 162: / Строка 162: @@
 of the ''suffix'' of the trace that remains once the if-part has been seen. This is
 illustrated for Properties 5.4a and 5.4b in Traces 5.4(i) and 5.4(ii).
+-->
 {| align=center
 ! [[Файл:Psl fig5.5.png]]
 |-
-! (i) A trace having multiple if-then pairs. Property 5.5a holds.
+! (i) Тракт имеет множественные if-then пары. Свойство 5.5a выполняется.
 |-
 |<pre>
@@ Строка 174: / Строка 176: @@
 </pre>
 |-
-! Fig. 5.5: The if-part of another if-then pair may begin before the if-part or the
+! Рис. 5.5:  if-часть другой if-then пары может начаться перед тем, как if-часть или
-then-part of a previous if-then pair has completed
+then-часть предыдущей if-then пары выполниться
 |}
+<!--
 In Traces 5.4(i) and 5.4(ii) there is a single assertion of signal <code>req_in</code>.
 If there are multiple assertions of <code>req_in</code>, then of course we will be able to
@@ Строка 191: / Строка 193: @@
 part of the second and of the third if-then pair. For a deeper discussion of this
 phenomenon, see Section 13.4.2.
 Properties 5.6a and 5.6b hold on Trace 5.6(i) because there is no sequence
@@ Строка 211: / Строка 215: @@
 ! Fig. 5.6: The else-part of a suffix implication defaults to true
 |}
 ==5.2 Weak and strong SEREs==

@@ Строка 43: / Строка 43: @@
 -->
 Как использовать SERE? Во-первых, SERE может также быть под-свойством. Например, свойство 5.2a выполняется, если существует утверждение  <code>req_in && gnt</code>, далее начиная со следующего цикла, мы видим последовательность циклов отмеченных SERE 5.1a. Свойство 5.2a выполняется на тракте 5.2(i).
-−
 NOTE: A SERE is a property, but a property is not a SERE. Thus, while
 you can use a SERE as an operand of a temporal operator, you cannot embed
 a temporal operator such as <code>always</code> or <code>next</code> inside of a SERE.
 Suppose now that we have a situation similar to that of Property 5.2a, but
 in which a grant (assertion of signal <code>gnt</code>) is given the cycle ''after'' the assertion of
@@ Строка 59: / Строка 63: @@
 This is slightly confusing, and indeed Property 5.3a is not in
 the simple subset of PSL discussed in Chapter 9.
 Let’s modify Property 5.3a as shown in Property 5.3b. Now a single <code>next</code>
 operator is applied to both <code>gnt</code> and the SERE, which are both operands of
@@ Строка 67: / Строка 74: @@
 <code>gnt</code>, we can manipulate Property 5.3b by adding a <code>next</code> as in Property 5.3c.
 However, the suffix implication operators provide a much easier way.
+-->
 {| align=center
 ! [[Файл:Psl fig5.1.png]]
 |-
-!(i) SERE 5.1a matches both 1 and 2. SERE 5.1b matches 1, but not 2.
+!(i) SERE 5.1a отмечает 1 и 2. SERE 5.1b отмечает 1, но не 2.
 |-
 |<pre>
@@ Строка 79: / Строка 87: @@
 </pre>
 |-
-! Fig. 5.1: Two simple SEREs
+! Рис. 5.1: Два простых SEREs
 |}
@@ Строка 86: / Строка 94: @@
 ! [[Файл:Psl fig5.2.png]]
 |-
-!(i) Property 5.2a holds
+!(i) Свойство 5.2a выполняется
 |-
 |<pre>
@@ Строка 93: / Строка 101: @@
 </pre>
 |-
-! Fig. 5.2: A SERE is a property
+! Рис. 5.2:  SERE - свойство
 |}
@@ Строка 107: / Строка 115: @@
 </pre>
 |-
-! Fig. 5.3: Property 5.3a is not in the simple subset. Properties 5.3b and 5.3c are
+! Рис. 5.3: Свойство 5.3a не из простого подмножества. Свойства 5.3b и 5.3c из простого подмножества,
-in the simple subset, but are difficult to read. These properties can be
+ но они сложны для чтения. Эти свойства можно выразить проще, используя суффиксную импликацию.
-expressed more easily using suffix implication.
 |}
-==5.1 Suffix implication (<code>|-></code> and <code>|=></code>)==
+==5.1 Суффиксная импликация (<code>|-></code> и <code>|=></code>)==
 The ''suffix implication'' operators (<code>|-></code> and <code>|=></code>) provide a way to link two
 SEREs in such a way that the right-hand side starts when the left-hand side
@@ Строка 125: / Строка 133: @@
 ier to grasp than the equivalent property without suffix implication, and both
 belong to the simple subset, discussed in Chapter 9.
@@ Строка 138: / Строка 148: @@
 </pre>
 |-
-! Fig. 5.4: Suffix implication
+! Рис. 5.4: Суффиксная импликация
 |}

PSL/A Practical Introduction to PSL/SERE Style - История изменений

Valentin: /* 5.4 Операторы повторения SERE ([*n], [=n], и [->n]) */

Valentin: /* 5.4 Операторы повторения SERE ([*n], [=n], и [->n]) */

Valentin: /* 5.4 SERE repetition operators ([*n], [=n], and [->n]) */

Valentin: /* 5.3 The never operator applied to a SERE */

Valentin: /* 5.2 Слабый и сильный SERE */

Valentin: /* 5.2 Weak and strong SEREs */

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

Valentin: /* 5.1 Суффиксная импликация (|-> и |=>) */

Valentin: /* Стиль SERE */

Valentin: /* 5.4 Операторы повторения SERE ([n], [=n], и [->n]) /

Valentin: /* 5.4 Операторы повторения SERE ([n], [=n], и [->n]) /

Valentin: /* 5.4 SERE repetition operators ([n], [=n], and [->n]) /