The Designer's Guide To PSL/ru - История изменений

ANA: /* Простые свойства */

2013-09-25T14:26:52Z

‎Простые свойства

ANA: /* Структура PSL */

2013-09-25T13:53:50Z

‎Структура PSL

Valentin: /* Еще PSL? */

2013-09-21T13:26:36Z

‎Еще PSL?

Valentin: /* More PSL? */

2013-09-21T13:25:44Z

‎More PSL?

Valentin: /* Semantics */

2013-09-21T13:21:54Z

‎Semantics

Valentin: /* Sequences */

2013-09-19T17:12:17Z

‎Sequences

Valentin: /* Strong Operators and Liveness Properties */

2013-09-18T17:59:49Z

‎Strong Operators and Liveness Properties

Valentin: /* Временная логика */

2013-09-17T16:26:45Z

‎Временная логика

Valentin: /* Temporal Logic */

2013-09-15T16:12:22Z

‎Temporal Logic

Valentin: /* Simple Properties */

2013-09-15T15:34:43Z

‎Simple Properties

@@ Строка 148: / Строка 148: @@
 However, this form of property is not particularly useful, since it is vulnerable to race hazards. It is more common to introduce a sampling event or clock.
 -->
-Однако, эта форма свойств практически не используется, т.к. является уязвимой для многих возможных рисков. Наиболее основным является представление разделенных событий или часов.
+Однако, эта форма свойств практически не используется, т.к. является уязвимой для многих возможных рисков. Наиболее основным является задания выборки событий или синхросигнала.
   assert (always CONDITION) @(posedge clk);
@@ Строка 155: / Строка 155: @@
 It is also possible to define a default clock and thus avoid the need to repeat the explicit clock operator <code>@</code> in every single assertion.
 -->
-Также возможно определить часы по умолчанию и таким образом избежать потребности в повторении явного оператора времени <code>@</code> для каждого отдельного утверждения.
+Также возможно определить синхросигнал по умолчанию и, таким образом, избежать потребности в повторении явного оператора синхросигнала <code>@</code> для каждого отдельного утверждения.
   default clock = (posedge clk);
@@ Строка 163: / Строка 163: @@
 It is more common still for a property to take the form of an implication, with a pre-condition that must be satisfied before the main condition is checked.
 -->
-Основным, для свойств, остается принятие формы импликации, с предварительным условием, которое должно быть выполнено до того, как основное условие будет проверено.
+Часто для свойств применяется форма импликации, которая включает предварительное условие, которое должно быть выполнено до того, как основное условие будет проверено.
   assert always PRECONDITION -> CONDITION;
@@ Строка 170: / Строка 170: @@
 This asserts that whenever <code>PRECONDITION</code> holds, <code>CONDITION</code> must hold in the same cycle. The symbol <code>-></code> denotes logical implication.
 -->
-Утверждение <code>PRECONDITION</code> должно поддерживаться всегда, <code>CONDITION</code> должно поддерживаться в этом же цикле. Символ <code>-></code> обозначает логическую импликацию.
+Данное утверждение означает, что всякий раз, когда выполняется предусловие <code>PRECONDITION</code>, условие <code>CONDITION</code> должно удовлетворяться в том же цикле. Символ <code>-></code> обозначает логическую импликацию.
 <!--
@@ Строка 182: / Строка 182: @@
 The sequence <code>{a;b}</code> holds if <code>a</code> holds in a cycle and <code>b</code> holds in the following cycle. The symbol <code>|-></code> placed between the two sequences denotes suffix implication, meaning that if the first sequence holds, the second sequence must hold also, with the two sequences overlapping by a single cycle.
 -->
-Последовательность <code>{a;b}</code> удерживается в цикле, если <code>a</code>, и имеет место в следующем цикле, если <code>b</code>. Символ <code>|-></code>, находящийся между двумя последовательностями, обозначает окончание импликации, это значит, что если первая последовательность удерживается, то вторая также удерживается, две последовательности совмещаются одним циклом.
+Последовательность <code>{a;b}</code> выполняется, если условие <code>a</code> верно в текущем цикле, а <code>b</code> b — в следующем. Символ <code>|-></code>, находящийся между двумя последовательностями, обозначает суффиксную импликацию (suffix implication), это значит, что если первая последовательность выполняется, то вторая также должна выполняться, причем две последовательности пересекаются в одном цикле.
 <!--
 Finally, it is common for properties to include a terminating condition (such as a reset) which will cause the property to be abandoned mid-way through the matching of a temporal sequence.
 -->
