لغة مواصفات العقار

لغة مواصفات الخصائص ( PSL ) هي منطق زمني يمتد من المنطق الزمني الخطي، مع مجموعة من المعاملات لتسهيل التعبير وتعزيز القدرة التعبيرية. تستخدم PSL على نطاق واسع التعابير النمطية والتحسينات النحوية. وهي شائعة الاستخدام في صناعة تصميم الأجهزة والتحقق منها، حيث تُستخدم أدوات التحقق الرسمي (مثل فحص النموذج ) و/أو أدوات محاكاة المنطق لإثبات أو دحض صحة صيغة PSL معينة على تصميم محدد.

طُوِّرت لغة PSL في البداية من قِبَل شركة Accellera لتحديد خصائص أو تأكيدات تصميمات الأجهزة. ومنذ سبتمبر 2004، جرى توحيد معايير هذه اللغة في مجموعة عمل IEEE 1850. وفي سبتمبر 2005، أُعلن عن معيار IEEE 1850 للغة تحديد الخصائص (PSL).

بناء الجملة والدلالات

يمكن لـ PSL أن تعبر عن أنه إذا حدث سيناريو معين الآن، فمن المفترض أن يحدث سيناريو آخر في وقت لاحق. على سبيل المثال، يمكن التعبير عن خاصية " يجب دائمًا الموافقة على الطلب في النهاية" باستخدام صيغة PSL التالية:

 دائماً (طلب -> في النهاية! منح)

يمكن التعبير عن الخاصية "كل طلب يتبعه مباشرة إشارة تأكيد ، يجب أن يتبعه نقل بيانات كامل ، حيث يكون نقل البيانات الكامل عبارة عن تسلسل يبدأ بإشارة البدء وينتهي بإشارة النهاية التي يكون فيها مشغولاً في هذه الأثناء" بواسطة صيغة PSL:

 (صحيح[*]؛ طلب؛ تأكيد) |=> (بدء؛ مشغول[*]؛ نهاية)

يُظهر الشكل الموجود على اليمين أثراً يحقق هذه الصيغة.

يمكن تصنيف عوامل التشغيل الزمنية في لغة PSL تقريبًا إلى عوامل تشغيل على نمط LTL وعوامل تشغيل على نمط التعبيرات النمطية . تأتي العديد من عوامل PSL بنسختين: نسخة قوية، يُشار إليها بعلامة تعجب ( ! )، ونسخة ضعيفة. تُشترط النسخة القوية تحقق شرط معين (أي أن شيئًا ما سيتحقق في المستقبل)، بينما لا تشترط النسخة الضعيفة ذلك . يُستخدم رمز الشرطة السفلية ( _ ) للتمييز بين الشروط الشاملة وغير الشاملة . يُستخدم الرمزان _a و_ e للدلالة على الشروط الشاملة (الكل) مقابل الشروط الوجودية (الموجودة). يُشار إلى النوافذ الزمنية الدقيقة بـ [n] ، بينما يُشار إلى النوافذ الزمنية المرنة بـ [m..n] .

مشغلون على نمط SERE

أكثر عوامل PSL استخدامًا هو عامل "الاستلزام اللاحق" (المعروف أيضًا باسم عامل "المحفزات")، ويُرمز له بـ |=> . معامله الأيسر هو تعبير نمطي PSL، ومعامله الأيمن هو أي صيغة PSL (سواء كانت بنمط LTL أو بنمط التعبير النمطي). دلالة r |=> p هي أنه عند كل نقطة زمنية i بحيث يُطابق تسلسل النقاط الزمنية حتى i التعبير النمطي r، يجب أن يُحقق المسار من i+1 الخاصية p. يوضح الشكلان على اليمين هذا الأمر.

