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

Valentin: /* 3.5 Reporting a failure */

2013-11-25T11:04:35Z

‎3.5 Reporting a failure

Valentin: /* 3.4 Текущий цикл, субтракты, модульность */

2013-11-25T10:50:09Z

‎3.4 Текущий цикл, субтракты, модульность

Valentin: /* 3.4 Current cycle, sub-traces, and modularity */

2013-11-25T09:29:21Z

‎3.4 Current cycle, sub-traces, and modularity

Valentin: /* 3.3 Designs and traces */

2013-11-25T07:25:29Z

‎3.3 Designs and traces

Valentin: /* 3.2 Понятие времени */

2013-11-15T18:56:19Z

‎3.2 Понятие времени

Valentin: /* 3.2 Понятие времени */

2013-11-15T10:54:41Z

‎3.2 Понятие времени

Valentin: /* 3.2 The notion of time */

2013-11-15T09:22:43Z

‎3.2 The notion of time

Valentin: /* 3.1 Утверждения против свойств */

2013-11-15T08:43:24Z

‎3.1 Утверждения против свойств

Valentin: /* Some Philosophy */

2013-11-13T10:59:37Z

‎Some Philosophy

ANA: /* 3.3 Designs and traces */

2013-11-13T10:19:40Z

‎3.3 Designs and traces

Внесённые изменения

@@ Строка 261: / Строка 261: @@
 Предварительно, например в рассматриваемых утверждениях 2.2а и 2.3b, мы видели случаи, где были перекрытия между циклами вовлеченными в удовлетворение двух разных случаев левой стороны логической импликации. Эти перекрытия вызваны присутствием оператора <code>always</code> в свойстве. Если мы удалим этот оператор, вопрос перекрытия исчезнет из утверждений 2.2a и 2.3b. Перекрытие утверждения 3.3а отличается от перекрытия утверждений 2.2a и 2.3b, и это очень важно: утверждение 3.3a написано таким образом, что циклы вовлеченные в подсчет левой стороны логической импликации перекрываются с циклами правой логической импликации: подсчитывая часть “if” логической вовлекают рассматриваемый текущий цикл, а также “предстоящие” шесть циклов, в то время как подсчет части “then” логической импликации вовлекает рассматриваемый текущий цикл и также “предстоящие” два цикла. Таким образом,перекрытие появляется от самой логической импликации. Такой стиль PSL свойств, обычно, труден для новых пользователей PSL, и вообще это не интуитивный способ использования языка. Поэтому, такие свойства не рекомендуется использовать, и <code>простое подмножество</code> ограничений языка PSL не позволяет использование таких свойств. Мы обсудим простое подмножество в деталях поздней. На данный момент, запомните, что если вы написали свойство, в котором циклы вовлечены в подсчет левой стороны одного оператора перекрываются в течение более одного цикла с циклами вовлеченными для подсчета правой стороны того же оператора, то вы написали свойство не относящиеся к простому подмножеству.
-=== 3.5 Reporting a failure ===
+=== 3.5 Сообщение об ошибке ===
 Consider Assertion 3.4a on the traces shown in Figure 3.4. Obviously, Assertion
 .4a does not hold on them. Now consider four different verification tools,
@@ Строка 271: / Строка 272: @@
 reports a failure at the end of the trace, and Tool 4 reports a failure at cycle
 , when <code>a</code> is asserted.
 Which tool is correct? The answer is that they all are. PSL defines whether
 or not a property holds on a trace – that is all. It says nothing about when
@@ Строка 281: / Строка 285: @@
 is concerned, as long as a tool indicates correctly whether or not a property
 holds on a trace, it has done its job.
+-->
 {| align=center
@@ Строка 290: / Строка 295: @@
 </pre>
 |-
-! Fig. 3.4: Four different tools reporting the failure of Assertion 3.4a on the same trace
+! Рис. 3.4: Четыре инструмент,выдающих сообщение об ошибке утверждения 3.4a на одном и том же тракте
 |}

@@ Строка 194: / Строка 194: @@
 Другой тонкий момент, что свойство может выполняться в суффиксе тракта,а не на самом тракте. Таким образом, свойство <code>always a</code> выполняется на субтракте тракта 3.2(i), начиная с циклов 12, 13, 14. Это будет важно, если мы используем свойство <code>always a</code>, как под-свойство какого-либо друо свойства. Например, утверждение 3.2c выполняется на тракте 3.2(i), потому что свойство <code>always a</code> выполняется на 12<sup>''ти''</sup> следующих циклах.
 Finally, the cycles involved in calculating the left-hand side of a logical
 implication may overlap those involved in calculating the right-hand side of
@@ Строка 203: / Строка 204: @@
 “if” part of a logical implication does not hold, then the “else” part defaults
 to true.