-В итоге для свойств включающих временные условия (таких как сброс), которые могут прерывать свойства в любой момент временной последовательности.
+И наконец, для свойств, включающих условие остановки (таких как сброс (reset)), при активации которого прервётся проверка свойства в любой момент временной последовательности.
   assert (always ({a;b} |-> {c;d} abort reset))
@@ Строка 194: / Строка 194: @@
 When the reset goes true, the obligation for the suffix implication to hold is removed, whether or not there has been a partial match between the property and the actual state of the design.
 -->
-Когда сброс принимает значение правда, обязательство удержания окончания импликации удаляется, и проверяется наличие совпадений между свойством и актуальным состоянием проекта.????
+Когда reset принимает значение истины, обязательство удержания окончания импликации удаляется, и проверяется наличие совпадений между свойством и актуальным состоянием проекта.????
 ==Временная логика==

@@ Строка 87: / Строка 87: @@
 -->
-Язык PSL официально структурирован в четыре отдельных уровня: булевый уровень,временной,уровень верификации и уровень моделирования. Слой верификации и временной слой имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом говорят,что PSL сочетает три вкуса:VHDL, Verilog and GDL. вкус напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
+Язык PSL официально структурирован в четыре отдельных уровня (layers - слоя): булевый уровень (boolean), временной (temporal), уровень верификации (verification) и уровень моделирования (modelling). Уровень верификации и временной уровень имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом говорят, что PSL сочетает три «вкуса»/«привкуса» (flavour): VHDL, Verilog и GDL. «Вкус» напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
-−
-Язык PSL официально структурирован в четыре отдельных уровня: булевый уровень,временной,уровень верификации и уровень моделирования. Слой верификации и временной слой имеют свой собственный синтаксис, в то время как уровень моделирования и булевый уровень заимствуют синтаксис из лежащего в основе HDL. Таким образом говорят,что PSL сочетает три вкуса:VHDL, Verilog and GDL. вкус напрямую определяет синтаксис используемый на булевом уровне и уровне моделирования, а также немного влияет на синтаксис временного уровня.
 <!--
 The boolean layer consists of boolean expressions containing variables and operators from the underlying language. Formally, the boolean layer consists of any expression that is allowed as the condition in an <code>if</code> statement in the underlying language. As such, expressions in the boolean layer are evaluated at a single point in time.
 -->
-Булевый уровень состоит из булевых выражений, включающих в себя переменные и операторы основополагающего языка. Формально, булевый уровень состоит из выражений, которые представляют собой условия для оператора <code>if</code> сновополагающего языка. Как таковые, выражения булевого уровня оцениваются в определенный момент времени.
+Булевый уровень состоит из булевых выражений, включающих в себя переменные и операторы основополагающего языка. Формально, булевый уровень состоит из выражений, которые представляют собой условия для оператора <code>if</code> базового языка. Как таковые, выражения булевого уровня оцениваются в определенный момент времени.
   (a &   (a-1)) == 0         // Verilog flavour
@@ Строка 102: / Строка 98: @@
 <!--
 The temporal layer forms the major part of the PSL language. As well as including expressions from the boolean layer, expressions in the temporal layer may include temporal operators and Sequential Extended Regular Expressions or SEREs. It is usual for temporal expressions to be sampled on a clock. PSL is intended for designs with synchronous timing.
-<<<<<<<  :
+-->
   (always req -> next (ack until grant)) @clk
 <!--
 The verification layer consists of verification directives together with syntax to group PSL statements and bind them to HDL modules. A verification directive is an instruction to a tool to tell it what to do with a property. The principle verification directives are <code>assert</code> (the tool should attempt to prove the property), <code>assume</code> (the tool may assume the given property is true) and <code>cover</code> (the tool should measure how often the given property occurs during simulation).
 -->