تحتوي التعبيرات النمطية لـ PSL على عوامل مشتركة للربط ( ; )، وإغلاق كلين ( * )، والاتحاد ( | )، بالإضافة إلى عامل للدمج ( : )، والتقاطع ( && ) ونسخة أضعف ( & )، والعديد من الاختلافات للعد المتتالي [*n] والعد غير المتتالي على سبيل المثال [=n] و [->n] .

يأتي مشغل الزناد بعدة أشكال مختلفة، موضحة في الجدول أدناه.

هنا s و t عبارة عن تعبيرات منتظمة من نوع PSL، و p عبارة عن صيغة PSL.

s \|=> t!	إذا كان هناك تطابق للحرف s، فسيكون هناك تطابق للحرف t في لاحقة الأثر. يبدأ t الدورة بعد انتهاء s، يجب أن تصل مباراة t إلى نهايتها
s \|-> t!	إذا كان هناك تطابق للحرف s، فسيكون هناك تطابق للحرف t في لاحقة الأثر. يبدأ t نفس الدورة التي ينتهي عندها s، يجب أن تصل مباراة t إلى نهايتها
s \|=> t	إذا كان هناك تطابق للحرف s، فسيكون هناك تطابق للحرف t في لاحقة الأثر. يبدأ t الدورة بعد انتهاء s، قد "تتعثر" مباراة t في المنتصف
s \|-> t	إذا كان هناك تطابق للحرف s، فسيكون هناك تطابق للحرف t في لاحقة الأثر. يبدأ t نفس الدورة التي ينتهي عندها s، قد "تتعثر" مباراة t في المنتصف

يتم عرض عوامل الربط والدمج والاتحاد والتقاطع وتنوعاتها في الجدول أدناه.

هنا s و t عبارة عن تعبيرات منتظمة من لغة PSL.

`s ; t`	تطابق s متبوعًا بتطابق t، يبدأ t الدورة بعد انتهاء s
`s : t`	إذا تطابق الحرف s متبوعًا بتطابق الحرف t، يبدأ الحرف t نفس الدورة التي ينتهي عندها الحرف s
`s \| t`	تطابق حرف s أو تطابق حرف t
`s && t`	تطابق s وتطابق t، مدة كليهما متساوية
`s & t`	قد تختلف مدة تطابق حرف "s" وتطابق حرف "t".
`s within t`	مطابقة s داخل مطابقة t، اختصار لـ ([]; s; []) && t

تظهر عوامل التشغيل للتكرارات المتتالية في الجدول أدناه.

هنا s هو تعبير نمطي بلغة PSL.

`s[*i]`	تكرارات متتالية لـ
`s[*i..j]`	بين i و j تكرارات متتالية من s
`s[*i..]`	على الأقل i إلى تكرارات متتالية من s
`s[*]`	تكرار صفر أو أكثر من s على التوالي
`s[+]`	تكرار واحد أو أكثر متتالي لـ s

تظهر عوامل التشغيل للتكرارات غير المتتالية في الجدول أدناه.

هنا b هو أي تعبير منطقي من لغة PSL.

`b[=i]`	لا يشترط أن تكون تكرارات متتالية للحرف b، مكافئ لـ (!b[];b)[i]; !b[*]
`b[=i..j]`	على الأقل i ولا يزيد عن j، ليس بالضرورة تكرارات متتالية لـ b، مكافئ لـ (!b[];b)[i..j]; !b[*]
`b[=i..]`	على الأقل ليس بالضرورة تكرارات متتالية لـ b، مكافئ لـ (!b[];b)[i..]; !b[*]
`b[->m]`	لا يشترط أن تكون m تكرارات متتالية للحرف b تنتهي بالحرف b، مكافئ لـ (!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)

عوامل التشغيل بنمط LTL

فيما يلي عينة من بعض عوامل التشغيل من نوع LTL في لغة PSL.

هنا، p و q هما أي صيغ من صيغ PSL.

