प्रॉपर्टी स्पेसिफिकेशन लैंग्वेज

गुणधर्म विशिष्टता लैंग्वेज (पीएसएल) अभिव्यक्ति की आसानी और अभिव्यंजक शक्ति में वृद्धि दोनों के लिए ऑपरेटरों की एक श्रृंखला के साथ रैखिक अस्थायी तर्क का विस्तार करने वाला एक अस्थायी तर्क होता है। पीएसएल नियमित अभिव्यक्ति और सिंटैक्टिक शुगरिंग का व्यापक उपयोग करता है। यह हार्डवेयर डिज़ाइन और सत्यापन उद्योग में व्यापक रूप से उपयोग किया जाता है, जहाँ औपचारिक सत्यापन उपकरण जैसे मॉडल जाँच और तर्क सिमुलेशन उपकरण का उपयोग यह साबित करने या खंडन करने के लिए किया जाता है कि एक दिया गया पीएसएल फॉर्मूला किसी दिए गए डिज़ाइन पर टिका है।

पीएसएल को प्रारंभ में एक्सेलेरा द्वारा हार्डवेयर डिजाइन के बारे में गुणों या अभिकथन (कंप्यूटिंग) को निर्दिष्ट करने के लिए विकसित किया गया था। सितंबर 2004 से आईईईई 1850 वर्किंग ग्रुप में लैंग्वेज का मानकीकरण किया गया है। सितंबर 2005 में, गुणधर्म विशिष्टता लैंग्वेज (पीएसएल ) के लिए आईईईई 1850 मानक की घोषणा की गई है।

सिंटेक्स और सिमेंटिक्स

पीएसएल कहता है कि यदि अभी कुछ परिदृश्य होता है, तो कुछ समय बाद दूसरा परिदृश्य होना चाहिए। उदाहरण के लिए गुणधर्म का अनुरोध सदैव अंत मेंदिया जाना चाहिए स्वीकृत को पीएसएल सूत्र द्वारा व्यक्त किया जाता है,

  always (request -> eventually! grant)

गुणधर्म प्रत्येक अनुरोध जिसके तुरंत बाद एसीके संकेत है, एक पूर्ण डेटा स्थानांतरण के बाद किया जाना चाहिए, जहां एक पूर्ण डेटा स्थानांतरण एक अनुक्रम के रूप में, जो सिग्नल प्रारंभ से शुरू होता है, सिग्नल अंत के साथ समाप्त होता है जिसमें इस बीच व्यस्त रहता है" पीएसएल सूत्र द्वारा व्यक्त किया जा सकता है

  (true[*]; req; ack)  |=> (start; busy[*]; end)

इस सूत्र को संतुष्ट करने वाला एक निशान दाईं ओर की आकृति में दिखाया गया है।

एक साहोल्ड ट्रेस संतोषजनक

(true[*]; req; ack)  |=> (start; busy[*]; end)

पीएसएल के अस्थायी ऑपरेटरों को मोटे तौर पर एलटीएल शैली ऑपरेटरों और नियमित अभिव्यक्ति शैली ऑपरेटरों में वर्गीकृत किया जा सकता है। कई पीएसएल ऑपरेटर दो संस्करणों में आते हैं एक विस्मयादिबोधक चिह्न प्रत्यय ( ! ) द्वारा इंगित एक मजबूत संस्करण और एक कमजोर संस्करण के रूप में होते है। मजबूत संस्करण संभावित आवश्यकताएँ बनाता है, अर्थात यह आवश्यक है कि भविष्य में कुछ होगा जबकि कमजोर संस्करण नहीं करता है। एक अंडरस्कोर प्रत्यय (_) का उपयोग समावेशी बनाम गैर-समावेशी आवश्यकताओं को अलग करने के लिए किया जाता है। _a और _e प्रत्यय का उपयोग सार्वभौमिक (सभी) बनाम अस्तित्वगत उपस्थित आवश्यकताओं को दर्शाने के लिए किया जाता है। सटीक समय विंडो को [n] और फ्लेक्सिबल को [m..n].से दर्शाया जाता है।

सेरे - स्टाइल ऑपरेटर्स