-Уровень верификации состоит из директив верификации и синтаксиса,позволяющего группировать PSL-операторы и связывать их с HDL-модулями. Директивы верификации- это инструкции программе, которые поясняют, что делать со свойствами. Принцип директив верификации следующий: <code>assert</code> (программа должна попытаться доказать свойство), <code>assume</code> (программа может предположить, что данное свойство справедливо) и <code>cover</code> (программа должна подсчитать, как часто используется свойство во время моделирования).
+Уровень верификации состоит из директив верификации и синтаксических конструкций, позволяющих группировать PSL-операторы и связывать их с HDL-модулями. Директивы верификации — это инструкции программе, которые поясняют, что делать со свойствами. Принцип директив верификации следующий: <code>assert</code> (программа должна попытаться доказать свойство), <code>assume</code> (программа может предположить, что данное свойство истинно) и <code>cover</code> (программа должна подсчитать, как часто используется свойство во время моделирования).
-−
   assert (always req -> ack) @clk;
 <!--
 Verification directives such as the one above can be embedded in the HDL code as comments. Alternatively, verification directives can be grouped into verification units, or <code>vunit</code>s, and placed in a separate file. There are actually three kinds of verification unit, with the <code>vunit</code> being the most general, the <code>vprop</code> containing nothing but assertions, and the <code>vmode</code> containing anything but assertions. A verification unit can be explicitly bound to an HDL module or design unit.
 -->
 Директивы верификации, такие как приведены выше, могут быть встроены в HDL-код, как комментарии. С другой стороны, директивы верификации могут быть сгруппированы в блоках верификации или <code>vunit</code>s, и размещаться в отдельном файле. Существует три вида блоков верификации, <code>vunit</code> является наиболее общим, <code>vprop</code> не содержит ничего, кроме утверждений, <code>vmode</code> может содержать не только утверждения. Блок верификации может быть ясно связан с HDL-модулем или блоком проекта.
@@ Строка 138: / Строка 122: @@
 <!--
 The modelling layer allows extra code fragments from the underlying language to be included with the properties to augment what is possible using PSL alone. For example, the modelling layer could be used to calculate the expected value of an output.
 -->
-Уровень моделирования позволяет дополнительным фрагментам кода, из основополагающего языка, включаться в свойства и расширять их, что делает возможным использовать PSL отдельно. Например, уровень моделирования может использоваться для расчета ожидаемых выходных значений.
+Уровень моделирования позволяет дополнительным фрагментам кода, из базового языка, включаться в свойства и расширять их, что делает возможным использовать PSL отдельно (самостоятельно). Например, уровень моделирования может использоваться для расчета ожидаемых выходных значений.
 <!--
->>>>>>> ( )
+The modelling layer includes some additional language constructs and convenience functions. For example, the <code>prev()</code> function returns the value of an expression in the previous cycle. Currently, these functions are only part of the Verilog flavour modelling layer, but most tools unofficially support VHDL flavoured versions too.
-The modelling layer includes some additional language constructs and convenience functions. For example, the <code>prev()</code> function returns the value of an expression in the previous cycle. Currently, these functions are only part of the Verilog flavour modelling layer, but most tools unofficially support VHDLflavoured versions too.
-<<<<<<<  :
-=======
 -->
-Уровень моделирования включает некоторые дополнительные языковые конструкции и удобные функции. Например, функция <code>prev()</code> возвращает значение выражения прошлого цикла. В настоящее время эти функции только часть уровня моделирования со вкусом Verilog, большинство программ, неофициально, поддерживают версии со вкусом VHDL.
+Уровень моделирования включает некоторые дополнительные языковые конструкции и удобные функции. Например, функция <code>prev()</code> возвращает значение выражения прошлого цикла. В настоящее время эти функции только часть уровня моделирования со «вкусом» Verilog, большинство программ, неофициально, поддерживают версии со «вкусом» VHDL.
 <!--
 PSL keywords are case sensitive. As you've probably noticed above, statements are terminated by a semi-colon <code>;</code>.
 -->
 Ключевые слова PSL чувствительны к регистру. Как вы уже могли заметить, операторы разделяются <code>;</code>.

@@ Строка 379: / Строка 379: @@
 ==Еще PSL?==
