प्रॉपर्टी स्पेसिफिकेशन लैंग्वेज
गुणधर्म विशिष्टता लैंग्वेज (पीएसएल) अभिव्यक्ति की आसानी और अभिव्यंजक शक्ति में वृद्धि दोनों के लिए ऑपरेटरों की एक श्रृंखला के साथ रैखिक अस्थायी तर्क का विस्तार करने वाला एक अस्थायी तर्क होता है। पीएसएल नियमित अभिव्यक्ति और सिंटैक्टिक शुगरिंग का व्यापक उपयोग करता है। यह हार्डवेयर डिज़ाइन और सत्यापन उद्योग में व्यापक रूप से उपयोग किया जाता है, जहाँ औपचारिक सत्यापन उपकरण जैसे मॉडल जाँच और तर्क सिमुलेशन उपकरण का उपयोग यह साबित करने या खंडन करने के लिए किया जाता है कि एक दिया गया पीएसएल फॉर्मूला किसी दिए गए डिज़ाइन पर टिका है।
पीएसएल को प्रारंभ में एक्सेलेरा द्वारा हार्डवेयर डिजाइन के बारे में गुणों या अभिकथन (कंप्यूटिंग) को निर्दिष्ट करने के लिए विकसित किया गया था। सितंबर 2004 से आईईईई 1850 वर्किंग ग्रुप में लैंग्वेज का मानकीकरण किया गया है। सितंबर 2005 में, गुणधर्म विशिष्टता लैंग्वेज (पीएसएल ) के लिए आईईईई 1850 मानक की घोषणा की गई है।
सिंटेक्स और सिमेंटिक्स
पीएसएल कहता है कि यदि अभी कुछ परिदृश्य होता है, तो कुछ समय बाद दूसरा परिदृश्य होना चाहिए। उदाहरण के लिए गुणधर्म का अनुरोध सदैव अंत मेंदिया जाना चाहिए स्वीकृत को पीएसएल सूत्र द्वारा व्यक्त किया जाता है,
always (request -> eventually! grant)
गुणधर्म प्रत्येक अनुरोध जिसके तुरंत बाद एसीके संकेत है, एक पूर्ण डेटा स्थानांतरण के बाद किया जाना चाहिए, जहां एक पूर्ण डेटा स्थानांतरण एक अनुक्रम के रूप में, जो सिग्नल प्रारंभ से शुरू होता है, सिग्नल अंत के साथ समाप्त होता है जिसमें इस बीच व्यस्त रहता है" पीएसएल सूत्र द्वारा व्यक्त किया जा सकता है
(true[*]; req; ack) |=> (start; busy[*]; end)
इस सूत्र को संतुष्ट करने वाला एक निशान दाईं ओर की आकृति में दिखाया गया है।
पीएसएल के अस्थायी ऑपरेटरों को मोटे तौर पर एलटीएल शैली ऑपरेटरों और नियमित अभिव्यक्ति शैली ऑपरेटरों में वर्गीकृत किया जा सकता है। कई पीएसएल ऑपरेटर दो संस्करणों में आते हैं एक विस्मयादिबोधक चिह्न प्रत्यय ( ! ) द्वारा इंगित एक मजबूत संस्करण और एक कमजोर संस्करण के रूप में होते है। मजबूत संस्करण संभावित आवश्यकताएँ बनाता है, अर्थात यह आवश्यक है कि भविष्य में कुछ होगा जबकि कमजोर संस्करण नहीं करता है। एक अंडरस्कोर प्रत्यय (_) का उपयोग समावेशी बनाम गैर-समावेशी आवश्यकताओं को अलग करने के लिए किया जाता है। _a और _e प्रत्यय का उपयोग सार्वभौमिक (सभी) बनाम अस्तित्वगत उपस्थित आवश्यकताओं को दर्शाने के लिए किया जाता है। सटीक समय विंडो को [n] और फ्लेक्सिबल को [m..n].से दर्शाया जाता है।
सेरे - स्टाइल ऑपरेटर्स
सबसे अधिक उपयोग किया जाने वाला पीएसएल ऑपरेटर प्रत्यय-निहितार्थ ऑपरेटर होता है, जिसे ट्रिगर ऑपरेटर के रूप में भी जाना जाता है, जिसे |=>.द्वारा दर्शाया जाता है। इसका बायाँ ऑपरेंड एक पीएसएल रेगुलर एक्सप्रेशन होता है और इसका राइट ऑपरेंड कोई भी पीएसएल फॉर्मूला होता है चाहे वह एलटीएल स्टाइल या रेगुलर एक्सप्रेशन स्टाइल में हो। का शब्दार्थ r |=> p का शब्दार्थ यह है कि प्रत्येक समय बिंदु पर i पर ऐसा है कि समय का क्रम i तक इंगित करता है जो नियमित अभिव्यक्ति r से मेल खाता है, i+1 से पथ गुणधर्म पी को संतुष्ट करना चाहिए। यह दाईं ओर के आंकड़ों में उदाहरण के रूप में है।
पीएसएल के रेगुलर एक्सप्रेशंस में संयोजन के लिए सामान्य ऑपरेटर हैं (;), क्लीने क्लोसर (*), और संघ (|), साथ ही फ्यूजन के लिए ऑपरेटर (:), प्रतिछेदन (&&) और कमजोर संस्करण (&) और निरंतर गिनती के लिए कई विविधताएं [*n] और निरंतर गिनती के रूप में एक उदाहरण इस प्रकार है [=n] और [->n].
ट्रिगर ऑपरेटर नीचे दी गई तालिका में दिखाए गए कई रूपों में आता है।
यहाँ s और t पीएसएल रेगुलर एक्सप्रेशन हैं और पी एक पीएसएल सूत्र के रूप में होता है।
s |=> t!
|
यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है।
|
s |-> t!
|
यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है।
|
s |=> t
|
यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है।
|
s |-> t
|
यदि s का मेल है, तो ट्रेस के प्रत्यय पर t का मेल है।
|
संयोजन, संलयन, संघ, प्रतिच्छेदन और उनकी विविधताओं के लिए ऑपरेटर नीचे दी गई तालिका में दिखाए गए हैं।
यहाँ 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[=i..j]
|
कम से कम i और j से अधिक नहीं जरूरी नहीं कि लगातार b की पुनरावृत्ति हो,
|
b[=i..]
|
कम से कम मैं जरूरी नहीं कि बी की लगातार पुनरावृत्ति हो
|
b[->m]
|
एम आवश्यक रूप से बी के साथ समाप्त होने वाले बी की लगातार पुनरावृत्ति नहीं है,
|
b[->m:n]
|
कम से कम m और n से अधिक नहीं आवश्यक रूप से b के साथ समाप्त होने वाले b का लगातार दोहराव नहीं है,
|
b[->m..]
|
कम से कम m अनिवार्य रूप से b के साथ समाप्त होने वाले b की लगातार पुनरावृत्ति नहीं है,
|
b[->]
|
शॉर्टकट के लिए b[->1], है
|
एलटीएल-शैली ऑपरेटर
नीचे पीएसएल के कुछ एलटीएल-शैली के ऑपरेटरों का एक नमूना है।
यहाँ 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 कहाँ p एक पीएसएल फॉर्मूला है और c एक पीएसएल बूलियन एक्सप्रेशंस दिए गए पथ पर होल्ड करता है यदि p उस पथ पर प्रक्षेपित चक्रों पर जिसमें c धारण करता है, जैसा कि दाईं ओर के आंकड़ों में दिखाया गया है।
पहली गुणधर्म बताती है कि हर request जिसके तुरंत बाद एक है ack संकेत, एक पूर्ण द्वारा पीछा किया जाना चाहिए data transfer, जहां एक पूर्ण डेटा स्थानांतरण सिग्नल से प्रारंभ होने वाला अनुक्रम है start, संकेत के साथ समाप्त end जिसमें data कम से कम 8 बार रुकना चाहिए:
(true[*]; req; ack) |=> (start; data[=8]; end)
लेकिन कभी-कभी केवल उन स्थितियों ं पर विचार करना वांछित होता है जहां उपरोक्त संकेत एक चक्र पर होते हैं जहां clk उच्च है। यह दूसरे चित्र में दर्शाया गया है जिसमें चूंकि सूत्र
((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk
उपयोग data[*3] और [*n] निरंतर दोहराव है, मिलान ट्रेस में 3 गैर-निरंतर समय बिंदु होते हैं data धारण करता है, लेकिन जब केवल समय बिंदुओं पर विचार किया जाता है clk धारण करता है, समय बिंदु कहाँ है data निरंतर होल्ड करें।
नेस्टेड @ वाले सूत्रों का शब्दार्थ थोड़ा सूक्ष्म है। इच्छुक पाठक [2] को संदर्भित करता है।
ऑपरेटरों को छोड़ें
पीएसएल के पास काटे गए रास्तों से निपटने के लिए कई ऑपरेटर हैं (परिमित पथ जो संगणना के एक उपसर्ग के अनुरूप हो सकते हैं)। काटे गए पथ रीसेट और कई अन्य परिदृश्यों के कारण बाउंडेड-मॉडल जाँच में होते हैं। एबॉर्ट ऑपरेटर निर्दिष्ट करते हैं कि किसी पथ को छोटा किए जाने पर संभावित घटनाओं से कैसे निपटा जाए। वे [1] में प्रस्तावित संक्षिप्त शब्दार्थ पर भरोसा करते हैं।
यहाँ p कोई पीएसएल फॉर्मूला है और b कोई भी पीएसएल बूलियन व्यंजक है।
p async_abort b
|
either p holds or p does not fail up until b holds;
|
p sync_abort b
|
either p holds or p does not fail up until b holds;
|
p abort b
|
equivalent to p async_abort b |
अभिव्यंजक शक्ति
पीएसएल टेम्पोरल लॉजिक लीनियर टेम्पोरल लॉजिक को समाहित करता है और अपनी अभिव्यंजक शक्ति को ओमेगा-नियमित भाषाओं तक बढ़ाता है। एलटीएल की तुलना में अभिव्यंजक शक्ति में वृद्धि, जिसमें स्टार-मुक्त ω-नियमित अभिव्यक्तियों की अभिव्यंजक शक्ति होती है, को प्रत्यय निहितार्थ के लिए जिम्मेदार ठहराया जा सकता है, जिसे ट्रिगर्स ऑपरेटर के रूप में भी जाना जाता है, जिसे |-> दर्शाया गया है। सूत्र r |-> f जहां r एक रेगुलर एक्सप्रेशन है और f एक टेम्पोरल लॉजिक फॉर्मूला है जो गणना w पर टिका रहता है यदि w मैचिंग r के किसी भी उपसर्ग में निरंतर संतोषजनक f है। पीएसएल के अन्य गैर-एलटीएल ऑपरेटर हैं @ ऑपरेटर, मल्टी-क्लॉक्ड डिज़ाइन निर्दिष्ट करने के लिए, एबॉर्ट ऑपरेटर, हार्डवेयर रीसेट से निपटने के लिए, और संक्षिप्तता के लिए स्थानीय चर।
परतें
पीएसएल को 4 परतों में परिभाषित किया गया है: बूलियन परत, टेम्पोरल परत, मॉडलिंग परत और सत्यापन परत।
- बूलियन परत का उपयोग डिजाइन की वर्तमान स्थिति का वर्णन करने के लिए किया जाता है और उपर्युक्त एचडीएल में से किसी एक का उपयोग करके इसका वर्णन किया जाता है।
- टेम्पोरल लेयर में टेम्पोरल ऑपरेटर्स होते हैं जिनका उपयोग उन परिदृश्यों का वर्णन करने के लिए किया जाता है जो समय के साथ विस्तारित होते हैं (संभवतः समय इकाइयों की असीमित संख्या में)।
- मॉडलिंग परत का उपयोग प्रक्रियात्मक विधियों से सहायक राज्य मशीनों का वर्णन करने के लिए किया जा सकता है।
- सत्यापन परत में एक सत्यापन उपकरण के लिए निर्देश होते हैं (उदाहरण के लिए यह प्रमाणित करने के लिए कि दी गई गुणधर्म सही है या यह मानने के लिए कि गुणों का एक निश्चित सेट गुणों के दूसरे सेट की पुष्टि करते समय सही है)।
लैंग्वेज अनुकूलता
गुणधर्म विशिष्टता लैंग्वेज का उपयोग कई इलेक्ट्रॉनिक सिस्टम डिज़ाइन भाषाओं (HDL) के साथ किया जा सकता है जैसे:
- वीएचडीएल (आईईईई 1076)
- Verilog (आईईईई 1364)
- सिस्टम वेरिलॉग (आईईईई 1800)
- सिस्टमसी (आईईईई 1666) [[ओपन सिस्टम सी पहल]] द्वारा। ओपन सिस्टमसी इनिशिएटिव (ओएससीआई)।
जब पीएसएल का उपयोग उपरोक्त HDL में से किसी एक के साथ किया जाता है, तो इसकी बूलियन परत संबंधित HDL के ऑपरेटरों का उपयोग करती है।
संदर्भ
- 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 मानक श्रेणी:आईईसी मानक