सबसे अधिक उपयोग किया जाने वाला पीएसएल ऑपरेटर प्रत्यय-निहितार्थ ऑपरेटर होता है, जिसे ट्रिगर ऑपरेटर के रूप में भी जाना जाता है, जिसे |=>.द्वारा दर्शाया जाता है। इसका बायाँ ऑपरेंड एक पीएसएल रेगुलर एक्सप्रेशन होता है और इसका राइट ऑपरेंड कोई भी पीएसएल फॉर्मूला होता है चाहे वह एलटीएल स्टाइल या रेगुलर एक्सप्रेशन स्टाइल में हो। का शब्दार्थ r |=> p का शब्दार्थ यह है कि प्रत्येक समय बिंदु पर i पर ऐसा है कि समय का क्रम i तक इंगित करता है जो नियमित अभिव्यक्ति r से मेल खाता है, i+1 से पथ गुणधर्म पी को संतुष्ट करना चाहिए। यह दाईं ओर के आंकड़ों में उदाहरण के रूप में है।

पथ संतोषजनक आर दो गैर-अतिव्यापी तरीकों से पी ट्रिगर करता है

पथ संतोषजनक r दो अतिव्यापी तरीकों से p को ट्रिगर करता है

पथ संतोषजनक r तीन तरह से p को ट्रिगर करता है

पीएसएल के रेगुलर एक्सप्रेशंस में संयोजन के लिए सामान्य ऑपरेटर हैं (;), क्लीने क्लोसर (*), और संघ (|), साथ ही फ्यूजन के लिए ऑपरेटर (:), प्रतिछेदन (&&) और कमजोर संस्करण (&) और निरंतर गिनती के लिए कई विविधताएं [*n] और निरंतर गिनती के रूप में एक उदाहरण इस प्रकार है [=n] और [->n].

ट्रिगर ऑपरेटर नीचे दी गई तालिका में दिखाए गए कई रूपों में आता है।

यहाँ s और t पीएसएल रेगुलर एक्सप्रेशन हैं और पी एक पीएसएल सूत्र के रूप में होता है।

s |=> t!	यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है। s समाप्त होने के बाद t चक्र शुरू करता है। टी का मैच अपने अंत तक पहुंचना चाहिए।
s |-> t!	यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है। t उसी चक्र को प्रारंभ करता है जो s समाप्त होता है। टी का मैच अपने अंत तक पहुंचना चाहिए।
s |=> t	यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है। s समाप्त होने के बाद t चक्र शुरू करता है। टी का मैच बीच में "अटक" सकता है।
s |-> t	यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है। t उसी चक्र को प्रारंभ करता है जो s समाप्त होता है। टी का मैच बीच में "अटक" सकता है।

संयोजन, संलयन, संघ, प्रतिच्छेदन और उनकी विविधताओं के लिए ऑपरेटर नीचे दी गई तालिका में दिखाए गए हैं।

यहाँ s और t पीएसएल रेगुलर एक्सप्रेशन के रूप में हैं।

s ; t	s के मिलान के बाद t का मिलान, s समाप्त होने के बाद t चक्र शुरू करता है
s : t	s के मैच के बाद t का मैच, t उसी चक्र को शुरू करता है जो s समाप्त होता है
s | t	एस का मैच या टी का मैच है
s && t	एस का मैच और टी का मैच, दोनों की अवधि समान लंबाई की है
s & t	एस का मैच और टी का मैच, अवधि मैच शायद अलग होते है
s within t	टी के मैच के भीतर एस का मैच, ([*]; s; [*]) && t का संक्षिप्त नाम है

नीचे दी गई तालिका में निरंतर दोहराव के लिए ऑपरेटरों को दिखाया गया है।

यहाँ s एक पीएसएल रेगुलर एक्सप्रेशन के रूप में है।

s[*i]	आई एस की लगातार पुनरावृत्ति है
s[*i..j]	i से j के बीच s का लगातार दोहराव है
s[*i..]	कम से कम आईएस की लगातार पुनरावृत्ति होती है
s[*]	एस के शून्य या अधिक लगातार दोहराव के रूप में है
s[+]	एस के एक या अधिक लगातार दोहराव होता है

नीचे दी गई तालिका में गैर-निरंतर दोहराव के लिए ऑपरेटरों को दिखाया गया है।

यहाँ b कोई भी पीएसएल बूलियन व्यंजक है।