-Изучайте больше PSL и используйте его для улучшения своего процесса верификации. Подумайте о вступлении в  [http://www.doulos.com/content/training/assertion_verification_psl_training.php Assertion-Based Verification with PSL]. Или,если вы хотите изучать VHDL или Verilog на более продвинутом уровне, загляните сюда [http://www.doulos.com/content/training/vhdl_expert.php Expert VHDL] or [http://www.doulos.com/content/training/expert_verilog_training.php Expert Verilog] classes now including PSL.
+Изучайте больше PSL и используйте его для улучшения своего процесса верификации. Подумайте о вступлении в  [http://www.doulos.com/content/training/assertion_verification_psl_training.php Assertion-Based Verification with PSL]. Или,если вы хотите изучать VHDL или Verilog на более продвинутом уровне, загляните сюда [http://www.doulos.com/content/training/vhdl_expert.php Expert VHDL] или [http://www.doulos.com/content/training/expert_verilog_training.php Expert Verilog] здесь присутствует и PSL.
 == Источник ==

@@ Строка 377: / Строка 377: @@
 Семантика SERE определена отчасти по-разному, учитывая набор всех возможных последовательностей, которые могут быть сгенерированы из конкретного SERE. Например, SERE <code>{a[+]}</code> генерирует последовательности <code>{a}</code>, <code>{a;a}</code>, <code>{a;a;a}</code>,... SERE ''плотно удерживается'' на конечном пути, если последовательность состояний, которые составляют этот путь, принадлежит набору последовательностей сгенерированых SERE. Другими словами, SERE, которая соответствует конкретной конечной последовательности состояний, ''плотно удерживается'' в этом пути, в то время как свойство ''удерживается'' в конкретном цикле, если это соответствует конечной или бесконечной последовательности состояний, ожидая времени, чтобы начать с этого цикла.
-==More PSL?==
+==Еще PSL?==
-−
-Learn more about PSL and using PSL to improve your verification process. Consider attending [http://www.doulos.com/content/training/assertion_verification_psl_training.php Assertion-Based Verification with PSL]. Or, if you are ready to learn some advanced VHDL or Verilog then consider the new improved [http://www.doulos.com/content/training/vhdl_expert.php Expert VHDL] or [http://www.doulos.com/content/training/expert_verilog_training.php Expert Verilog] classes now including PSL.
 == Источник ==

@@ Строка 360: / Строка 360: @@
 * <code>{seq1} && {seq2}</code> означает, что обе должны удерживаться и быть одной длины
-==Semantics==
+==Семантика==
 The semantics of PSL are declarative rather than imperative, meaning that PSL allows you to describe and reason about an abstract succession of states in such a way as to be equally applicable for generating simulation checkers, for formal proof and for documentation. Unlike some other current property languages, the definition of PSL is not tied to the idea of a checker implemented as a finite state machine executing in monotonically increasing simulation time. Indeed, it is possible to write PSL properties that cannot be implemented efficiently as simulation checkers. Those properties that can be implemented as efficient finite state machine automata are said to belong to the ''simple subset'' of PSL. Most practical properties fall in the simple subset.
 The semantics of the temporal layer are defined by considering all possible paths through all possible states of a design. A PSL property is said to hold in a particular cycle if it matches (depending on the meaning of the temporal operator in question) a path starting with the current cycle and extending a finite or infinite number of cycles into the future. In other words, to see if a particular property holds, you should choose a particular cycle to start from and then peer forward into the future, comparing the actual state of the design with the obligations imposed by the temporal operators. For a typical PSL property (i.e. one that uses the <code>always</code> operator), this rule applies equally and independently for every cycle.
 The semantics of SEREs is defined somewhat differently by considering the set of all possible sequences that can be generated from a particular SERE. For example, the SERE <code>{a[+]}</code> generates the sequences <code>{a}</code>, <code>{a;a}</code>, <code>{a;a;a}</code>,... A SERE is said to ''hold tightly'' on a finite path if the sequence of states that constitute that path belongs to the set of sequences generated by the SERE. In other words, a SERE that matches a particular finite sequence of states is said to ''hold tightly'' over that path, whereas a property is said to ''hold'' in a particular cycle if it matches a finite or infinite sequence of states, looking forward in time starting from that cycle.
 ==More PSL?==

@@ Строка 320: / Строка 320: @@
   always P
-==Sequences==
+==Последовательности==
 The sequence, which is the syntactic equivalent of the timing diagram, often provide the most convenient way to write properties in PSL, with time advancing as we move from left to right through the text. The Sequential Extended Regular Expression or SERE (which rhymes with beer) permits a compact abbreviation for many common timing relationships.
 Consider the following assertion:
   assert always {a;b} |-> {c;d};
 As was explained above, the semicolon operator moves forward one cycle, whilst the suffix implication operator <code>|-></code> means that the first sequence must always be followed by the second with an overlap of one cycle. (There is an alternative suffix implication operator <code>|=></code> which requires that the two sequences do not overlap.)
 SEREs permit longer sequences and families of related sequences to be written in a compact notation. For example:
-* <code>{a[*2]}</code> means <code>{a;a}</code>
+<!--
-* <code>{a[+]}</code> means <code>{a;a;...;a}</code> with a repeated one or more times
-* <code>{a[*]}</code> means <code>{a;a;...;a}</code> with a repeated zero of more times
-* <code>{[*]}</code> matches any sequence whatsoever
-* <code>{a[=2]}</code> means <code>{[*];a;[*];a;[*]}</code>, i.e. non-consecutive repetition
-* <code>{a[*1 to 3]}</code> means <code>{a}</code> or <code>{a;a}</code> or <code>{a;a;a}</code>
-−
 There are also several operators that work with whole sequences:
-* <code>{seq1} | {seq2}</code> means that one or the other sequence must hold
+* <code>{seq1} | {seq2}</code> означает, что одна из двух последовательностей должна удерживаться
-* <code>{seq1} & {seq2}</code> means that both sequences must hold
+* <code>{seq1} & {seq2}</code> означает, что обе последовательности должны удерживаться
-* <code>{seq1} && {seq2}</code> means that both must hold and be of equal length
+* <code>{seq1} && {seq2}</code> означает, что обе должны удерживаться и быть одной длины
 ==Semantics==

@@ Строка 280: / Строка 280: @@
 Смысл заключается в том, что когда бы <code>req</code> не принимал значение "правда", <code>ack</code> должен принять значение "правда" по крайней мере один раз в период, начиная со следующего цикла и заканчивая последним циклом,перед тем, как <code>grant</code> примет значение "правда". Не существует обязательного значения для <code>ack</code> ни в цикле, в котором <code>req</code> принимает значение "правда", ни в цикле, в котором <code>grant</code> принимает значение "правда". Не существует никаких правил, по которым  <code>grant</code> должен, когда-либо принимать значение "правда", следуя за <code>req</code>, в это случае <code>ack</code>, также, не должен принимать этого значения. Другими словами, следуя за <code>req</code>, и <code>ack</code>, и <code>grant</code> могут оставаться в значении "ложь" неопределенное время.
-==Strong Operators and Liveness Properties==
+==Сильные операторы и живучие свойства==
-Consider the following assertion:
+<!--
   assert always req -> eventually! ack;
 This asserts that whenever <code>req</code> is true, <code>ack</code> must go true at some future cycle, but there is no upper limit on the time by which <code>ack</code> is required to go true. This is known as a '''liveness''' property. Liveness properties are characterised by the fact that they do not possess a finite counter-example, and hence in principle they cannot be disproved by simulation. However, liveness properties can in principle be proved or disproved by static model checking tools. Properties that do possess finite counter-examples are known as safety properties.
 Liveness properties are written in PSL using strong operators, all of which include an exclamation mark in their name. There exist strong forms of several temporal operators, including <code>next!</code>, <code>until!</code> and <code>before!</code>. For example:
+-->
   assert always req -> next (ack until! grant);
 This means that whenever <code>req</code> is true, <code>ack</code> is true in the following cycle, <code>ack</code> remains true until the first subsequent cycle in which grant is true '''''and''' grant must go true eventually''.
 Non-negated strong operators always create liveness properties, but you might care to ponder the fact that:
   not eventually! (not P)
 is actually formally equivalent to
   always P

@@ Строка 238: / Строка 238: @@
 means that whenever the HDL signal <code>req</code> is true, the HDL signal <code>grant</code> must be true in the following cycle. The meaning of a cycle will typically be specified either by defining a default clock or by including the clocking operator @ within the property. Note that when <code>req</code> is true, this assertion says nothing about the value of <code>grant</code> in any cycle other than the immediately following cycle. Also, it says nothing about the value of <code>grant</code> when <code>req</code> is false. It only says that whenever <code>req</code> is true, it must be the case that <code>grant</code> is true in the very next cycle.
 -->
-означает, что когда бы HDL-сигнал <code>req</code> не принимал значение "правда", HDL-сигнал <code>grant</code> должен принимать значение "правда" в следующем цикле.
+означает, что когда бы HDL-сигнал <code>req</code> не принимал значение "правда", HDL-сигнал <code>grant</code> должен принимать значение "правда" в следующем цикле. Цикл имеет типичное представление обозначенное часами по умолчанию или включая оператор времени с течением свойства. Следует отметить, что когда <code>req</code> принимает значение "правда", то это утверждение ничего не говорит о значении <code>grant</code> в любом другом цикле,кроме последующего. Также ничего не говорит о значении <code>grant</code>, когда <code>req</code> принимает значение "ложь". Это говорит лишь о том, что когда бы <code>req</code> не принимало значение "правда", всегда найдется случай, в котором <code>grant</code> примет значение "правда" уже на следующем цикле.
 The <code>next</code> operator can take a number of cycles as an argument, enclosed in square brackets, as in:
   assert always req -> next[2] (grant);
 This means that whenever <code>req</code> is true, <code>grant</code> must be true two cycles later. It says nothing about the value of <code>grant</code> one cycle after <code>req</code> is true. An interesting feature of this assertion is that it must hold in every single cycle, such that if <code>req</code> were true for three consecutive cycles, say, so must <code>grant</code> be true for three consecutive cycles, but with a latency of two cycles. If this assertion is implemented as a simulation check, it would be re-triggered every time <code>req</code> is true, such that concurrent invocations of the simulation check are effectively pipelined.
 The meaning of the <code>until</code> operator is a bit more subtle:
   assert always req -> next (ack until grant);
 This asserts that whenever <code>req</code> is true, <code>ack</code> is true in the following cycle and <code>ack</code> remains true until the first subsequent cycle in which <code>grant</code> is true. There is no obligation on the value of <code>ack</code> in the cycle in which <code>grant</code> goes true, nor in any subsequent cycles (unless the check is re-triggered by <code>req</code> going true once more). If <code>req</code> goes true and then <code>grant</code> goes true in the following cycle, <code>ack</code> need not go true at all. On the other hand, there is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> would have to remain true indefinitely.
 The cycle in which the left-hand operand to <code>until</code> is first required to hold is determined by the context in which that operator appears. In the example above, the obligation for <code>ack</code> to be true begins in the cycle after <code>req</code> is true. Once again, the always operator requires that the temporal expression shall hold in every cycle, and hence concurrent invocations of the check are pipelined.
+-->
-Finally, the before operator:
+Цикл, в котором левый операнд <code>until</code> вызывается первым, определен контекстом, в котором этот оператор появился. В пример выше, <code>ack</code> должен принимать значение "правда" в цикле, после того, как <code>req</code> примет значение "правда".
   assert always req -> next (ack before grant);
 This asserts that whenever <code>req</code> is true, <code>ack</code> must be true at least once in the period starting in the following cycle and ending in the last cycle before <code>grant</code> is true. There are no obligations on the value of <code>ack</code> in the cycle in which <code>req</code> goes true, nor in the cycle in which <code>grant</code> goes true. There is no obligation for <code>grant</code> to ever go true following a <code>req</code>, in which case <code>ack</code> need not go true either. In other words, following a <code>req</code> both <code>ack</code> and <code>grant</code> could remain false indefinitely.
 ==Strong Operators and Liveness Properties==

@@ Строка 221: / Строка 221: @@
 Когда сброс принимает значение правда, обязательство удержания окончания импликации удаляется, и проверяется наличие совпадений между свойством и актуальным состоянием проекта.????
-==Temporal Logic==
+==Временная логика==
 The temporal operators of the foundation language provide syntactic sugaring on top of the LTL operators. These temporal operators include <code>always</code>, <code>never</code>, <code>next</code>, <code>until</code> and <code>before</code>, amongst others. The meaning of these operators is quite intuitive, but there are a few surprises.
 The <code>always</code> operator holds if its operand holds in every single cycle, whilst the <code>never</code> operator holds if its operand fails to hold in every single cycle. The <code>next</code> operator holds if its operand holds in the cycle that immediately follows. Hence the assertion
   assert always req -> next grant;
 means that whenever the HDL signal <code>req</code> is true, the HDL signal <code>grant</code> must be true in the following cycle. The meaning of a cycle will typically be specified either by defining a default clock or by including the clocking operator @ within the property. Note that when <code>req</code> is true, this assertion says nothing about the value of <code>grant</code> in any cycle other than the immediately following cycle. Also, it says nothing about the value of <code>grant</code> when <code>req</code> is false. It only says that whenever <code>req</code> is true, it must be the case that <code>grant</code> is true in the very next cycle.
+-->
 The <code>next</code> operator can take a number of cycles as an argument, enclosed in square brackets, as in: