Misplaced Pages

#24975

32-533: PSL was initially developed by Accellera for specifying properties or assertions about hardware designs. Since September 2004 the standardization on the language has been done in IEEE 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced. PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance,

64-453: A weak until binary operator, denoted W , with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release). It is sometimes useful since both U and R can be defined in terms of the weak until: The strong release binary operator, denoted M , is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it

96-400: A complete data transfer is a sequence starting with signal start , ending with signal end in which data should hold at least 8 times: But sometimes it is desired to consider only the cases where the above signals occur on a cycle where clk is high. This is depicted in the second figure in which although the formula uses data[*3] and [*n] is consecutive repetition,

128-521: A continuation satisfying f . Other non-LTL operators of PSL are the @ operator, for specifying multiply-clocked designs, the abort operators, for dealing with hardware resets, and local variables for succinctness. PSL is defined in 4 layers: the Boolean layer , the temporal layer , the modeling layer and the verification layer . Property Specification Language can be used with multiple electronic system design languages (HDLs) such as: When PSL

160-597: A merger was announced between Accellera and The SPIRIT Consortium , another major EDA standards organization focused on IP deployment and reuse. The SPIRIT Consortium obtained SystemRDL from the SystemRDL Alliance and then developed IP-XACT . The merger was completed in April 2010. SPIRIT stood for "Structure for Packaging, Integrating and Re-using IP within Tool-flows". In December 2011, Accellera and

192-429: A word on a path of a Kripke structure (an ω-word over alphabet 2 ). Let w = a 0 ,a 1 ,a 2 ,... be such an ω-word. Let w ( i ) = a i . Let w = a i , a i +1 ,..., which is a suffix of w . Formally, the satisfaction relation ⊨ between a word and an LTL formula is defined as follows: We say an ω-word w satisfies an LTL formula ψ when w ⊨ ψ . The ω-language L ( ψ ) defined by ψ

224-474: Is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths , e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL* , which additionally allows branching time and quantifiers . LTL is sometimes called propositional temporal logic , abbreviated PTL . In terms of expressive power , linear temporal logic (LTL)

256-415: Is a fragment of first-order logic . LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977. LTL is built up from a finite set of propositional variables AP , the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N ) and U . Formally, the set of LTL formulas over AP is inductively defined as follows: X

288-451: Is exemplified in the figures on the right. The regular expressions of PSL have the common operators for concatenation ( ; ), Kleene-closure ( * ), and union ( | ), as well as operator for fusion ( : ), intersection ( && ) and a weaker version ( & ), and many variations for consecutive counting [*n] and in-consecutive counting e.g. [=n] and [->n] . The trigger operator comes in several variations, shown in

320-527: Is read as ne x t and U is read as u ntil. Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators, in order to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔, true , and false . Following are the additional temporal operators. An LTL formula can be satisfied by an infinite sequence of truth valuations of variables in AP . These sequences can be viewed as

352-407: Is stronger than the release operator. The semantics for the temporal operators are pictorially presented as follows. [REDACTED] [REDACTED] Let φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences that extend standard equivalences among the usual logical operators. All the formulas of LTL can be transformed into negation normal form , where Using

SECTION 10

#1732780891025

384-417: Is used for this purpose. The formula p @ c where p is a PSL formula and c a PSL Boolean expressions holds on a given path if p on that path projected on the cycles in which c holds, as exemplified in the figures to the right. The first property states that "every request that is immediately followed by an ack signal, should be followed by a complete data transfer , where

416-422: Is used in conjunction with one of the above HDLs, its Boolean layer uses the operators of the respective HDL. Accellera Accellera Systems Initiative (Accellera) is a standards organization that supports a mix of user and vendor standards and open interfaces development in the area of electronic design automation (EDA) and integrated circuit (IC) design and manufacturing. It is less constrained than

448-410: Is { w | w ⊨ ψ }, which is the set of ω-words that satisfy ψ . A formula ψ is satisfiable if there exist an ω-word w such that w ⊨ ψ . A formula ψ is valid if for each ω-word w over alphabet 2 , we have w ⊨ ψ . The additional logical operators are defined as follows: The additional temporal operators R , F , and G are defined as follows: Some authors also define

480-514: The Institute of Electrical and Electronics Engineers (IEEE) and is therefore the starting place for many standards. Once mature and adopted by the broader community, the standards are usually transferred to the IEEE. In 2000, Accellera was founded from the merger of Open Verilog International (OVI) and VHDL International , the developers of Verilog and VHDL respectively. Both were originally formed nine years earlier in 1991. In June 2009,

512-452: The monadic first-order logic of order , FO[<]—a result known as Kamp's theorem — or equivalently to star-free languages . Computation tree logic (CTL) and linear temporal logic (LTL) are both a subset of CTL* , but are incomparable. For example, Model checking and satisfiability against an LTL formula are PSPACE-complete problems. LTL synthesis and the problem of verification of games against an LTL winning condition