b[=i]	आई जरूरी नहीं कि बी की लगातार पुनरावृत्ति हो के बराबर (!b[*];b)[*i]; !b[*] है
b[=i..j]	कम से कम i और j से अधिक नहीं जरूरी नहीं कि लगातार b की पुनरावृत्ति हो, equivalent to (!b[*];b)[*i..j]; !b[*] है
b[=i..]	कम से कम मैं जरूरी नहीं कि बी की लगातार पुनरावृत्ति हो के बराबर (!b[*];b)[*i..]; !b[*] है
b[->m]	एम आवश्यक रूप से बी के साथ समाप्त होने वाले बी की लगातार पुनरावृत्ति नहीं है, के बराबर (!b[*];b)[*m] है
b[->m:n]	कम से कम m और n से अधिक नहीं आवश्यक रूप से b के साथ समाप्त होने वाले b का लगातार दोहराव नहीं है, के बराबर (!b[*];b)[*m..n] है
b[->m..]	कम से कम m अनिवार्य रूप से b के साथ समाप्त होने वाले b की लगातार पुनरावृत्ति नहीं है, के बराबर (!b[*];b)[*m..]; !b[*] है
b[->]	शॉर्टकट के लिए b[->1], है के बराबर (!b[*];b) है

एलटीएल-शैली ऑपरेटर

नीचे पीएसएल के कुछ एलटीएल-शैली के ऑपरेटरों का एक नमूना है।

यहाँ p और q कोई भी पीएसएल सूत्र हैं।

always p	गुणधर्म पी प्रत्येक समय बिंदु पर पकड़ बनाये रखती है
never p	गुणधर्म पी किसी भी समय बिंदु पर पकड़ नहीं बनाती है
eventually! p	वहाँ एक भविष्य समय बिंदु मौजूद है जहाँ p होल्ड करता है
next! p	वहाँ एक अगली बार बिंदु उपस्थित है और p इस बिंदु पर कायम है
next p	यदि कोई अगली बार बिंदु उपस्थित है, तो p इस बिंदु पर रहता है
next![n] p	एक n-वाँ समय बिंदु उपस्थित है और p इस बिंदु पर कायम है
next[n] p	यदि कोई n-वाँ समय बिंदु उपस्थित है, तो p इस बिंदु पर रहता है
next_e![m..n] p	जहां पी होल्ड करता है, वहां से एम-वें से एन-वें के भीतर एक समय बिंदु उपस्थित है।
next_e[m..n] p	यदि कम से कम n-वें समय बिंदु उपस्थित हैं, तो p m-वें से n-वें बिंदुओं में से एक पर रहता है।
next_a![m..n] p	m-वें से n-वें सहित, सभी समय बिंदुओं में कम से कम n और समय बिंदु मौजूद हैं और p होल्ड करता है।
next_a[m..n] p	पी अगले सभी एम-वें से एन-वें समय बिंदुओं पर कायम रहता है, चूँकि कई उपस्थित हैं
p until! q	वहाँ एक समय बिंदु मौजूद है जहाँ q होल्ड करता है और p उस समय बिंदु तक रुकता है
p until q	p उस समय बिंदु तक टिका रहता है जहाँ q होल्ड करता है, यदि ऐसा उपस्थित है
p until!_ q	वहाँ एक समय बिंदु उपस्थित है जहाँ q होल्ड करता है, और p उस समय बिंदु तक और उस समय बिंदु तक बना रहता है
p until_ q	p उस समय बिंदु तक रुकता है जहाँ q होल्ड करता है, और उस समय बिंदु में, यदि ऐसा उपस्थित है
p before! q	p उस समय बिंदु से पहले सख्ती से पकड़ रखता है जहाँ q होल्ड करता है, और p अंततः होल्ड करता है
p before q	p सख्ती से उस समय बिंदु से पहले रखता है जहाँ q होल्ड करता है, यदि p कभी भी होल्ड नहीं करता है, तो q भी नहीं करता है
p before!_ q	p पहले या उसी समय बिंदु पर रखता है जहाँ q होल्ड करता है, और p अंततः होल्ड करता है
p before_ q	p पहले या उसी समय बिंदु पर रखता है जहाँ q होल्ड करता है, यदि p होल्ड नहीं करता है, तो q भी होल्ड नही करता है

सैंपलिंग ऑपरेटर

