Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Мазмұны
Кіріспе
Property Specification Language (PSL) – өрнектің айқындығын арттыру және оны оңай түсіндіру үшін операторлар жиынымен сызықтық уақыт логикасын кеңейтетін уақытша логика. PSL реттегіш өрнектерді және синтаксистік жеңілдетулерді кеңінен пайдаланады. Ол аппараттық құрылымдау және тексеру саласында кеңінен қолданылады, онда формальды тексеру құралдары (мысалы, модельді тексеру) және/немесе логикалық симуляция құралдары берілген PSL формуласының белгілі бір құрылымға сәйкес екенін немесе одан өзгеше екенін дәлелдеу үшін қолданылады. PSL бастапқыда Accellera компаниясымен аппараттық дизайн қасиеттерін немесе талаптарын көрсету үшін әзірленді. 2004 жылдың қыркүйегінен бастап тілді стандарттау IEEE 1850 жұмыс тобында жүзеге асырылды. 2005 жылдың қыркүйегінде Property Specification Language (PSL) стандарты IEEE 1850 ретінде жарияланды.
Property Specification Language (PSL) is a temporal logic extending linear temporal logic with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of regular expressions and syntactic sugaring. It is widely used in the hardware design and verification industry, where formal verification tools (such as model checking) and/or logic simulation tools are used to prove or refute that a given PSL formula holds on a given design. 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.
LTL үлгісіндегі операторлар
Төменде PSL-дің кейбір LTL стильді операторларының үлгісі келтірілген. Мұнда және кез келген PSL формулалары. p қасиеті әр уақыт нүктесінде орындалады. p қасиеті ешқандай уақыт нүктесінде орындалмайды. p қасиеті болашақтағы бір уақыт нүктесінде орындалады. p қасиеті келесі уақыт нүктесінде орындалады. Егер келесі уақыт нүктесі болса, онда p қасиеті осы нүктеде орындалады. p қасиеті n-ші уақыт нүктесінде орындалады. Егер n-ші уақыт нүктесі болса, онда p қасиеті осы нүктеде орындалады. p қасиеті ағымдағы уақыттан m-ден n-ге дейінгі аралықтағы бір уақыт нүктесінде орындалады. Егер кем дегенде n уақыт нүктесі болса, онда p қасиеті m-ден n-ге дейінгі нүктелердің бірінде орындалады. Кем дегенде n уақыт нүктесі бар және p қасиеті m-ден n-ге дейінгі барлық уақыт нүктелерінде, оның ішінде орындалады. p қасиеті келесі m-ден n-ге дейінгі барлық уақыт нүктелерінде орындалады, қанша болса да. p қасиеті q орындалатын уақытқа дейін орындалады. p қасиеті q орындалатын уақытқа дейін орындалады, егер мұндай уақыт болса. p қасиеті q орындалатын уақытқа дейін орындалады, және сол уақытта да орындалады. p қасиеті q орындалатын уақытқа дейін орындалады, және сол уақытта, егер мұндай уақыт болса. p қасиеті q орындалатын уақыттан бұрын орындалады, және p қасиеті әрі қарай орындалады. p қасиеті q орындалатын уақыттан бұрын орындалады, егер p қасиеті ешқашан орындалмаса, онда q да орындалмайды. p қасиеті q орындалатын уақыттан бұрын немесе сол уақытта орындалады, және p қасиеті әрі қарай орындалады. p қасиеті q орындалатын уақыттан бұрын немесе сол уақытта орындалады, егер p қасиеті ешқашан орындалмаса, онда q да орындалмайды.
Below is a sample of some LTL style operators of PSL. Here and are any PSL formulas. property p holds on every time point property p does not hold on any time point there exists a future time point where p holds there exists a next time point, and p holds on this point if there exists a next time point, then p holds on this point there exists an n th time point, and p holds on this point if there exists an n th time point, then p holds on this point there exists a time point, within m th to n th from the current where p holds. if there exists at least n th time points, then p holds on one of the m th to n th points. there exists at least n more time points and p holds in all the time points between the m th to the n th, inclusive. p holds on all the next m th through n th time points, however many exist there exists a time point where q holds, and p hold up until that time point p holds up until a time point where q hold, if such exists there exists a time point where q holds, and p holds up until that time point and in that time point p holds up until a time point where q holds, and in that time point, if such exists p holds strictly before the time point where q holds, and p eventually holds p holds strictly before the time point where q holds, if p never holds, then neither does q p holds before or at the same time point where q holds, and p eventually holds p holds before or at the same time point where q holds, if p never holds, then neither does q
Экспрессивтік күш
PSL LTL уақытша логикасын қамтиды және оның экспрессивті күшін омега реттелген тілдеріне дейін кеңейтеді. LTL-мен салыстырғанда, экспрессивті күштің артуы, LTL жұлдызсыз ω реттелген өрнектерінің экспрессивті күшіне ие болса, жұрнақ импликациясына байланысты, ол триггер операторы деп те белгілі. r |> f формуласы, мұндағы r – реттелген өрнек және f – уақытша логикалық формула, егер w есептеуінің кез келген r префиксі f-ді қанағаттандыратын жалғасы болса, онда орындалады. PSL-дің LTL емес операторларына @ операторы (көп сағатталған жүйелерді көрсету үшін), аппараттық қайта орналастыруларды басқару үшін тоқтату операторлары және ықшамдық үшін жергілікті айнымалылар жатады.
PSL subsumes the temporal logic LTL and extends its expressive power to that of 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 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 4 қабатта анықталады: Бульдік қабат, уақыт қабаты, модельдеу қабаты және тексеру қабаты. Бульдік қабат жобаның ағымдағы күйін сипаттау үшін қолданылады және жоғарыда аталған HDL-дердің бірін пайдаланып өрнектеледі. Уақыт қабаты уақыт бойынша (мүмкін, шексіз уақыт бірліктері бойы) созылатын сценарийлерді сипаттау үшін қолданылатын уақыт операторларынан тұрады. Модельдеу қабаты көмекші күй машиналарын процедуралық тәсілмен сипаттауға мүмкіндік береді. Тексеру қабаты тексеру құралына берілетін директивалардан тұрады (мысалы, белгілі бір қасиеттің дұрыс екенін растау немесе басқа қасиеттерді тексеру кезінде қасиеттердің белгілі бір жиынтығының дұрыс екенін жорамалдау).
PSL is defined in 4 layers: the Boolean layer, the temporal layer, the modeling layer and the verification layer. The Boolean layer is used for describing a current state of the design and is phrased using one of the above mentioned HDLs. The temporal layer consists of the temporal operators used to describe scenarios that span over time (possibly over an unbounded number of time units). The modeling layer can be used to describe auxiliary state machines in a procedural manner. The verification layer consists of directives to a verification tool (for instance to assert that a given property is correct or to assume that a certain set of properties is correct when verifying another set of properties).