`always p`	خاصية p مخفية في كل نقطة زمنية
`never p`	لا تنطبق الخاصية 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`	توجد نقطة زمنية، ضمن الفترة من m إلى n من الفترة الحالية حيث يتحقق الشرط p.
`next_e[m..n] p`	إذا كان هناك على الأقل نقطة زمنية رقم n، فإن p يتحقق عند إحدى النقاط من m إلى n.
`next_a![m..n] p`	يوجد على الأقل n نقطة زمنية أخرى، ويكون الشرط p صحيحًا في جميع النقاط الزمنية بين النقطة m والنقطة n، شاملةً.
`next_a[m..n] p`	ينطبق الشرط p على جميع النقاط الزمنية التالية من m إلى n، مهما كان عددها.
`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 صيغة PSL و c تعبير منطقي PSL، تكون صحيحة على مسار معين إذا كانت p على ذلك المسار مُسقطة على الدورات التي تكون فيها c صحيحة، كما هو موضح في الأشكال على اليمين.

تنص الخاصية الأولى على أنه " يجب أن يتبع كل طلب متبوع مباشرة بإشارة تأكيد ، نقل بيانات كامل ، حيث يكون نقل البيانات الكامل عبارة عن تسلسل يبدأ بإشارة البدء وينتهي بإشارة النهاية ، ويجب أن يحتوي على البيانات 8 مرات على الأقل:

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

لكن في بعض الأحيان يُفضّل النظر فقط في الحالات التي تحدث فيها الإشارات المذكورة أعلاه في دورة يكون فيها تردد الساعة مرتفعًا. وهذا موضح في الشكل الثاني، حيث على الرغم من أن الصيغة

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

يستخدم البيانات[*3] و [*n] هو تكرار متتالي، يحتوي المسار المطابق على 3 نقاط زمنية غير متتالية حيث تكون البيانات موجودة، ولكن عند النظر فقط في النقاط الزمنية التي تكون فيها إشارة الساعة موجودة، تصبح النقاط الزمنية التي تكون فيها البيانات متتالية.

إن دلالات الصيغ التي تحتوي على علامة @ متداخلة دقيقة بعض الشيء. يُرجى الرجوع إلى [2] لمزيد من المعلومات.

مشغلو الإجهاض

تحتوي لغة PSL على عدة عوامل للتعامل مع المسارات المبتورة (المسارات المحدودة التي قد تُطابق بادئة الحساب). تظهر المسارات المبتورة في التحقق من النماذج المحدودة، نتيجةً لعمليات إعادة الضبط، وفي العديد من السيناريوهات الأخرى. تُحدد عوامل الإجهاض كيفية التعامل مع الحالات الطارئة عند اقتطاع مسار ما، وهي تعتمد على دلالات الاقتطاع المقترحة في [1].

هنا p هي أي صيغة PSL و b هي أي تعبير منطقي PSL.

`p async_abort b`	إما أن تكون قيمة p صحيحة أو أن قيمة p لا تفشل حتى تتحقق قيمة b؛ ب- تم التعرف عليه بشكل غير متزامن
`p sync_abort b`	إما أن تكون قيمة p صحيحة أو أن قيمة p لا تفشل حتى تتحقق قيمة b؛ ب- تم التعرف عليها بشكل متزامن
`p abort b`	مكافئ لـ p async_abort b

القدرة التعبيرية

تستوعب لغة PSL منطق الزمن LTL وتوسع قدرتها التعبيرية لتشمل لغات أوميغا المنتظمة . يُعزى هذا التحسن في القدرة التعبيرية، مقارنةً بلغة LTL التي تتمتع بقدرة تعبيرية مماثلة لتعبيرات أوميغا المنتظمة الخالية من النجمة، إلى خاصية الاستلزام اللاحق ، المعروفة أيضًا بمعامل التشغيل ، والمُشار إليها بـ "|->". تتحقق الصيغة r |-> f، حيث r تعبير منتظم و f صيغة منطقية زمنية، في عملية حسابية w إذا كان لأي بادئة من w تُطابق r استمرار يُحقق f . من بين معاملات PSL الأخرى غير LTL: المعامل @ ، لتحديد التصاميم متعددة التوقيت، ومعاملات الإجهاض ، للتعامل مع إعادة ضبط الأجهزة، والمتغيرات المحلية للاختصار.