कभी-कभी अगली बार-बिंदु की परिलैंग्वेज को बदलना वांछनीय होता है, उदाहरण के लिए बहु-घड़ी वाली डिज़ाइनों में या जब उच्च स्तर की अमूर्तता वांछित होती है। सैंपलिंग ऑपरेटर जिसे क्लॉक ऑपरेटर के रूप में भी जाना जाता है, जिसका अर्थ @, इस प्रयोजन के लिए प्रयोग किया जाता है। सूत्र p @ c जहां पी एक पीएसएल फॉर्मूला है और c एक पीएसएल बूलियन एक्सप्रेशंस दिए गए पथ पर होल्ड करता है यदि p उस पथ पर उन चक्रों पर प्रक्षेपित होता है जिसमें c दाईं ओर के आंकड़ों में उदाहरण के रूप में होता है।

पथ और सूत्र एक नमूनाकरण ऑपरेटर की आवश्यकता दिखा रहा है

पहली गुणधर्म बताती है कि हर अनुरोध एसीके संकेत, के तुरंत बाद आने वाले प्रत्येक अनुरोध को एक पूर्ण डेटा ट्रांसफर के बाद किया जाना चाहिए, जहां एक पूर्ण डेटा स्थानांतरण सिग्नल से प्रारंभ होने वाला अनुक्रम है जो सिग्नल के अंत से शुरू होता है जिसमें डेटा कम से कम 8 बार होना चाहिए

  (true[*]; req; ack)  |=> (start; data[=8]; end)

लेकिन कभी-कभी केवल उन स्थितियों पर विचार करना वांछित होता है, जहां उपरोक्त संकेत एक चक्र पर होते हैं जहां सीएलक उच्च है। इसे दूसरे अंक में दर्शाया गया है, यद्यपि यह सूत्र में दर्शाया गया है।

  ((true[*]; req; ack)  |=> (start; data[*3]; end)) @ clk

डेटा का उपयोग करता है [*3] और [*n] निरंतर दोहराव होता है, मिलान ट्रेस में 3 गैर-लगातार समय बिंदु होते हैं जहां डेटा होल्ड होता है, लेकिन जब केवल उन समय बिंदुओं पर विचार किया जाता है, तो समय बिंदु जहां डेटा होल्ड लगातार होता है।

सैंपलिंग ऑपरेटर @ का प्रभाव दिखाने वाला पथ और सूत्र

नेस्टेड @ वाले सूत्रों का शब्दार्थ थोड़ा सूक्ष्म है। इच्छुक पाठक [2] को संदर्भित करता है।

ऑपरेटरों को छोड़ें

पीएसएल के पास काटे गए रास्तों से निपटने के लिए कई ऑपरेटर हैं, परिमित पथ जो संगणना के एक उपसर्ग के अनुरूप हो सकते हैं। काटे गए पथ रीसेट और कई अन्य परिदृश्यों के कारण बाउंडेड-मॉडल जाँच में होते हैं। एबॉर्ट ऑपरेटर निर्दिष्ट करते हैं कि किसी पथ को छोटा किए जाने पर संभावित घटनाओं से कैसे निपटा जाए। वे [1] में प्रस्तावित संक्षिप्त शब्दार्थ पर भरोसा करते हैं।

यहाँ p कोई पीएसएल फॉर्मूला है और b कोई भी पीएसएल बूलियन व्यंजक के रूप में होता है।

p async_abort b	या तो p धारण करता है या p तब तक विफल नहीं होता जब तक b धारण नहीं करता है। b अतुल्यकालिक रूप से पहचाना गया है।
p sync_abort b	या तो p धारण करता है या p तब तक विफल नहीं होता जब तक b धारण नहीं करता है। b समकालिक रूप से पहचाना गया है।
p abort b	पी के बराबर async_abort b है।

अभिव्यंजक शक्ति

पीएसएल लौकिक तर्क एलटीएल को समाहित करता है और इसकी अभिव्यंजक शक्ति को ओमेगा नियमित लैंग्वेजो तक बढ़ाता है। एलटीएल की तुलना में अभिव्यंजक शक्ति में वृद्धि, जिसमें स्टार मुक्त ω की अभिव्यंजक शक्ति होती है, नियमित अभिव्यक्तियों को प्रत्यय निहितार्थ के लिए जिम्मेदार ठहराया जा सकता है, जिसे ट्रिगर्स ऑपरेटर के रूप में भी जाना जाता है जिसे "|->" दर्शाया गया है। सूत्र r |-> f जहां r एक रेगुलर एक्सप्रेशन के रूप में होते है और f एक टेम्पोरल लॉजिक फॉर्मूला होता है जो गणना w पर टिका रहता है यदि w मैचिंग r के किसी भी उपसर्ग में निरंतर संतोषजनक f होता है। पीएसएल के अन्य गैर एलटीएल ऑपरेटर मल्टीपल क्लॉक्ड डिजाइनों को निर्दिष्ट करने के लिए @ ऑपरेटरहोते है, संक्षिप्तता के लिए हार्डवेयर रीसेट और स्थानीय चर से निपटने के लिए स्थानीय चर होते है।