+-->
 {| align=center
 ! [[Файл:Psl fig3.2.png]]
 |-
-!(i) Assertions 3.2a and 3.2c hold, but 3.2b does not
+!(i) Утверждение 3.2a и 3.2c выполняются, но 3.2b нет
 |-
 |<pre>
@@ Строка 216: / Строка 218: @@
 </pre>
 |-
-! Fig. 3.2: The importance of the always operator
+! Рис. 3.2: Важность оператора always
 |}
@@ Строка 223: / Строка 225: @@
 ! [[Файл:Psl fig3.3.png]]
 |-
-!(i) An illustration of the overlap between the left- and right-hand sides of <br />
+!(i) Иллюстрация перекрытие левой и правой стороны  <br />
-Assertion 3.3a. Assertion 3.3a holds.
+утверждение 3.3a. Утверждение 3.3a выполняется.
 |-
 |<pre>
@@ Строка 230: / Строка 232: @@
 </pre>
 |-
-! Fig. 3.3: The current cycle
+! Рис. 3.3: Текущий цикл
 |}
+<!--
 Previously, for example in examining Assertions 2.2a and 2.3b, we have
 seen cases where there is an overlap between the cycles involved in satisfying
@@ Строка 256: / Строка 258: @@
 with those involved in calculating the right-hand side of the same operator,
 you have not written a property that is in the simple subset.
 === 3.5 Reporting a failure ===

@@ Строка 95: / Строка 95: @@
 Другой подход, используется дополнительным ветвлением расширения, используется дерево структуры, которое представляет несколько путей. Этот подход подходить только для формальной верификации, и, очень кратко, затрагивается в главе 11.
-=== 3.4 Current cycle, sub-traces, and modularity ===
+=== 3.4 Текущий цикл, субтракты, модульность ===
 When a PSL property composed of two or more sub-properties is checked on
 a trace, it is sometimes necessary to decide the meaning of the sub-properties
 on a sub-trace. The ''current cycle'' is the name we give to the first cycle of a
 trace or a sub-trace on which we are evaluating a property or a sub-property.
 Assuming that the cycles of a trace are numbered starting from 0, the
 current cycle of an assertion is 0. The current cycle of a sub-property of some
@@ Строка 112: / Строка 116: @@
 which has a current cycle that corresponds either to the current cycle or to
 some future cycle, etc.
 NOTE: It is very important to understand that the term “multiple instances”
 is intended to convey an intuition which is useful in understanding
@@ Строка 125: / Строка 132: @@
 <code>always</code> operator works, and a naive and inefficient implementation may well
 generate multiple instances of a checker or of a process.
 Getting back to our main point, consider the assertion <code>assert always (a -> next b);</code>. The current cycle of <code>always (a -> next b)</code> is 0. Whether or
 not <code>always (a -> next b)</code> holds at cycle 0 depends on whether or not the
@@ Строка 134: / Строка 144: @@
 and next b with a current cycle of ''N'', which means that we need to evaluate
 sub-property b with a current cycle of ''N'' + 1.
 To make the discussion more concrete, let’s consider our assertion, Assertion
 .1a, on Trace 3.1(i). Signal a holds in cycles 4 and 8. Signal <code>b</code> holds in
@@ Строка 147: / Строка 160: @@
 .1a does not hold on Trace 3.1(i) (because it does not hold on cycle 0 –
 the first cycle of the trace).
+-->
 {| align=center
@@ Строка 156: / Строка 170: @@
 </pre>
 |-
-! Fig. 3.1: A concrete example
+! Рис. 3.1: Конкретный пример
 |}
 The above explanation seems straightforward. However, the idea of modularity
 hides some subtle points – for example, that the value of the property
@@ Строка 166: / Строка 181: @@
 that <code>a</code> should hold in every cycle, you must use the <code>always</code> operator, as in
 Assertion 3.2b. Assertion 3.2b does not hold on Trace 3.2(i).
 Another subtle point is that a property can hold on a suffix of a trace
 without holding on the trace itself. Thus, the property <code>always a</code> holds on
@@ Строка 173: / Строка 191: @@
 other property. For example, Assertion 3.2c holds on Trace 3.2(i) because the
 property <code>always a</code> holds on the 12<sup>''th''</sup> next cycle.
 Finally, the cycles involved in calculating the left-hand side of a logical
@@ Строка 236: / Строка 256: @@
 with those involved in calculating the right-hand side of the same operator,
 you have not written a property that is in the simple subset.
 === 3.5 Reporting a failure ===

@@ Строка 75: / Строка 75: @@
 Тем не менее, существует путь гарантировать, что значение свойства PSL не влияет на степень детализации времени, с точки зрения программ верификации. Свойства PSL могут быть модифицированы, используя ''временное выражение'' для того, чтобы показать, что время должно быть получено во временных циклах временного выражения. В случаи временного свойства, результат программы базирующейся на циклах должен быть такой же, как и для программы базирующейся на изменениях. PSL допускает спецификацию ''времени по-умолчанию'', таким образом, что время не должно быть упомянуто отдельно для каждого свойства. Далее в этой книге мы предполагаем однократный тактовый проект под модель, базирующуюся на циклах, таким образом в большинстве примеров опущены явные упоминания о времени.