الطبقات

يتم تعريف PSL في 4 طبقات: الطبقة المنطقية ، والطبقة الزمنية ، وطبقة النمذجة ، وطبقة التحقق .

تُستخدم الطبقة المنطقية لوصف الحالة الحالية للتصميم ويتم صياغتها باستخدام إحدى لغات وصف الأجهزة المذكورة أعلاه.
تتكون الطبقة الزمنية من عوامل التشغيل الزمنية المستخدمة لوصف السيناريوهات التي تمتد عبر الزمن (ربما عبر عدد غير محدود من الوحدات الزمنية).
يمكن استخدام طبقة النمذجة لوصف آلات الحالة المساعدة بطريقة إجرائية.
تتكون طبقة التحقق من توجيهات لأداة التحقق (على سبيل المثال، للتأكيد على أن خاصية معينة صحيحة أو لافتراض أن مجموعة معينة من الخصائص صحيحة عند التحقق من مجموعة أخرى من الخصائص).

التوافق اللغوي

يمكن استخدام لغة مواصفات الخصائص مع لغات تصميم الأنظمة الإلكترونية المتعددة (HDLs) مثل:

VHDL (IEEE 1076)
فيريلوج (IEEE 1364)
SystemVerilog (IEEE 1800)
SystemC (IEEE 1666) من خلال مبادرة Open SystemC (OSCI) .

عند استخدام PSL بالتزامن مع أحد لغات وصف الأجهزة المذكورة أعلاه، فإن طبقة Boolean الخاصة بها تستخدم عوامل التشغيل الخاصة بلغة وصف الأجهزة المعنية.

مراجع

1850-2005 – معيار IEEE للغة مواصفات الخصائص (PSL) . 2005. doi : 10.1109/IEEESTD.2005.97780 . ISBN 0-7381-4780-X.
- IEC 62531:2007 62531-2007 – IEC 62531 الإصدار 1 (2007-11) (IEEE Std 1850-2005): معيار لغة مواصفات الخصائص (PSL) . 2007. doi : 10.1109/IEEESTD.2007.4408637 . ISBN 978-0-7381-5727-6.
1850-2010 – معيار IEEE للغة مواصفات الخصائص (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): معيار لغة مواصفات الخصائص (PSL) . 2012. doi : 10.1109/IEEESTD.2012.6228486 . ISBN 978-0-7381-7299-6.
إيسنر، سيندي؛ فيسمان، دانا ؛ هافليسيك، جون؛ لوستيج، يواد؛ ماكإسحاق، أنتوني؛ فان كامبنهوت، ديفيد (2003). "الاستدلال باستخدام المنطق الزمني على المسارات المبتورة" (ملف PDF) . التحقق بمساعدة الحاسوب . سلسلة محاضرات في علوم الحاسوب. المجلد 2725. ص 27. doi : 10.1007/978-3-540-45069-6_3 . ISBN 978-3-540-40524-5.
إيسنر، سيندي؛ فيسمان، دانا ؛ هافليسيك، جون؛ ماكإسحاق، أنتوني؛ فان كامبنهوت، ديفيد (2003). "تعريف مُشغِّل الساعة الزمنية" (ملف PDF) . الأوتوماتا، واللغات، والبرمجة . سلسلة محاضرات في علوم الحاسوب. المجلد 2719. ص 857. doi : 10.1007/3-540-45061-0_67 . ISBN 978-3-540-40493-4.

روابط خارجية

مجموعة عمل IEEE 1850
إعلان معهد مهندسي الكهرباء والإلكترونيات (IEEE) - سبتمبر 2005
أكسيليرا
دليل المصممين لـ PSL