544-429: The omega-regular languages . The augmentation in expressive power, compared to that of LTL, which has the expressive power of the star-free ω-regular expressions, can be attributed to the suffix implication , also known as the triggers operator, denoted "|->". The formula r |-> f where r is a regular expression and f is a temporal logic formula holds on a computation w if any prefix of w matching r has

576-453: The "triggers" operator), which is denoted by |=> . Its left operand is a PSL regular expression and its right operand is any PSL formula (be it in LTL style or regular expression style). The semantics of r |=> p is that on every time point i such that the sequence of time points up to i constitute a match to the regular expression r, the path from i+1 should satisfy the property p. This

608-565: The OCP-IP solution. Corporate members have a right to be eligible for election to the Board of Directors. Associate member companies have voting rights in all of Accellera's Technical Working Groups. The following EDA standards developed by Accellera were ratified by IEEE by 2019: The following EDA initiatives were developed by Accellera: Linear temporal logic In logic , linear temporal logic or linear-time temporal logic ( LTL )

640-670: The Open SystemC Initiative (OSCI) approved their merger, adopting the name Accellera Systems Initiative (Accellera) while continuing to develop SystemC . In October 2013, Accellera acquired the Open Core Protocol (OCP) standard, the intellectual property of the OCP International Partnership (OCP-IP). The SPIRIT Consortium was a group of vendors and users of electronic design automation (EDA) tools, defining standards for

672-483: The PSL formula: A trace satisfying this formula is given in the figure on the right. PSL's temporal operators can be roughly classified into LTL-style operators and regular-expression-style operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix ( ! ), and a weak version. The strong version makes eventuality requirements (i.e. require that something will hold in

SECTION 20

#1732780891025

704-509: The SPIRIT consortium. The Board of Directors (BoD) was the ruling body. Members around the time of the merge were: Contributing members performed the standardization work and donate time and effort to the production of new specifications. Reviewing member status was a free membership for companies. These get early access to specifications to facilitate a deep review round of each proposal before it goes public. Associate member status

736-438: The above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows R , true , false , and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the length of the formula. This normal form is useful in translation from an LTL formula to a Büchi automaton . LTL can be shown to be equivalent to

768-421: The computation). Truncated paths occur in bounded-model checking, due to resets and in many other scenarios. The abort operators, specify how eventualities should be dealt with when a path has been truncated. They rely on the truncated semantics proposed in [1]. Here p is any PSL formula and b is any PSL Boolean expression. PSL subsumes the temporal logic LTL and extends its expressive power to that of

800-446: The exchange of System-on-a-chip (SoC) design information. The standards defined included IP-XACT , an XML schema for vendor-neutral descriptions of design components, and SystemRDL , a language for describing registers in components. SPIRIT stood for "Structure for Packaging, Integrating and Re-using IP within Tool-flows". In June 2009 it was announced that SPIRIT would merge with Accellera. There were four levels of membership in

832-422: The future), while the weak version does not. An underscore suffix ( _ ) is used to differentiate inclusive vs. non-inclusive requirements. The _a and _e suffixes are used to denote universal (all) vs. existential (exists) requirements. Exact time windows are denoted by [n] and flexible by [m..n] . The most commonly used PSL operator is the "suffix-implication" operator (also known as

864-404: The matching trace has 3 non-consecutive time points where data holds, but when considering only the time points where clk holds, the time points where data hold become consecutive. The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2]. PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of

896-411: The property "a request should always eventually be grant ed" can be expressed by the PSL formula: The property "every request that is immediately followed by an ack signal, should be followed by a complete data transfer , where a complete data transfer is a sequence starting with signal start , ending with signal end in which busy holds at the meantime" can be expressed by

928-411: The table below. Here b is any PSL Boolean expression. Below is a sample of some LTL-style operators of PSL. Here p and q are any PSL formulas. Sometimes it is desirable to change the definition of the next time-point , for instance in multiply-clocked designs, or when a higher level of abstraction is desired. The sampling operator (also known as the clock operator ), denoted @ ,

960-428: The table below. Here s and t are PSL-regular expressions, and p is a PSL formula. Operators for concatenation, fusion, union, intersection and their variations are shown in the table below. Here s and t are PSL regular expressions. Operators for consecutive repetitions are shown in the table below. Here s is a PSL regular expression. Operators for non-consecutive repetitions are shown in

992-496: Was similar to a reviewing membership but for academics and other not-for-profit organizations. The Open Core Protocol International Partnership Association, Inc. ( OCP-IP ) was an independent, non-profit semiconductor industry consortium formed to administer the support, promotion and enhancement of the Open Core Protocol (OCP). OCP was the first fully supported, openly licensed, comprehensive, interface socket for semiconductor intellectual property (IP) cores. The mission of OCP-IP

Property Specification Language - Misplaced Pages Continue

1024-504: Was to address problems relating to design, verification, and testing which are common to IP core reuse in " plug and play " system on a chip (SoC) products. This initiative comprehensively fulfills system-level integration requirements by promoting IP core reusability and reducing design time, risk and manufacturing costs for SoC designs. Design teams developing consumer, data processing , telecom (wireless or wired), datacom and mass storage applications can gain significant benefits from

#24975