«Бог не меняет того, что (происходит) с людьми, пока они сами не изменят своих помыслов.» Коран, Сура 12:13

PSL/Дневник

Материал из Wiki
< PSL
Версия от 14:53, 21 ноября 2012; ANA (обсуждение | вклад)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Это снимок страницы. Он включает старые, но не удалённые версии шаблонов и изображений.
Перейти к: навигация, поиск
PSL
Литература
Введение в PSL
* VHDL * OS-VVM * Co-Simulation *

Содержание

страница 17

The structure of PSL is based on four layers – the Boolean layer, the temporal layer, the verification layer and the modeling layer – and comes in a numbers of flavors, which influence the syntax in a limited way. The four layers of the language are:

  • The Boolean layer is composed of Boolean expressions, that is, expressions whose value is either true or false. For example, a is a Boolean expression. PSL interprets a high signal as true, and a low signal as false, independent of whether the signal is active-high or active-low. Thus, if signal a is active-high, the Boolean expression a has the value true when a is asserted, and false when it is deasserted. And if signal b is active-low, the Boolean expression b has the value false when b is asserted and true when it is deasserted. In the remainder of this book, we will assume that all signals are active-high unless stated otherwise. Of course, it is easy to get the active-low versions of the example properties by switching a with !a and vice versa. The Boolean layer consists of any Boolean expression in the underlying flavor. For example, a && !b is a Boolean expression in the Verilog flavor stating that a holds and b does not, a[31:0]==b[31:0] is a Verilog-flavored Boolean expression stating that the 32-bit vectors a[31:0] and b[31:0] are equal, and addr1[127:0]==128’b0 is a Verilog-flavored Boolean expression stating that the 128-bit vector addr1[127:0] has the value zero.
  • The temporal layer consists of temporal properties which describe the relationships between Boolean expressions over time. For example, always (req -> next ack) is a temporal property expressing the fact that whenever (always) signal req is asserted, then (->) at the next cycle (next), signal ack is asserted.
  • The verification layer consists of directives which describe how the temporal properties should be used by verification tools. For example, assert always (req -> next ack); is a verification directive that tells the tools to verify that the property always (req -> next ack) holds. Other verification directives include an instruction to assume, rather than verify, that a particular temporal property holds, or to specify coverage criteria. The verification layer also provides a means to group PSL statements into verification units. 
vunit example1 {
  assert never (a and b);
 }
 
 vunit example1 {
   assert never (a && b);
 }
(i) VHDL flavor (ii) Verilog flavor
Fig. 1.1: The same vunit in two different flavors
  • The modeling layer provides a means to model behavior of design inputs, and to declare and give behavior to auxiliary signals and variables. This part of the modeling layer is simply a subset of the underlying flavor. For instance, the declaration of auxiliary signals in the Verilog flavor follows Verilog syntax.


2.1 Операторы always и never

Основные временные опреаторы always и never ранее уже встречались. Большенство PSL свойств будут начинаться с одного из этих операторов. Так как «голые» (булевы) свойства языка PSL относятся только к первому циклу временных диаграмм. Например, Утверждение 2.1а требует только того, чтобы булево выражение !(a && b) состоялось в первом цикле. Таким образом, Утверждение 2.1а имеет место на диаграмме 2.1(i) потому что булево выражение !(a && b) имеет место в цикле 0. Для того чтобы состояние, которое мы хотим его захватить в каждом цикле проета, то мы должны добавить временной оператор always как в Утверждении 2.1b. Утверждении 2.1b не происходит на диаграмме 2.1(i) потому что булево выражение !(a && b) не выполняется на 5м такте. Эквивалентным будет Утверждение 2.1c, если заменить оператор always на булево отрицание ! и оператор newer. 

assert !(a && b);                (2.1a)
assert always !(a && b);         (2.1b)
assert never (a && b);           (2.1c)

Рис. 2.1: Операторы always и never

Both Assertion 2.1b and Assertion 2.1c state that signals a and b are mutually exclusive. Obviously, anything that can be stated with the always operator can be stated with the never operator and vice versa, simply by negating the operand when switching between always and never. PSL pro- vides both operators for convenience, as sometimes it is more natural to state the property in the positive (that is, stating what must hold at all cycles) and sometimes in the negative (that is, what must not hold for any cycle). In general, there are many ways to state any property in PSL. We will see other examples throughout the rest of this book.

2.2 The next operator