-===3.3 Designs and traces===
+===3.3 Проекты и тракты ===
 The purpose of a PSL property is to describe the desired behavior of a design.
 In order to do so, it is usually convenient to examine individual traces of that
@@ Строка 84: / Строка 85: @@
 The Foundation Language is suitable for both static (formal) and dynamic
 (simulation-based) verification.
 Another approach, used by the Optional Branching Extension (OBE), uses
 a tree structure that represents multiple paths. This approach is applicable
 only to formal verification, and is touched on very briefly in Chapter 11.
+-->
 === 3.4 Current cycle, sub-traces, and modularity ===

@@ Строка 51: / Строка 51: @@
 PSL предполагает, что время дискретно, таким образом, время состоит из последовательности оцененных циклов. Значение свойства PSL определенно по отношению к такой последовательности циклов. В этой книге, мы будем называть такую последовательность циклов ''трактом''.
 PSL does not dictate how time ticks – that is, it does not dictate how such
 a sequence of cycles is extracted from a design under verification. This means
@@ Строка 57: / Строка 58: @@
 calculated cycle-by-cycle, while an event-based simulator running on the same
 design sees a more detailed sequence of signal values.
 Nevertheless, there is a way to ensure that the meaning of a PSL property
 is not affected by the granularity of time as seen by the verification tool. PSL
@@ Строка 68: / Строка 72: @@
 the cycle-based model, and thus most examples omit the explicit mention of
 the clock. Clocks are discussed in detail in Chapters 6 and 14.
 ===3.3 Designs and traces===

@@ Строка 41: / Строка 41: @@
 must be given more consideration.
 -->
-Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении -  утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется.
+Когда Булево утверждение встроено в код, который выполняется, как в простом утверждении Java или (моделирования) VHDL, понятие времени не нуждается в определении -  утверждение проверяется всякий раз, когда заявление, содержащее утверждение выполняется. Для более сложных утверждений PSL, которые, во-первых, находяться отдельно от кода (таким образом понятие “исполнение” чужое для них), и во-вторых охватывает множество шагов во времени, понятию времени необходими уелить больше внимания.
 PSL assumes that time is discrete, that is, that time consists of a sequence
 of evaluation cycles. The meaning of a PSL property is defined relative to such
 a sequence of cycles. In this book, we will refer to such a sequence of cycles
 as a ''trace''.
 PSL does not dictate how time ticks – that is, it does not dictate how such

@@ Строка 30: / Строка 30: @@
 Как мы уже видели, утверждения PSL состоят из ключевого слова assert плюс ''свойства'' PSL для утверждения, разделенных точкой с запятой. Например, в утверждении <code>assert always (a -> next b);</code>, свойство - <code>always (a -> next b)</code>. Свойство выполняется или не выполняется в данном тракте. Утверждение, с другой стороны, указывает программе верификации, что свойство было утверждено, и требуется выполнение. Далее в книге мы будем внимательно рассматривать отличия между свойствами, которые просто описывают поведения, и утверждения,которые устанавливают требования. Например, мы можем сказать, что утверждение <code>assert always (a -> next b);</code> требует, чтобы когда бы сигнал <code>a</code> не утверждался, сигнал <code>b</code> должен будет утвердиться в следующем цикле. Однако, мы никогда не скажем такого о свойстве <code>always (a -> next b)</code>, по двум причинам. Первая - потому что если свойство используется в предположении (<code>assume always (a -> next b);</code>), то нету никаких требований. Вторая - потому что свойство может использоваться, как под-свойство более сложного свойства, и если так, то не может исходить требований от него самого.
-=== 3.2 The notion of time ===
+=== 3.2 Понятие времени ===
 When a Boolean assertion is embedded in code that is being run, like in the
 simple assertions of Java and (simulated) VHDL, the notion of time need not
@@ Строка 39: / Строка 40: @@
 to them) and which second of all span multiple time steps, the notion of time
 must be given more consideration.
 PSL assumes that time is discrete, that is, that time consists of a sequence
@@ Строка 62: / Строка 65: @@
 the cycle-based model, and thus most examples omit the explicit mention of
 the clock. Clocks are discussed in detail in Chapters 6 and 14.
 ===3.3 Designs and traces===

@@ Строка 2: / Строка 2: @@
-== Some Philosophy ==
+== Немного философии ==
-−
 We have seen some basic PSL and gotten a feel for how it is intended to be
 used. Before we continue, we discuss some of the concepts at the root of PSL.
-=== 3.1 Assertions vs. properties ===
+<!--
-−
 As we have seen, a PSL assertion is made up of the keyword assert plus
 the PSL ''property'' being asserted, followed by a semi-colon. For example, in
@@ Строка 25: / Строка 27: @@
 sub-property of a more complicated property, and as such, it does not state a
 requirement on its own.
+-->
 === 3.2 The notion of time ===