परतें

पीएसएल को 4 परतों में परिभाषित किया गया है, बूलियन परत, टेम्पोरल परत, मॉडलिंग परत और सत्यापन परत के रूप में होते है।

• बूलियन परत का उपयोग डिजाइन की वर्तमान स्थिति का वर्णन करने के लिए किया जाता है और उपर्युक्त एचडीएल में से किसी एक का उपयोग करके इसका वर्णन किया जाता है।
• टेम्पोरल लेयर में टेम्पोरल ऑपरेटर्स होते हैं जिनका उपयोग उन परिदृश्यों का वर्णन करने के लिए किया जाता है जो समय के साथ विस्तारित होते हैं, संभवतः समय इकाइयों की असीमित संख्या में होते है।
• मॉडलिंग परत का उपयोग प्रक्रियात्मक विधियों से सहायक राज्य मशीनों का वर्णन करने के लिए किया जाता है।
• सत्यापन परत में एक सत्यापन उपकरण के लिए निर्देश होते हैं, उदाहरण के लिए यह प्रमाणित करने के लिए कि दी गई गुणधर्म सही है यह मानने के लिए कि गुणों का एक निश्चित सेट गुणों के दूसरे सेट की पुष्टि करते समय सही है।

लैंग्वेज अनुकूलता

गुणधर्म विशिष्टता लैंग्वेज का उपयोग कई इलेक्ट्रॉनिक प्रणाली डिज़ाइन लैंग्वेजो (एचडीएल) के साथ किया जा सकता है जैसे

• वीएचडीएल (आईईईई 1076)
• Verilog (आईईईई 1364)
• प्रणाली वेरिलॉग (आईईईई 1800)
• सिस्टमसी (आईईईई 1666) ओपन सिस्टमसी इनिशिएटिव ओएससीआई द्वारा।

जब पीएसएल का उपयोग उपरोक्त एचडीएल में से किसी एक के साथ किया जाता है, तो इसकी बूलियन परत संबंधित एचडीएल के ऑपरेटरों का उपयोग करती है।

संदर्भ

• 1850-2005 – IEEE Standard for Property Specification Language (PSL). 2005. doi:10.1109/IEEESTD.2005.97780. ISBN 0-7381-4780-X.
  • IEC 62531:2007 62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL). 2007. doi:10.1109/IEEESTD.2007.4408637. ISBN 978-0-7381-5727-6.
• 1850-2010 – IEEE Standard for Property Specification Language (PSL). 2010. doi:10.1109/IEEESTD.2010.5446004. ISBN 978-0-7381-6255-3.
  • IEC 62531:2012 62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL). 2012. doi:10.1109/IEEESTD.2012.6228486. ISBN 978-0-7381-7299-6.
• Eisner, Cindy; Fisman, Dana; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). "Reasoning with Temporal Logic on Truncated Paths" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2725. p. 27. doi:10.1007/978-3-540-45069-6_3. ISBN 978-3-540-40524-5.
• Eisner, Cindy; Fisman, Dana; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). "The Definition of a Temporal Clock Operator" (PDF). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 2719. p. 857. doi:10.1007/3-540-45061-0_67. ISBN 978-3-540-40493-4.

बाहरी संबंध

• आईईईई 1850 working group
• आईईईई Announcement September 2005
• Accellera
• Property Specification Language Tutorial
• Designers guide to पीएसएल

पीएसएल पर किताबें

• यूजिंग पीएसएल/शुगर फॉर फॉर्मल एंड डायनामिक वेरिफिकेशन 2रा संस्करण, बेन कोहेन, अजीता कुमारी, श्रीनिवासन वेंकटरमनन
• पीएसएल का व्यावहारिक परिचय, सिंडी आइजनर, डाना फिशमैन

श्रेणी:हार्डवेयर सत्यापन भाषाएं श्रेणी:औपचारिक विनिर्देश भाषाएँ श्रेणी:आईईईई DASC मानक श्रेणी:आईईसी मानक