Another temporal operator is the next operator. It indicates that the property will hold if its operand holds at the next cycle. For instance, Assertion 2.2a states that whenever a holds, then b should hold in the next cycle. Asser- tion 2.2a uses another important operator, the logical implication operator (->). While the logical implication operator is a Boolean and not a temporal operator (it does not link two sub-properties over time), it plays a very impor- tant role in many temporal properties. A logical implication prop1 -> prop2 holds if either prop1 does not hold or prop2 holds. A good way to think of it is like an if-then expression, with the else-part being implicitly true. That is, prop1 -> prop2 can be understood as “if prop1 then prop2 else true”. Thus, the sub-property a -> next b in our example holds if either a does not hold (because then the property defaults to true) or if a holds and also next b holds. By adding an always operator, we get a property that holds if the sub-property a -> next b holds at every cycle. Thus, Assertion 2.2a states that whenever a holds, b must hold at the next cycle. Assertion 2.2a holds on Trace 2.2(i) because every assertion of signal a is followed by an assertion of signal b. This is shown in the “if” and “then” annotations on Trace 2.2(ii). The “additional” assertions of signal b at cycles 1 and 10 are allowed by As- sertion 2.2a, because it says nothing about the value of b in cycles other than those following an assertion of a.

Note that the cycles involved in satisfying one assertion of signal a may overlap with those involved in satisfying another assertion. For example, con- sider Trace 2.2(iii), which is simply Trace 2.2(ii) with the if-then pairs num- bered. There are four assertions of signal a on Trace 2.2(iii), and thus four associated cycles in which b must be asserted. Each pair of cycles (an asser- tion of a followed by an assertion of b) is numbered in Trace 2.2(iii). Consider pairs 2 and 3. Signal a is asserted at cycle 4 in pair 2, thus signal b needs to be asserted at cycle 5 in order for Assertion 2.2a to hold. Signal a is asserted at cycle 5 in pair 3, thus requiring that signal b be asserted at cycle 6. Pairs 2 and 3 overlap, because while we are looking for an assertion of signal b at cycle 5 in order to satisfy the assertion of a at cycle 4, we see an additional assertion of signal a that must be considered.

Assertion 2.2a does not hold on Trace 2.2(iv) because the third assertion of signal a, at cycle 5, is missing an assertion of signal b at the following cycle.

2.3 Variations on next including next event

A next property holds if its operand holds in the next cycle. Variations on the next operator allow you to specify the nth next cycle, and ranges of future cycles. A next[n] property holds if its operand holds in the nth next cycle. For example, Assertion 2.3a states that whenever signal a holds, signal b holds three cycles later. Assertion 2.3a holds on Traces 2.3(i), 2.3(iii), and 2.3(iv), while it does not hold on Traces 2.3(ii) or 2.3(v) because of a missing assertion of signal b at cycle 7, and does not hold on Trace 2.3(vi) because of a missing assertion of signal b at cycle 5.

Agenda

  • Assertion Based Verification (ABV)
    • What is ABV?
    • Contrasting HDL, OVL and PSL assertions
  • PSL Basics
    • Language layers
    • VHDL and Verilog flavors
    • Structure & placement
    • Always and never
  • Boolean Layer
    • Boolean assertions
    • Boolean flavors
    • Clocked and unclocked properties
    • Default clocks
    • Conditional assertions
  • Foundation Language (FL)
    • Next cycle checks
    • FSM properties
    • Eventually
    • Until and before
    • Aborting properties
    • Cascading FL operators
  • Sequential Extended Regular Expressions (SERE’s)
    • SERE introduction
    • Conditional assertions
    • Sequence repetition
    • Aborting SERE’s
    • Named sequences
  • SERE Composition
    • Fusion & disjunction
    • Processor example
    • Sequence matching
    • Whilenot and within
  • Advanced PSL and the Verification Layer
    • Built-in functions
    • Parameterized constructs
    • Replicated properties
    • Verification units
    • Dealing with multiple clocks
  • Property Clocking
    • Correct time to clock properties
    • Multi-clocked properties
    • Counter-intuitive clock behavior
  • Coding Guidelines and Avoiding Common Problems
    • Abstraction levels
    • Over and under constrained assertions
    • Overlapping
    • Never failing constructs
    • Assertion refinement with arbiter case study
  • Coverage
    • What is coverage?
    • Structural and functional coverage examples
    • Coverage of the arbiter design
    • Coverage applications
  • Practical PSL Application
    • FIFO
    • Transaction-Based assertion modelling using AMBA
  • Introduction to Static Formal Verification
    • Static and dynamic verification
    • Model checking
    • Properties and constraints
  • Conclusions and Next Steps
  • Appendices

NEW

Источник — «http://www.simhard.com/wiki/index.php?title=PSL/Дневник&oldid=2681»