CINXE.COM

<!DOCTYPE html> <html class="client-nojs vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available" lang="en" dir="ltr"> <head> <meta charset="UTF-8"> <title>Property Specification Language - Wikipedia</title> <script>(function(){var className="client-js vector-feature-language-in-header-enabled vector-feature-language-in-main-page-header-disabled vector-feature-sticky-header-disabled vector-feature-page-tools-pinned-disabled vector-feature-toc-pinned-clientpref-1 vector-feature-main-menu-pinned-disabled vector-feature-limited-width-clientpref-1 vector-feature-limited-width-content-enabled vector-feature-custom-font-size-clientpref-1 vector-feature-appearance-pinned-clientpref-1 vector-feature-night-mode-enabled skin-theme-clientpref-day vector-toc-available";var cookie=document.cookie.match(/(?:^|; )enwikimwclientpreferences=([^;]+)/);if(cookie){cookie[1].split('%2C').forEach(function(pref){className=className.replace(new RegExp('(^| )'+pref.replace(/-clientpref-\w+$|[^\w-]+/g,'')+'-clientpref-\\w+( |$)'),'$1'+pref+'$2');});}document.documentElement.className=className;}());RLCONF={"wgBreakFrames":false,"wgSeparatorTransformTable":["",""],"wgDigitTransformTable":["",""],"wgDefaultDateFormat":"dmy", "wgMonthNames":["","January","February","March","April","May","June","July","August","September","October","November","December"],"wgRequestId":"00892ed6-11b3-4157-8e45-d5f53996b312","wgCanonicalNamespace":"","wgCanonicalSpecialPageName":false,"wgNamespaceNumber":0,"wgPageName":"Property_Specification_Language","wgTitle":"Property Specification Language","wgCurRevisionId":1237719664,"wgRevisionId":1237719664,"wgArticleId":762084,"wgIsArticle":true,"wgIsRedirect":false,"wgAction":"view","wgUserName":null,"wgUserGroups":["*"],"wgCategories":["Pages using the JsonConfig extension","Hardware verification languages","Formal specification languages","IEEE DASC standards","IEC standards"],"wgPageViewLanguage":"en","wgPageContentLanguage":"en","wgPageContentModel":"wikitext","wgRelevantPageName":"Property_Specification_Language","wgRelevantArticleId":762084,"wgIsProbablyEditable":true,"wgRelevantPageIsProbablyEditable":true,"wgRestrictionEdit":[],"wgRestrictionMove":[],"wgNoticeProject": "wikipedia","wgCiteReferencePreviewsActive":false,"wgFlaggedRevsParams":{"tags":{"status":{"levels":1}}},"wgMediaViewerOnClick":true,"wgMediaViewerEnabledByDefault":true,"wgPopupsFlags":0,"wgVisualEditor":{"pageLanguageCode":"en","pageLanguageDir":"ltr","pageVariantFallbacks":"en"},"wgMFDisplayWikibaseDescriptions":{"search":true,"watchlist":true,"tagline":false,"nearby":true},"wgWMESchemaEditAttemptStepOversample":false,"wgWMEPageLength":20000,"wgRelatedArticlesCompat":[],"wgCentralAuthMobileDomain":false,"wgEditSubmitButtonLabelPublish":true,"wgULSPosition":"interlanguage","wgULSisCompactLinksEnabled":false,"wgVector2022LanguageInHeader":true,"wgULSisLanguageSelectorEmpty":false,"wgWikibaseItemId":"Q751505","wgCheckUserClientHintsHeadersJsApi":["brands","architecture","bitness","fullVersionList","mobile","model","platform","platformVersion"],"GEHomepageSuggestedEditsEnableTopics":true,"wgGETopicsMatchModeEnabled":false,"wgGEStructuredTaskRejectionReasonTextInputEnabled":false, "wgGELevelingUpEnabledForUser":false};RLSTATE={"ext.globalCssJs.user.styles":"ready","site.styles":"ready","user.styles":"ready","ext.globalCssJs.user":"ready","user":"ready","user.options":"loading","ext.pygments":"ready","skins.vector.search.codex.styles":"ready","skins.vector.styles":"ready","skins.vector.icons":"ready","jquery.makeCollapsible.styles":"ready","ext.wikimediamessages.styles":"ready","ext.visualEditor.desktopArticleTarget.noscript":"ready","ext.uls.interlanguage":"ready","wikibase.client.init":"ready","ext.wikimediaBadges":"ready"};RLPAGEMODULES=["ext.pygments.view","mediawiki.page.media","site","mediawiki.page.ready","jquery.makeCollapsible","mediawiki.toc","skins.vector.js","ext.centralNotice.geoIP","ext.centralNotice.startUp","ext.gadget.ReferenceTooltips","ext.gadget.switcher","ext.urlShortener.toolbar","ext.centralauth.centralautologin","mmv.bootstrap","ext.popups","ext.visualEditor.desktopArticleTarget.init","ext.visualEditor.targetLoader","ext.echo.centralauth", "ext.eventLogging","ext.wikimediaEvents","ext.navigationTiming","ext.uls.interface","ext.cx.eventlogging.campaigns","ext.cx.uls.quick.actions","wikibase.client.vector-2022","ext.checkUser.clientHints","ext.growthExperiments.SuggestedEditSession","wikibase.sidebar.tracking"];</script> <script>(RLQ=window.RLQ||[]).push(function(){mw.loader.impl(function(){return["user.options@12s5i",function($,jQuery,require,module){mw.user.tokens.set({"patrolToken":"+\\","watchToken":"+\\","csrfToken":"+\\"}); }];});});</script> <link rel="stylesheet" href="/w/load.php?lang=en&modules=ext.pygments%2CwikimediaBadges%7Cext.uls.interlanguage%7Cext.visualEditor.desktopArticleTarget.noscript%7Cext.wikimediamessages.styles%7Cjquery.makeCollapsible.styles%7Cskins.vector.icons%2Cstyles%7Cskins.vector.search.codex.styles%7Cwikibase.client.init&only=styles&skin=vector-2022"> <script async="" src="/w/load.php?lang=en&modules=startup&only=scripts&raw=1&skin=vector-2022"></script> <meta name="ResourceLoaderDynamicStyles" content=""> <link rel="stylesheet" href="/w/load.php?lang=en&modules=site.styles&only=styles&skin=vector-2022"> <meta name="generator" content="MediaWiki 1.44.0-wmf.4"> <meta name="referrer" content="origin"> <meta name="referrer" content="origin-when-cross-origin"> <meta name="robots" content="max-image-preview:standard"> <meta name="format-detection" content="telephone=no"> <meta name="viewport" content="width=1120"> <meta property="og:title" content="Property Specification Language - Wikipedia"> <meta property="og:type" content="website"> <link rel="preconnect" href="//upload.wikimedia.org"> <link rel="alternate" media="only screen and (max-width: 640px)" href="//en.m.wikipedia.org/wiki/Property_Specification_Language"> <link rel="alternate" type="application/x-wiki" title="Edit this page" href="/w/index.php?title=Property_Specification_Language&action=edit"> <link rel="apple-touch-icon" href="/static/apple-touch/wikipedia.png"> <link rel="icon" href="/static/favicon/wikipedia.ico"> <link rel="search" type="application/opensearchdescription+xml" href="/w/rest.php/v1/search" title="Wikipedia (en)"> <link rel="EditURI" type="application/rsd+xml" href="//en.wikipedia.org/w/api.php?action=rsd"> <link rel="canonical" href="https://en.wikipedia.org/wiki/Property_Specification_Language"> <link rel="license" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en"> <link rel="alternate" type="application/atom+xml" title="Wikipedia Atom feed" href="/w/index.php?title=Special:RecentChanges&feed=atom"> <link rel="dns-prefetch" href="//meta.wikimedia.org" /> <link rel="dns-prefetch" href="//login.wikimedia.org"> </head> <body class="skin--responsive skin-vector skin-vector-search-vue mediawiki ltr sitedir-ltr mw-hide-empty-elt ns-0 ns-subject mw-editable page-Property_Specification_Language rootpage-Property_Specification_Language skin-vector-2022 action-view"><a class="mw-jump-link" href="#bodyContent">Jump to content</a> <div class="vector-header-container"> <header class="vector-header mw-header"> <div class="vector-header-start"> <nav class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-dropdown" class="vector-dropdown vector-main-menu-dropdown vector-button-flush-left vector-button-flush-right" > <input type="checkbox" id="vector-main-menu-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-main-menu-dropdown" class="vector-dropdown-checkbox " aria-label="Main menu" > <label id="vector-main-menu-dropdown-label" for="vector-main-menu-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-menu mw-ui-icon-wikimedia-menu"></span> <span class="vector-dropdown-label-text">Main menu</span> </label> <div class="vector-dropdown-content"> <div id="vector-main-menu-unpinned-container" class="vector-unpinned-container"> <div id="vector-main-menu" class="vector-main-menu vector-pinnable-element"> <div class="vector-pinnable-header vector-main-menu-pinnable-header vector-pinnable-header-unpinned" data-feature-name="main-menu-pinned" data-pinnable-element-id="vector-main-menu" data-pinned-container-id="vector-main-menu-pinned-container" data-unpinned-container-id="vector-main-menu-unpinned-container" > <div class="vector-pinnable-header-label">Main menu</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-main-menu.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-main-menu.unpin">hide</button> </div> <div id="p-navigation" class="vector-menu mw-portlet mw-portlet-navigation" > <div class="vector-menu-heading"> Navigation </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-mainpage-description" class="mw-list-item"><a href="/wiki/Main_Page" title="Visit the main page [z]" accesskey="z"><span>Main page</span></a></li><li id="n-contents" class="mw-list-item"><a href="/wiki/Wikipedia:Contents" title="Guides to browsing Wikipedia"><span>Contents</span></a></li><li id="n-currentevents" class="mw-list-item"><a href="/wiki/Portal:Current_events" title="Articles related to current events"><span>Current events</span></a></li><li id="n-randompage" class="mw-list-item"><a href="/wiki/Special:Random" title="Visit a randomly selected article [x]" accesskey="x"><span>Random article</span></a></li><li id="n-aboutsite" class="mw-list-item"><a href="/wiki/Wikipedia:About" title="Learn about Wikipedia and how it works"><span>About Wikipedia</span></a></li><li id="n-contactpage" class="mw-list-item"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us" title="How to contact Wikipedia"><span>Contact us</span></a></li> </ul> </div> </div> <div id="p-interaction" class="vector-menu mw-portlet mw-portlet-interaction" > <div class="vector-menu-heading"> Contribute </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="n-help" class="mw-list-item"><a href="/wiki/Help:Contents" title="Guidance on how to use and edit Wikipedia"><span>Help</span></a></li><li id="n-introduction" class="mw-list-item"><a href="/wiki/Help:Introduction" title="Learn how to edit Wikipedia"><span>Learn to edit</span></a></li><li id="n-portal" class="mw-list-item"><a href="/wiki/Wikipedia:Community_portal" title="The hub for editors"><span>Community portal</span></a></li><li id="n-recentchanges" class="mw-list-item"><a href="/wiki/Special:RecentChanges" title="A list of recent changes to Wikipedia [r]" accesskey="r"><span>Recent changes</span></a></li><li id="n-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_upload_wizard" title="Add images or other media for use on Wikipedia"><span>Upload file</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> <a href="/wiki/Main_Page" class="mw-logo"> <img class="mw-logo-icon" src="/static/images/icons/wikipedia.png" alt="" aria-hidden="true" height="50" width="50"> <span class="mw-logo-container skin-invert"> <img class="mw-logo-wordmark" alt="Wikipedia" src="/static/images/mobile/copyright/wikipedia-wordmark-en.svg" style="width: 7.5em; height: 1.125em;"> <img class="mw-logo-tagline" alt="The Free Encyclopedia" src="/static/images/mobile/copyright/wikipedia-tagline-en.svg" width="117" height="13" style="width: 7.3125em; height: 0.8125em;"> </span> </a> </div> <div class="vector-header-end"> <div id="p-search" role="search" class="vector-search-box-vue vector-search-box-collapses vector-search-box-show-thumbnail vector-search-box-auto-expand-width vector-search-box"> <a href="/wiki/Special:Search" class="cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only search-toggle" title="Search Wikipedia [f]" accesskey="f"><span class="vector-icon mw-ui-icon-search mw-ui-icon-wikimedia-search"></span> <span>Search</span> </a> <div class="vector-typeahead-search-container"> <div class="cdx-typeahead-search cdx-typeahead-search--show-thumbnail cdx-typeahead-search--auto-expand-width"> <form action="/w/index.php" id="searchform" class="cdx-search-input cdx-search-input--has-end-button"> <div id="simpleSearch" class="cdx-search-input__input-wrapper" data-search-loc="header-moved"> <div class="cdx-text-input cdx-text-input--has-start-icon"> <input class="cdx-text-input__input" type="search" name="search" placeholder="Search Wikipedia" aria-label="Search Wikipedia" autocapitalize="sentences" title="Search Wikipedia [f]" accesskey="f" id="searchInput" > <span class="cdx-text-input__icon cdx-text-input__start-icon"></span> </div> <input type="hidden" name="title" value="Special:Search"> </div> <button class="cdx-button cdx-search-input__end-button">Search</button> </form> </div> </div> </div> <nav class="vector-user-links vector-user-links-wide" aria-label="Personal tools"> <div class="vector-user-links-main"> <div id="p-vector-user-menu-preferences" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-userpage" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-dropdown" class="vector-dropdown " title="Change the appearance of the page's font size, width, and color" > <input type="checkbox" id="vector-appearance-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-appearance-dropdown" class="vector-dropdown-checkbox " aria-label="Appearance" > <label id="vector-appearance-dropdown-label" for="vector-appearance-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-appearance mw-ui-icon-wikimedia-appearance"></span> <span class="vector-dropdown-label-text">Appearance</span> </label> <div class="vector-dropdown-content"> <div id="vector-appearance-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <div id="p-vector-user-menu-notifications" class="vector-menu mw-portlet emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> <div id="p-vector-user-menu-overflow" class="vector-menu mw-portlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en" class=""><span>Donate</span></a> </li> <li id="pt-createaccount-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:CreateAccount&returnto=Property+Specification+Language" title="You are encouraged to create an account and log in; however, it is not mandatory" class=""><span>Create account</span></a> </li> <li id="pt-login-2" class="user-links-collapsible-item mw-list-item user-links-collapsible-item"><a data-mw="interface" href="/w/index.php?title=Special:UserLogin&returnto=Property+Specification+Language" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o" class=""><span>Log in</span></a> </li> </ul> </div> </div> </div> <div id="vector-user-links-dropdown" class="vector-dropdown vector-user-menu vector-button-flush-right vector-user-menu-logged-out" title="Log in and more options" > <input type="checkbox" id="vector-user-links-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-user-links-dropdown" class="vector-dropdown-checkbox " aria-label="Personal tools" > <label id="vector-user-links-dropdown-label" for="vector-user-links-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-ellipsis mw-ui-icon-wikimedia-ellipsis"></span> <span class="vector-dropdown-label-text">Personal tools</span> </label> <div class="vector-dropdown-content"> <div id="p-personal" class="vector-menu mw-portlet mw-portlet-personal user-links-collapsible-item" title="User menu" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-sitesupport" class="user-links-collapsible-item mw-list-item"><a href="https://donate.wikimedia.org/wiki/Special:FundraiserRedirector?utm_source=donate&utm_medium=sidebar&utm_campaign=C13_en.wikipedia.org&uselang=en"><span>Donate</span></a></li><li id="pt-createaccount" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:CreateAccount&returnto=Property+Specification+Language" title="You are encouraged to create an account and log in; however, it is not mandatory"><span class="vector-icon mw-ui-icon-userAdd mw-ui-icon-wikimedia-userAdd"></span> <span>Create account</span></a></li><li id="pt-login" class="user-links-collapsible-item mw-list-item"><a href="/w/index.php?title=Special:UserLogin&returnto=Property+Specification+Language" title="You're encouraged to log in; however, it's not mandatory. [o]" accesskey="o"><span class="vector-icon mw-ui-icon-logIn mw-ui-icon-wikimedia-logIn"></span> <span>Log in</span></a></li> </ul> </div> </div> <div id="p-user-menu-anon-editor" class="vector-menu mw-portlet mw-portlet-user-menu-anon-editor" > <div class="vector-menu-heading"> Pages for logged out editors <a href="/wiki/Help:Introduction" aria-label="Learn more about editing"><span>learn more</span></a> </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="pt-anoncontribs" class="mw-list-item"><a href="/wiki/Special:MyContributions" title="A list of edits made from this IP address [y]" accesskey="y"><span>Contributions</span></a></li><li id="pt-anontalk" class="mw-list-item"><a href="/wiki/Special:MyTalk" title="Discussion about edits from this IP address [n]" accesskey="n"><span>Talk</span></a></li> </ul> </div> </div> </div> </div> </nav> </div> </header> </div> <div class="mw-page-container"> <div class="mw-page-container-inner"> <div class="vector-sitenotice-container"> <div id="siteNotice"></div> </div> <div class="vector-column-start"> <div class="vector-main-menu-container"> <div id="mw-navigation"> <nav id="mw-panel" class="vector-main-menu-landmark" aria-label="Site"> <div id="vector-main-menu-pinned-container" class="vector-pinned-container"> </div> </nav> </div> </div> <div class="vector-sticky-pinned-container"> <nav id="mw-panel-toc" aria-label="Contents" data-event-name="ui.sidebar-toc" class="mw-table-of-contents-container vector-toc-landmark"> <div id="vector-toc-pinned-container" class="vector-pinned-container"> <div id="vector-toc" class="vector-toc vector-pinnable-element"> <div class="vector-pinnable-header vector-toc-pinnable-header vector-pinnable-header-pinned" data-feature-name="toc-pinned" data-pinnable-element-id="vector-toc" > <h2 class="vector-pinnable-header-label">Contents</h2> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-toc.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-toc.unpin">hide</button> </div> <ul class="vector-toc-contents" id="mw-panel-toc-list"> <li id="toc-mw-content-text" class="vector-toc-list-item vector-toc-level-1"> <a href="#" class="vector-toc-link"> <div class="vector-toc-text">(Top)</div> </a> </li> <li id="toc-Syntax_and_semantics" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#Syntax_and_semantics"> <div class="vector-toc-text"> <span class="vector-toc-numb">1</span> <span>Syntax and semantics</span> </div> </a> <button aria-controls="toc-Syntax_and_semantics-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle Syntax and semantics subsection</span> </button> <ul id="toc-Syntax_and_semantics-sublist" class="vector-toc-list"> <li id="toc-SERE-style_operators" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#SERE-style_operators"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.1</span> <span>SERE-style operators</span> </div> </a> <ul id="toc-SERE-style_operators-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-LTL-style_operators" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#LTL-style_operators"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.2</span> <span>LTL-style operators</span> </div> </a> <ul id="toc-LTL-style_operators-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Sampling_operator" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Sampling_operator"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.3</span> <span>Sampling operator</span> </div> </a> <ul id="toc-Sampling_operator-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Abort_operators" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Abort_operators"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.4</span> <span>Abort operators</span> </div> </a> <ul id="toc-Abort_operators-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Expressive_power" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Expressive_power"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.5</span> <span>Expressive power</span> </div> </a> <ul id="toc-Expressive_power-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Layers" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Layers"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.6</span> <span>Layers</span> </div> </a> <ul id="toc-Layers-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-Language_compatibility" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Language_compatibility"> <div class="vector-toc-text"> <span class="vector-toc-numb">1.7</span> <span>Language compatibility</span> </div> </a> <ul id="toc-Language_compatibility-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> <li id="toc-References" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#References"> <div class="vector-toc-text"> <span class="vector-toc-numb">2</span> <span>References</span> </div> </a> <ul id="toc-References-sublist" class="vector-toc-list"> </ul> </li> <li id="toc-External_links" class="vector-toc-list-item vector-toc-level-1 vector-toc-list-item-expanded"> <a class="vector-toc-link" href="#External_links"> <div class="vector-toc-text"> <span class="vector-toc-numb">3</span> <span>External links</span> </div> </a> <button aria-controls="toc-External_links-sublist" class="cdx-button cdx-button--weight-quiet cdx-button--icon-only vector-toc-toggle"> <span class="vector-icon mw-ui-icon-wikimedia-expand"></span> <span>Toggle External links subsection</span> </button> <ul id="toc-External_links-sublist" class="vector-toc-list"> <li id="toc-Books_on_PSL" class="vector-toc-list-item vector-toc-level-2"> <a class="vector-toc-link" href="#Books_on_PSL"> <div class="vector-toc-text"> <span class="vector-toc-numb">3.1</span> <span>Books on PSL</span> </div> </a> <ul id="toc-Books_on_PSL-sublist" class="vector-toc-list"> </ul> </li> </ul> </li> </ul> </div> </div> </nav> </div> </div> <div class="mw-content-container"> <main id="content" class="mw-body"> <header class="mw-body-header vector-page-titlebar"> <nav aria-label="Contents" class="vector-toc-landmark"> <div id="vector-page-titlebar-toc" class="vector-dropdown vector-page-titlebar-toc vector-button-flush-left" > <input type="checkbox" id="vector-page-titlebar-toc-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-titlebar-toc" class="vector-dropdown-checkbox " aria-label="Toggle the table of contents" > <label id="vector-page-titlebar-toc-label" for="vector-page-titlebar-toc-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--icon-only " aria-hidden="true" ><span class="vector-icon mw-ui-icon-listBullet mw-ui-icon-wikimedia-listBullet"></span> <span class="vector-dropdown-label-text">Toggle the table of contents</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-titlebar-toc-unpinned-container" class="vector-unpinned-container"> </div> </div> </div> </nav> <h1 id="firstHeading" class="firstHeading mw-first-heading"><span class="mw-page-title-main">Property Specification Language</span></h1> <div id="p-lang-btn" class="vector-dropdown mw-portlet mw-portlet-lang" > <input type="checkbox" id="p-lang-btn-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-p-lang-btn" class="vector-dropdown-checkbox mw-interlanguage-selector" aria-label="Go to an article in another language. Available in 4 languages" > <label id="p-lang-btn-label" for="p-lang-btn-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet cdx-button--action-progressive mw-portlet-lang-heading-4" aria-hidden="true" ><span class="vector-icon mw-ui-icon-language-progressive mw-ui-icon-wikimedia-language-progressive"></span> <span class="vector-dropdown-label-text">4 languages</span> </label> <div class="vector-dropdown-content"> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li class="interlanguage-link interwiki-de mw-list-item"><a href="https://de.wikipedia.org/wiki/Property_Specification_Language" title="Property Specification Language – German" lang="de" hreflang="de" data-title="Property Specification Language" data-language-autonym="Deutsch" data-language-local-name="German" class="interlanguage-link-target"><span>Deutsch</span></a></li><li class="interlanguage-link interwiki-fr mw-list-item"><a href="https://fr.wikipedia.org/wiki/Property_Specification_Language" title="Property Specification Language – French" lang="fr" hreflang="fr" data-title="Property Specification Language" data-language-autonym="Français" data-language-local-name="French" class="interlanguage-link-target"><span>Français</span></a></li><li class="interlanguage-link interwiki-ja mw-list-item"><a href="https://ja.wikipedia.org/wiki/Property_Specification_Language" title="Property Specification Language – Japanese" lang="ja" hreflang="ja" data-title="Property Specification Language" data-language-autonym="日本語" data-language-local-name="Japanese" class="interlanguage-link-target"><span>日本語</span></a></li><li class="interlanguage-link interwiki-pl mw-list-item"><a href="https://pl.wikipedia.org/wiki/PSL_(j%C4%99zyk_opisu_w%C5%82a%C5%9Bciwo%C5%9Bci)" title="PSL (język opisu właściwości) – Polish" lang="pl" hreflang="pl" data-title="PSL (język opisu właściwości)" data-language-autonym="Polski" data-language-local-name="Polish" class="interlanguage-link-target"><span>Polski</span></a></li> </ul> <div class="after-portlet after-portlet-lang"><span class="wb-langlinks-edit wb-langlinks-link"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q751505#sitelinks-wikipedia" title="Edit interlanguage links" class="wbc-editpage">Edit links</a></span></div> </div> </div> </div> </header> <div class="vector-page-toolbar"> <div class="vector-page-toolbar-container"> <div id="left-navigation"> <nav aria-label="Namespaces"> <div id="p-associated-pages" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-associated-pages" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-nstab-main" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Property_Specification_Language" title="View the content page [c]" accesskey="c"><span>Article</span></a></li><li id="ca-talk" class="vector-tab-noicon mw-list-item"><a href="/wiki/Talk:Property_Specification_Language" rel="discussion" title="Discuss improvements to the content page [t]" accesskey="t"><span>Talk</span></a></li> </ul> </div> </div> <div id="vector-variants-dropdown" class="vector-dropdown emptyPortlet" > <input type="checkbox" id="vector-variants-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-variants-dropdown" class="vector-dropdown-checkbox " aria-label="Change language variant" > <label id="vector-variants-dropdown-label" for="vector-variants-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">English</span> </label> <div class="vector-dropdown-content"> <div id="p-variants" class="vector-menu mw-portlet mw-portlet-variants emptyPortlet" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> </ul> </div> </div> </div> </div> </nav> </div> <div id="right-navigation" class="vector-collapsible"> <nav aria-label="Views"> <div id="p-views" class="vector-menu vector-menu-tabs mw-portlet mw-portlet-views" > <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-view" class="selected vector-tab-noicon mw-list-item"><a href="/wiki/Property_Specification_Language"><span>Read</span></a></li><li id="ca-edit" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-history" class="vector-tab-noicon mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&action=history" title="Past revisions of this page [h]" accesskey="h"><span>View history</span></a></li> </ul> </div> </div> </nav> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-dropdown" class="vector-dropdown vector-page-tools-dropdown" > <input type="checkbox" id="vector-page-tools-dropdown-checkbox" role="button" aria-haspopup="true" data-event-name="ui.dropdown-vector-page-tools-dropdown" class="vector-dropdown-checkbox " aria-label="Tools" > <label id="vector-page-tools-dropdown-label" for="vector-page-tools-dropdown-checkbox" class="vector-dropdown-label cdx-button cdx-button--fake-button cdx-button--fake-button--enabled cdx-button--weight-quiet" aria-hidden="true" ><span class="vector-dropdown-label-text">Tools</span> </label> <div class="vector-dropdown-content"> <div id="vector-page-tools-unpinned-container" class="vector-unpinned-container"> <div id="vector-page-tools" class="vector-page-tools vector-pinnable-element"> <div class="vector-pinnable-header vector-page-tools-pinnable-header vector-pinnable-header-unpinned" data-feature-name="page-tools-pinned" data-pinnable-element-id="vector-page-tools" data-pinned-container-id="vector-page-tools-pinned-container" data-unpinned-container-id="vector-page-tools-unpinned-container" > <div class="vector-pinnable-header-label">Tools</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-page-tools.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-page-tools.unpin">hide</button> </div> <div id="p-cactions" class="vector-menu mw-portlet mw-portlet-cactions emptyPortlet vector-has-collapsible-items" title="More options" > <div class="vector-menu-heading"> Actions </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="ca-more-view" class="selected vector-more-collapsible-item mw-list-item"><a href="/wiki/Property_Specification_Language"><span>Read</span></a></li><li id="ca-more-edit" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&action=edit" title="Edit this page [e]" accesskey="e"><span>Edit</span></a></li><li id="ca-more-history" class="vector-more-collapsible-item mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&action=history"><span>View history</span></a></li> </ul> </div> </div> <div id="p-tb" class="vector-menu mw-portlet mw-portlet-tb" > <div class="vector-menu-heading"> General </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-whatlinkshere" class="mw-list-item"><a href="/wiki/Special:WhatLinksHere/Property_Specification_Language" title="List of all English Wikipedia pages containing links to this page [j]" accesskey="j"><span>What links here</span></a></li><li id="t-recentchangeslinked" class="mw-list-item"><a href="/wiki/Special:RecentChangesLinked/Property_Specification_Language" rel="nofollow" title="Recent changes in pages linked from this page [k]" accesskey="k"><span>Related changes</span></a></li><li id="t-upload" class="mw-list-item"><a href="/wiki/Wikipedia:File_Upload_Wizard" title="Upload files [u]" accesskey="u"><span>Upload file</span></a></li><li id="t-specialpages" class="mw-list-item"><a href="/wiki/Special:SpecialPages" title="A list of all special pages [q]" accesskey="q"><span>Special pages</span></a></li><li id="t-permalink" class="mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&oldid=1237719664" title="Permanent link to this revision of this page"><span>Permanent link</span></a></li><li id="t-info" class="mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&action=info" title="More information about this page"><span>Page information</span></a></li><li id="t-cite" class="mw-list-item"><a href="/w/index.php?title=Special:CiteThisPage&page=Property_Specification_Language&id=1237719664&wpFormIdentifier=titleform" title="Information on how to cite this page"><span>Cite this page</span></a></li><li id="t-urlshortener" class="mw-list-item"><a href="/w/index.php?title=Special:UrlShortener&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FProperty_Specification_Language"><span>Get shortened URL</span></a></li><li id="t-urlshortener-qrcode" class="mw-list-item"><a href="/w/index.php?title=Special:QrCode&url=https%3A%2F%2Fen.wikipedia.org%2Fwiki%2FProperty_Specification_Language"><span>Download QR code</span></a></li> </ul> </div> </div> <div id="p-coll-print_export" class="vector-menu mw-portlet mw-portlet-coll-print_export" > <div class="vector-menu-heading"> Print/export </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="coll-download-as-rl" class="mw-list-item"><a href="/w/index.php?title=Special:DownloadAsPdf&page=Property_Specification_Language&action=show-download-screen" title="Download this page as a PDF file"><span>Download as PDF</span></a></li><li id="t-print" class="mw-list-item"><a href="/w/index.php?title=Property_Specification_Language&printable=yes" title="Printable version of this page [p]" accesskey="p"><span>Printable version</span></a></li> </ul> </div> </div> <div id="p-wikibase-otherprojects" class="vector-menu mw-portlet mw-portlet-wikibase-otherprojects" > <div class="vector-menu-heading"> In other projects </div> <div class="vector-menu-content"> <ul class="vector-menu-content-list"> <li id="t-wikibase" class="wb-otherproject-link wb-otherproject-wikibase-dataitem mw-list-item"><a href="https://www.wikidata.org/wiki/Special:EntityPage/Q751505" title="Structured data on this page hosted by Wikidata [g]" accesskey="g"><span>Wikidata item</span></a></li> </ul> </div> </div> </div> </div> </div> </div> </nav> </div> </div> </div> <div class="vector-column-end"> <div class="vector-sticky-pinned-container"> <nav class="vector-page-tools-landmark" aria-label="Page tools"> <div id="vector-page-tools-pinned-container" class="vector-pinned-container"> </div> </nav> <nav class="vector-appearance-landmark" aria-label="Appearance"> <div id="vector-appearance-pinned-container" class="vector-pinned-container"> <div id="vector-appearance" class="vector-appearance vector-pinnable-element"> <div class="vector-pinnable-header vector-appearance-pinnable-header vector-pinnable-header-pinned" data-feature-name="appearance-pinned" data-pinnable-element-id="vector-appearance" data-pinned-container-id="vector-appearance-pinned-container" data-unpinned-container-id="vector-appearance-unpinned-container" > <div class="vector-pinnable-header-label">Appearance</div> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-pin-button" data-event-name="pinnable-header.vector-appearance.pin">move to sidebar</button> <button class="vector-pinnable-header-toggle-button vector-pinnable-header-unpin-button" data-event-name="pinnable-header.vector-appearance.unpin">hide</button> </div> </div> </div> </nav> </div> </div> <div id="bodyContent" class="vector-body" aria-labelledby="firstHeading" data-mw-ve-target-container> <div class="vector-body-before-content"> <div class="mw-indicators"> </div> <div id="siteSub" class="noprint">From Wikipedia, the free encyclopedia</div> </div> <div id="contentSub"><div id="mw-content-subtitle"></div></div> <div id="mw-content-text" class="mw-body-content"><div class="mw-content-ltr mw-parser-output" lang="en" dir="ltr"><p><b>Property Specification Language</b> (<b>PSL</b>) is a <a href="/wiki/Temporal_logic" title="Temporal logic">temporal logic</a> extending <a href="/wiki/Linear_temporal_logic" title="Linear temporal logic">linear temporal logic</a> with a range of operators for both ease of expression and enhancement of expressive power. PSL makes an extensive use of <a href="/wiki/Regular_expressions" class="mw-redirect" title="Regular expressions">regular expressions</a> and syntactic sugaring. It is widely used in the hardware design and verification industry, where <a href="/wiki/Formal_verification" title="Formal verification">formal verification</a> tools (such as <a href="/wiki/Model_checking" title="Model checking">model checking</a>) and/or <a href="/wiki/Logic_simulation" title="Logic simulation">logic simulation</a> tools are used to prove or refute that a given PSL formula holds on a given design. </p><p>PSL was initially developed by <a href="/wiki/Accellera" title="Accellera">Accellera</a> for specifying <a href="/wiki/Property_(philosophy)" title="Property (philosophy)">properties</a> or <a href="/wiki/Assertion_(computing)" class="mw-redirect" title="Assertion (computing)">assertions</a> about hardware designs. Since September 2004 the <a href="/wiki/Standardization" title="Standardization">standardization</a> on the language has been done in <a href="/wiki/IEEE" class="mw-redirect" title="IEEE">IEEE</a> 1850 working group. In September 2005, the IEEE 1850 Standard for Property Specification Language (PSL) was announced. </p> <meta property="mw:PageProp/toc" /> <div class="mw-heading mw-heading2"><h2 id="Syntax_and_semantics">Syntax and semantics</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=1" title="Edit section: Syntax and semantics"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>PSL can express that if some scenario happens now, then another scenario should happen some time later. For instance, the property "a <style data-mw-deduplicate="TemplateStyles:r886049734">.mw-parser-output .monospaced{font-family:monospace,monospace}</style><span class="monospaced">request</span> should always eventually be <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">grant</span>ed" can be expressed by the PSL formula: </p> <div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> always (request -> eventually! grant) </pre></div> <p>The property "every <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">request</span> that is immediately followed by an <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">ack</span> signal, should be followed by a complete <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data transfer</span>, where a complete data transfer is a sequence starting with signal <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">start</span>, ending with signal <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">end</span> in which <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">busy</span> holds at the meantime" can be expressed by the PSL formula: </p> <div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> (true[*]; req; ack) |=> (start; busy[*]; end) </pre></div> <p>A trace satisfying this formula is given in the figure on the right. </p> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:The_trigger_operator_-_slide_1.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/8/88/The_trigger_operator_-_slide_1.jpg/220px-The_trigger_operator_-_slide_1.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/8/88/The_trigger_operator_-_slide_1.jpg/330px-The_trigger_operator_-_slide_1.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/8/88/The_trigger_operator_-_slide_1.jpg/440px-The_trigger_operator_-_slide_1.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>a simple trace satisfying <div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span>(true[*]; req; ack) |=> (start; busy[*]; end) </pre></div></figcaption></figure> <p>PSL's temporal operators can be roughly classified into <i>LTL-style</i> operators and <i>regular-expression-style</i> operators. Many PSL operators come in two versions, a strong version, indicated by an exclamation mark suffix ( <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">!</span> ), and a weak version. The <i>strong version</i> makes eventuality requirements (i.e. require that something will hold in the future), while the <i>weak version</i> does not. An <i>underscore suffix</i> ( <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">_</span> ) is used to differentiate <i>inclusive</i> vs. <i>non-inclusive</i> requirements. The <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">_a</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">_e</span> suffixes are used to denote <i>universal</i> (all) vs. <i>existential</i> (exists) requirements. Exact time windows are denoted by <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[n]</span> and flexible by <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[m..n]</span>. </p> <div class="mw-heading mw-heading3"><h3 id="SERE-style_operators">SERE-style operators</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=2" title="Edit section: SERE-style operators"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>The most commonly used PSL operator is the "suffix-implication" operator (also known as the "triggers" operator), which is denoted by <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">|=></span>. 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 <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">r |=> p</span> 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 is exemplified in the figures on the right. </p> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:The_trigger_operator_-_slide_2.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/1/1e/The_trigger_operator_-_slide_2.jpg/220px-The_trigger_operator_-_slide_2.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/1/1e/The_trigger_operator_-_slide_2.jpg/330px-The_trigger_operator_-_slide_2.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/1/1e/The_trigger_operator_-_slide_2.jpg/440px-The_trigger_operator_-_slide_2.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>path satisfying <i>r triggers p</i> in two non-overlapping ways</figcaption></figure> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:The_trigger_operator_-_slide_3.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/6/67/The_trigger_operator_-_slide_3.jpg/220px-The_trigger_operator_-_slide_3.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/6/67/The_trigger_operator_-_slide_3.jpg/330px-The_trigger_operator_-_slide_3.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/6/67/The_trigger_operator_-_slide_3.jpg/440px-The_trigger_operator_-_slide_3.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>path satisfying <i>r triggers p</i> in two overlapping ways</figcaption></figure> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:The_trigger_operator_-_slide_4.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/9/90/The_trigger_operator_-_slide_4.jpg/220px-The_trigger_operator_-_slide_4.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/9/90/The_trigger_operator_-_slide_4.jpg/330px-The_trigger_operator_-_slide_4.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/9/90/The_trigger_operator_-_slide_4.jpg/440px-The_trigger_operator_-_slide_4.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>path satisfying <i>r triggers p</i> in three ways</figcaption></figure> <p>The regular expressions of PSL have the common operators for concatenation (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">;</span>), Kleene-closure (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">*</span>), and union (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">|</span>), as well as operator for fusion (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">:</span>), intersection (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">&&</span>) and a weaker version (<link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">&</span>), and many variations for consecutive counting <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[*n]</span> and in-consecutive counting e.g. <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[=n]</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[->n]</span>. </p><p>The trigger operator comes in several variations, shown in the table below. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">s</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">t</span> are PSL-regular expressions, and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">p</span> is a PSL formula. </p> <table class="wikitable"> <tbody><tr> <td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> s |=> t! </pre></div> </td> <td>if there is a match of s, then there is a match of t on the suffix of the trace, <ul><li>t starts the cycle after s ends,</li> <li>the match of t must reach to its end</li></ul> </td></tr> <tr> <td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> s |-> t! </pre></div> </td> <td>if there is a match of s, then there is a match of t on the suffix of the trace, <ul><li>t starts the same cycle that s ends,</li> <li>the match of t must reach to its end</li></ul> </td></tr> <tr> <td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> s |=> t </pre></div> </td> <td>if there is a match of s, then there is a match of t on the suffix of the trace, <ul><li>t starts the cycle after s ends,</li> <li>the match of t may "get stuck" in the middle</li></ul> </td></tr> <tr> <td><div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> s |-> t </pre></div> </td> <td>if there is a match of s, then there is a match of t on the suffix of the trace, <ul><li>t starts the same cycle that s ends,</li> <li>the match of t may "get stuck" in the middle</li></ul> </td></tr> </tbody></table> <p>Operators for concatenation, fusion, union, intersection and their variations are shown in the table below. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">s</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">t</span> are PSL regular expressions. </p> <table class="wikitable"> <tbody><tr> <td><code> s ; t </code> </td> <td>match of s followed by a match of t, t starts the cycle after s ends </td></tr> <tr> <td><code>s : t </code> </td> <td>match of s followed by a match of t, t starts the same cycle that s ends </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr">s | t</code> </td> <td>match of s or match of t </td></tr> <tr> <td><code>s && t </code> </td> <td>match of s and match of t, duration of both is of same length </td></tr> <tr> <td><code>s & t </code> </td> <td>match of s and match of t, duration matches maybe different </td></tr> <tr> <td><code> s within t </code> </td> <td>match of s within a match of t, abbreviation of ([*]; s; [*]) && t </td></tr> </tbody></table> <p>Operators for consecutive repetitions are shown in the table below. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">s</span> is a PSL regular expression. </p> <table class="wikitable"> <tbody><tr> <td><code> s[*i] </code> </td> <td>i consecutive repetitions of s </td></tr> <tr> <td><code> s[*i..j] </code> </td> <td>between i to j consecutive repetitions of s </td></tr> <tr> <td><code> s[*i..] </code> </td> <td>at least i to consecutive repetitions of s </td></tr> <tr> <td><code> s[*] </code> </td> <td>zero or more consecutive repetitions of s </td></tr> <tr> <td><code> s[+] </code> </td> <td>one or more consecutive repetitions of s </td></tr> </tbody></table> <p>Operators for non-consecutive repetitions are shown in the table below. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">b</span> is any PSL Boolean expression. </p> <table class="wikitable"> <tbody><tr> <td><code> b[=i] </code> </td> <td>i not necessarily consecutive repetitions of b, <ul><li>equivalent to (!b[*];b)[*i]; !b[*]</li></ul> </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr">b[=i..j]</code> </td> <td>at least i and no more than j not necessarily consecutive repetitions of b, <ul><li>equivalent to (!b[*];b)[*i..j]; !b[*]</li></ul> </td></tr> <tr> <td><code> b[=i..] </code> </td> <td>at least i not necessarily consecutive repetitions of b, <ul><li>equivalent to (!b[*];b)[*i..]; !b[*]</li></ul> </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr">b[->m]</code> </td> <td>m not necessarily consecutive repetitions of b ending with b, <ul><li>equivalent to (!b[*];b)[*m]</li></ul> </td></tr> <tr> <td><code> b[->m:n] </code> </td> <td>at least m and no more than n not necessarily consecutive repetitions of b ending with b, <ul><li>equivalent to (!b[*];b)[*m..n]</li></ul> </td></tr> <tr> <td><code> b[->m..] </code> </td> <td>at least m not necessarily consecutive repetitions of b ending with b, <ul><li>equivalent to (!b[*];b)[*m..]; !b[*]</li></ul> </td></tr> <tr> <td><code> b[->] </code> </td> <td>shortcut for b[->1], <ul><li>equivalent to (!b[*];b)</li></ul> </td></tr> </tbody></table> <div class="mw-heading mw-heading3"><h3 id="LTL-style_operators">LTL-style operators</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=3" title="Edit section: LTL-style operators"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Below is a sample of some LTL-style operators of PSL. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">p</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">q</span> are any PSL formulas. </p> <table class="wikitable"> <tbody><tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">always p</code> </td> <td>property p holds on every time point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">never p</code> </td> <td>property p does not hold on any time point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">eventually! p</code> </td> <td>there exists a future time point where p holds </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next! p</code> </td> <td>there exists a next time point, and p holds on this point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next p</code> </td> <td>if there exists a next time point, then p holds on this point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next![n] p</code> </td> <td>there exists an n-th time point, and p holds on this point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next[n] p</code> </td> <td>if there exists an n-th time point, then p holds on this point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next_e![m..n] p</code> </td> <td>there exists a time point, within m-th to n-th from the current where p holds. </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next_e[m..n] p</code> </td> <td>if there exists at least n-th time points, then p holds on one of the m-th to n-th points. </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next_a![m..n] p</code> </td> <td>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. </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">next_a[m..n] p</code> </td> <td>p holds on all the next m-th through n-th time points, however many exist </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until! q</code> </td> <td>there exists a time point where q holds, and p hold up until that time point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until q</code> </td> <td>p holds up until a time point where q hold, if such exists </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until!_ q</code> </td> <td>there exists a time point where q holds, and p holds up until that time point and in that time point </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p until_ q</code> </td> <td>p holds up until a time point where q holds, and in that time point, if such exists </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before! q</code> </td> <td>p holds strictly before the time point where q holds, and p eventually holds </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before q</code> </td> <td>p holds strictly before the time point where q holds, if p never holds, then neither does q </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before!_ q</code> </td> <td>p holds before or at the same time point where q holds, and p eventually holds </td></tr> <tr> <td><code class="mw-highlight mw-highlight-lang-text mw-content-ltr" style="" dir="ltr">p before_ q</code> </td> <td>p holds before or at the same time point where q holds, if p never holds, then neither does q </td></tr> </tbody></table> <div class="mw-heading mw-heading3"><h3 id="Sampling_operator">Sampling operator</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=4" title="Edit section: Sampling operator"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Sometimes it is desirable to change the definition of the <i>next time-point</i>, for instance in multiply-clocked designs, or when a higher level of abstraction is desired. The <i>sampling operator</i> (also known as the <i>clock operator</i>), denoted <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">@</span>, is used for this purpose. The formula <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced"> p @ c </span> where <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced"> p</span> is a PSL formula and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">c</span> a PSL Boolean expressions holds on a given path if <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced"> p</span> on that path projected on the cycles in which <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced"> c</span> holds, as exemplified in the figures to the right. </p> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:Need_for_multiple_clocks.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/8/85/Need_for_multiple_clocks.jpg/220px-Need_for_multiple_clocks.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/8/85/Need_for_multiple_clocks.jpg/330px-Need_for_multiple_clocks.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/8/85/Need_for_multiple_clocks.jpg/440px-Need_for_multiple_clocks.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>path and formula showing need for a sampling operator</figcaption></figure> <p>The first property states that "every <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">request</span> that is immediately followed by an <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">ack</span> signal, should be followed by a complete <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data transfer</span>, where a complete data transfer is a sequence starting with signal <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">start</span>, ending with signal <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">end</span> in which <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data</span> should hold at least 8 times: </p> <div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> (true[*]; req; ack) |=> (start; data[=8]; end) </pre></div> <p>But sometimes it is desired to consider only the cases where the above signals occur on a cycle where <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">clk</span> is high. This is depicted in the second figure in which although the formula </p> <div class="mw-highlight mw-highlight-lang-text mw-content-ltr" dir="ltr"><pre><span></span> ((true[*]; req; ack) |=> (start; data[*3]; end)) @ clk </pre></div> <p>uses <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data[*3]</span> and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">[*n]</span> is consecutive repetition, the matching trace has 3 non-consecutive time points where <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data</span> holds, but when considering only the time points where <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">clk</span> holds, the time points where <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">data</span> hold become consecutive. </p> <figure class="mw-default-size" typeof="mw:File/Thumb"><a href="/wiki/File:Multiple_clocks.jpg" class="mw-file-description"><img src="//upload.wikimedia.org/wikipedia/commons/thumb/5/56/Multiple_clocks.jpg/220px-Multiple_clocks.jpg" decoding="async" width="220" height="165" class="mw-file-element" srcset="//upload.wikimedia.org/wikipedia/commons/thumb/5/56/Multiple_clocks.jpg/330px-Multiple_clocks.jpg 1.5x, //upload.wikimedia.org/wikipedia/commons/thumb/5/56/Multiple_clocks.jpg/440px-Multiple_clocks.jpg 2x" data-file-width="720" data-file-height="540" /></a><figcaption>path and formula showing effect of the sampling operator @</figcaption></figure> <p>The semantics of formulas with nested @ is a little subtle. The interested reader is referred to [2]. </p> <div class="mw-heading mw-heading3"><h3 id="Abort_operators">Abort operators</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=5" title="Edit section: Abort operators"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>PSL has several operators to deal with truncated paths (finite paths that may correspond to a prefix of 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]. </p><p>Here <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">p</span> is any PSL formula and <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r886049734"><span class="monospaced">b</span> is any PSL Boolean expression. </p> <table class="wikitable"> <tbody><tr> <td><code> p async_abort b </code> </td> <td>either p holds or p does not fail up until b holds; <ul><li>b recognized asynchronously</li></ul> </td></tr> <tr> <td><code> p sync_abort b </code> </td> <td>either p holds or p does not fail up until b holds; <ul><li>b recognized synchronously</li></ul> </td></tr> <tr> <td><code> p abort b </code> </td> <td>equivalent to p async_abort b </td></tr> </tbody></table> <div class="mw-heading mw-heading3"><h3 id="Expressive_power">Expressive power</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=6" title="Edit section: Expressive power"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>PSL subsumes the temporal logic <a href="/wiki/Linear_temporal_logic" title="Linear temporal logic">LTL</a> and extends its expressive power to that of the <a href="/wiki/Omega-regular_languages" class="mw-redirect" title="Omega-regular languages">omega-regular languages</a>. 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 <i>suffix implication</i>, also known as the <i>triggers</i> operator, denoted "|->". The formula <i>r |-> f</i> where <i>r</i> is a regular expression and <i>f</i> is a temporal logic formula holds on a computation <i>w</i> if any prefix of <i>w</i> matching <i>r</i> has a continuation satisfying <i>f</i>. Other non-LTL operators of PSL are the <i>@</i> operator, for specifying multiply-clocked designs, the <i>abort</i> operators, for dealing with hardware resets, and <i>local variables</i> for succinctness. </p> <div class="mw-heading mw-heading3"><h3 id="Layers">Layers</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=7" title="Edit section: Layers"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>PSL is defined in 4 layers: the <i>Boolean layer</i>, the <i>temporal layer</i>, the <i>modeling layer</i> and the <i>verification layer</i>. </p> <ul><li>The <i>Boolean layer</i> is used for describing a current state of the design and is phrased using one of the above-mentioned HDLs.</li> <li>The <i>temporal layer</i> consists of the temporal operators used to describe scenarios that span over time (possibly over an unbounded number of time units).</li> <li>The <i>modeling layer</i> can be used to describe auxiliary state machines in a procedural manner.</li> <li>The <i>verification layer</i> consists of directives to a verification tool (for instance to <i>assert</i> that a given property is correct or to <i>assume</i> that a certain set of properties is correct when verifying another set of properties).</li></ul> <div class="mw-heading mw-heading3"><h3 id="Language_compatibility">Language compatibility</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=8" title="Edit section: Language compatibility"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <p>Property Specification Language can be used with multiple electronic system design languages (HDLs) such as: </p> <ul><li><a href="/wiki/VHDL" title="VHDL">VHDL</a> (IEEE 1076)</li> <li><a href="/wiki/Verilog" title="Verilog">Verilog</a> (IEEE 1364)</li> <li><a href="/wiki/SystemVerilog" title="SystemVerilog">SystemVerilog</a> (IEEE 1800)</li> <li><a href="/wiki/SystemC" title="SystemC">SystemC</a> (IEEE 1666) by <a href="/wiki/Open_SystemC_Initiative" class="mw-redirect" title="Open SystemC Initiative">Open SystemC Initiative (OSCI)</a>.</li></ul> <p>When PSL is used in conjunction with one of the above HDLs, its Boolean layer uses the operators of the respective HDL. </p> <div class="mw-heading mw-heading2"><h2 id="References">References</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=9" title="Edit section: References"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><style data-mw-deduplicate="TemplateStyles:r1238218222">.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("//upload.wikimedia.org/wikipedia/commons/6/65/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("//upload.wikimedia.org/wikipedia/commons/d/d6/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("//upload.wikimedia.org/wikipedia/commons/a/aa/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("//upload.wikimedia.org/wikipedia/commons/4/4c/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}</style><cite class="citation book cs1"><i>1850-2005 – IEEE Standard for Property Specification Language (PSL)</i>. 2005. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2005.97780">10.1109/IEEESTD.2005.97780</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/0-7381-4780-X" title="Special:BookSources/0-7381-4780-X"><bdi>0-7381-4780-X</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=1850-2005+%E2%80%93+IEEE+Standard+for+Property+Specification+Language+%28PSL%29&rft.date=2005&rft_id=info%3Adoi%2F10.1109%2FIEEESTD.2005.97780&rft.isbn=0-7381-4780-X&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span> <ul><li>IEC 62531:2007 <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation book cs1"><i>62531-2007 – IEC 62531 Ed. 1 (2007-11) (IEEE Std 1850-2005): Standard for Property Specification Language (PSL)</i>. 2007. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2007.4408637">10.1109/IEEESTD.2007.4408637</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-0-7381-5727-6" title="Special:BookSources/978-0-7381-5727-6"><bdi>978-0-7381-5727-6</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=62531-2007+%E2%80%93+IEC+62531+Ed.+1+%282007-11%29+%28IEEE+Std+1850-2005%29%3A+Standard+for+Property+Specification+Language+%28PSL%29&rft.date=2007&rft_id=info%3Adoi%2F10.1109%2FIEEESTD.2007.4408637&rft.isbn=978-0-7381-5727-6&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span></li></ul></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation book cs1"><i>1850-2010 – IEEE Standard for Property Specification Language (PSL)</i>. 2010. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2010.5446004">10.1109/IEEESTD.2010.5446004</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-0-7381-6255-3" title="Special:BookSources/978-0-7381-6255-3"><bdi>978-0-7381-6255-3</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=1850-2010+%E2%80%93+IEEE+Standard+for+Property+Specification+Language+%28PSL%29&rft.date=2010&rft_id=info%3Adoi%2F10.1109%2FIEEESTD.2010.5446004&rft.isbn=978-0-7381-6255-3&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span> <ul><li>IEC 62531:2012 <link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite class="citation book cs1"><i>62531-2012 – IEC 62531:2012(E) (IEEE Std 1850-2010): Standard for Property Specification Language (PSL)</i>. 2012. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1109%2FIEEESTD.2012.6228486">10.1109/IEEESTD.2012.6228486</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-0-7381-7299-6" title="Special:BookSources/978-0-7381-7299-6"><bdi>978-0-7381-7299-6</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=book&rft.btitle=62531-2012+%E2%80%93+IEC+62531%3A2012%28E%29+%28IEEE+Std+1850-2010%29%3A+Standard+for+Property+Specification+Language+%28PSL%29&rft.date=2012&rft_id=info%3Adoi%2F10.1109%2FIEEESTD.2012.6228486&rft.isbn=978-0-7381-7299-6&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span></li></ul></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFEisnerFismanHavlicekLustig2003" class="citation book cs1">Eisner, Cindy; <a href="/wiki/Dana_Fisman" title="Dana Fisman">Fisman, Dana</a>; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). <a rel="nofollow" class="external text" href="http://www.research.ibm.com/people/e/eisner/papers/cav49.pdf">"Reasoning with Temporal Logic on Truncated Paths"</a> <span class="cs1-format">(PDF)</span>. <i><a href="/wiki/Computer_Aided_Verification" title="Computer Aided Verification">Computer Aided Verification</a></i>. Lecture Notes in Computer Science. Vol. 2725. p. 27. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F978-3-540-45069-6_3">10.1007/978-3-540-45069-6_3</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-3-540-40524-5" title="Special:BookSources/978-3-540-40524-5"><bdi>978-3-540-40524-5</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=Reasoning+with+Temporal+Logic+on+Truncated+Paths&rft.btitle=Computer+Aided+Verification&rft.series=Lecture+Notes+in+Computer+Science&rft.pages=27&rft.date=2003&rft_id=info%3Adoi%2F10.1007%2F978-3-540-45069-6_3&rft.isbn=978-3-540-40524-5&rft.aulast=Eisner&rft.aufirst=Cindy&rft.au=Fisman%2C+Dana&rft.au=Havlicek%2C+John&rft.au=Lustig%2C+Yoad&rft.au=McIsaac%2C+Anthony&rft.au=Van+Campenhout%2C+David&rft_id=http%3A%2F%2Fwww.research.ibm.com%2Fpeople%2Fe%2Feisner%2Fpapers%2Fcav49.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span></li> <li><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1238218222"><cite id="CITEREFEisnerFismanHavlicekMcIsaac2003" class="citation book cs1">Eisner, Cindy; <a href="/wiki/Dana_Fisman" title="Dana Fisman">Fisman, Dana</a>; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). <a rel="nofollow" class="external text" href="http://www.cis.upenn.edu/~fisman/documents/EFHMV_ICALP03_full.pdf">"The Definition of a Temporal Clock Operator"</a> <span class="cs1-format">(PDF)</span>. <i>Automata, Languages and Programming</i>. Lecture Notes in Computer Science. Vol. 2719. p. 857. <a href="/wiki/Doi_(identifier)" class="mw-redirect" title="Doi (identifier)">doi</a>:<a rel="nofollow" class="external text" href="https://doi.org/10.1007%2F3-540-45061-0_67">10.1007/3-540-45061-0_67</a>. <a href="/wiki/ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <a href="/wiki/Special:BookSources/978-3-540-40493-4" title="Special:BookSources/978-3-540-40493-4"><bdi>978-3-540-40493-4</bdi></a>.</cite><span title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rft.genre=bookitem&rft.atitle=The+Definition+of+a+Temporal+Clock+Operator&rft.btitle=Automata%2C+Languages+and+Programming&rft.series=Lecture+Notes+in+Computer+Science&rft.pages=857&rft.date=2003&rft_id=info%3Adoi%2F10.1007%2F3-540-45061-0_67&rft.isbn=978-3-540-40493-4&rft.aulast=Eisner&rft.aufirst=Cindy&rft.au=Fisman%2C+Dana&rft.au=Havlicek%2C+John&rft.au=McIsaac%2C+Anthony&rft.au=Van+Campenhout%2C+David&rft_id=http%3A%2F%2Fwww.cis.upenn.edu%2F~fisman%2Fdocuments%2FEFHMV_ICALP03_full.pdf&rfr_id=info%3Asid%2Fen.wikipedia.org%3AProperty+Specification+Language" class="Z3988"></span></li></ul> <div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=10" title="Edit section: External links"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a rel="nofollow" class="external text" href="http://www.eda.org/ieee-1850">IEEE 1850 working group</a></li> <li><a rel="nofollow" class="external text" href="https://web.archive.org/web/20051210035642/http://standards.ieee.org/announcements/pr_1850psl.html">IEEE Announcement September 2005</a></li> <li><a rel="nofollow" class="external text" href="http://www.accellera.org/">Accellera</a></li> <li><a rel="nofollow" class="external text" href="http://www.project-veripage.com/psl_tutorial_1.php">Property Specification Language Tutorial</a></li> <li><a rel="nofollow" class="external text" href="http://www.doulos.com/knowhow/psl/">Designers guide to PSL</a></li></ul> <div class="mw-heading mw-heading3"><h3 id="Books_on_PSL">Books on PSL</h3><span class="mw-editsection"><span class="mw-editsection-bracket">[</span><a href="/w/index.php?title=Property_Specification_Language&action=edit&section=11" title="Edit section: Books on PSL"><span>edit</span></a><span class="mw-editsection-bracket">]</span></span></div> <ul><li><a rel="nofollow" class="external text" href="http://www.systemverilog.us/psl_info.html">Using PSL/Sugar for Formal and Dynamic Verification 2nd Edition, Ben Cohen, Ajeetha Kumari, Srinivasan Venkataramanan</a></li> <li><a rel="nofollow" class="external text" href="https://www.springer.com/engineering/circuits+%26+systems/book/978-0-387-35313-5">A Practical Introduction to PSL</a>, Cindy Eisner and <a href="/wiki/Dana_Fisman" title="Dana Fisman">Dana Fisman</a></li></ul> <div class="navbox-styles"><style data-mw-deduplicate="TemplateStyles:r1129693374">.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}</style><style data-mw-deduplicate="TemplateStyles:r1236075235">.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}</style></div><div role="navigation" class="navbox" aria-labelledby="Programmable_logic" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><style data-mw-deduplicate="TemplateStyles:r1239400231">.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}</style><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:Programmable_logic" title="Template:Programmable logic"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:Programmable_logic" title="Template talk:Programmable logic"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:Programmable_logic" title="Special:EditPage/Template:Programmable logic"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="Programmable_logic" style="font-size:114%;margin:0 4em"><a href="/wiki/Programmable_logic_device" title="Programmable logic device">Programmable logic</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Concepts</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Application-specific_integrated_circuit" title="Application-specific integrated circuit">ASIC</a></li> <li><a href="/wiki/System_on_a_chip" title="System on a chip">SoC</a></li> <li><a href="/wiki/Field-programmable_gate_array" title="Field-programmable gate array">FPGA</a> <ul><li><a href="/wiki/Logic_block" title="Logic block">Logic block</a></li></ul></li> <li><a href="/wiki/Complex_programmable_logic_device" title="Complex programmable logic device">CPLD</a></li> <li><a href="/wiki/Programmable_logic_device#EPLDs" title="Programmable logic device">EPLD</a></li> <li><a href="/wiki/Programmable_logic_array" title="Programmable logic array">PLA</a></li> <li><a href="/wiki/Programmable_Array_Logic" title="Programmable Array Logic">PAL</a></li> <li><a href="/wiki/Generic_array_logic" class="mw-redirect" title="Generic array logic">GAL</a></li> <li><a href="/wiki/Cypress_PSoC" title="Cypress PSoC">PSoC</a></li> <li><a href="/wiki/Reconfigurable_computing" title="Reconfigurable computing">Reconfigurable computing</a> <ul><li><a href="/wiki/Xputer" title="Xputer">Xputer</a></li></ul></li> <li><a href="/wiki/Soft_microprocessor" title="Soft microprocessor">Soft microprocessor</a></li> <li><a href="/wiki/Circuit_underutilization" title="Circuit underutilization">Circuit underutilization</a></li> <li><a href="/wiki/High-level_synthesis" title="High-level synthesis">High-level synthesis</a></li> <li><a href="/wiki/Hardware_acceleration" title="Hardware acceleration">Hardware acceleration</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Hardware_description_language" title="Hardware description language">Languages</a></th><td class="navbox-list-with-group navbox-list navbox-even hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Verilog" title="Verilog">Verilog</a> <ul><li><a href="/wiki/Verilog-A" title="Verilog-A">A</a></li> <li><a href="/wiki/Verilog-AMS" title="Verilog-AMS">AMS</a></li></ul></li> <li><a href="/wiki/VHDL" title="VHDL">VHDL</a> <ul><li><a href="/wiki/VHDL-AMS" title="VHDL-AMS">AMS</a></li> <li><a href="/wiki/VHDL-VITAL" title="VHDL-VITAL">VITAL</a></li></ul></li> <li><a href="/wiki/SystemVerilog" title="SystemVerilog">SystemVerilog</a> <ul><li><a href="/wiki/SystemVerilog_DPI" title="SystemVerilog DPI">DPI</a></li></ul></li> <li><a href="/wiki/SystemC" title="SystemC">SystemC</a></li> <li><a href="/wiki/Altera_Hardware_Description_Language" title="Altera Hardware Description Language">AHDL</a></li> <li><a href="/wiki/Handel-C" title="Handel-C">Handel-C</a></li> <li><a href="/wiki/Lola_(computing)" title="Lola (computing)">Lola</a></li> <li><a class="mw-selflink selflink">PSL</a></li> <li><a href="/wiki/Unified_Power_Format" title="Unified Power Format">UPF</a></li> <li><a href="/wiki/PALASM" title="PALASM">PALASM</a></li> <li><a href="/wiki/Advanced_Boolean_Expression_Language" title="Advanced Boolean Expression Language">ABEL</a></li> <li><a href="/wiki/Programmable_Array_Logic#CUPL" title="Programmable Array Logic">CUPL</a></li> <li><a href="/wiki/C_to_HDL" title="C to HDL">C to HDL</a></li> <li><a href="/wiki/Flow_to_HDL" title="Flow to HDL">Flow to HDL</a></li> <li><a href="/wiki/MyHDL" title="MyHDL">MyHDL</a></li> <li><a href="/wiki/ELLA_(programming_language)" title="ELLA (programming language)">ELLA</a></li> <li><a href="/wiki/Chisel_(programming_language)" title="Chisel (programming language)">Chisel</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Companies</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Accellera" title="Accellera">Accellera</a></li> <li><a href="/wiki/Achronix" title="Achronix">Achronix</a></li> <li><a href="/wiki/AMD" title="AMD">AMD</a></li> <li><a href="/wiki/Aldec" title="Aldec">Aldec</a></li> <li><a href="/wiki/Arm_Holdings" title="Arm Holdings">Arm</a></li> <li><a href="/wiki/Cadence_Design_Systems" title="Cadence Design Systems">Cadence</a></li> <li><a href="/wiki/Infineon_Technologies" title="Infineon Technologies">Infineon</a></li> <li><a href="/wiki/Intel" title="Intel">Intel</a></li> <li><a href="/wiki/Lattice_Semiconductor" title="Lattice Semiconductor">Lattice</a></li> <li><a href="/wiki/Microchip_Technology" title="Microchip Technology">Microchip Technology</a></li> <li><a href="/wiki/NXP_Semiconductors" title="NXP Semiconductors">NXP</a></li> <li><a href="/wiki/Siemens" title="Siemens">Siemens</a></li> <li><a href="/wiki/Synopsys" title="Synopsys">Synopsys</a></li> <li><a href="/wiki/Texas_Instruments" title="Texas Instruments">Texas Instruments</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Products</th><td class="navbox-list-with-group navbox-list navbox-odd hlist" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%">Hardware</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ICE_(FPGA)" title="ICE (FPGA)">iCE</a></li> <li><a href="/wiki/Stratix" title="Stratix">Stratix</a></li> <li><a href="/wiki/Virtex_(FPGA)" title="Virtex (FPGA)">Virtex</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Software</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Intel_Quartus_Prime" title="Intel Quartus Prime">Intel Quartus Prime</a></li> <li><a href="/wiki/Xilinx_ISE" title="Xilinx ISE">Xilinx ISE</a></li> <li><a href="/wiki/Vivado" title="Vivado">Vivado</a></li> <li><a href="/wiki/ModelSim" title="ModelSim">ModelSim</a></li> <li><a href="/wiki/Verilog-to-Routing" title="Verilog-to-Routing">VTR</a></li> <li><a href="/wiki/List_of_HDL_simulators" title="List of HDL simulators">Simulators</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Intellectual_property" title="Intellectual property">Intellectual<br />property</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Proprietary_hardware" title="Proprietary hardware">Proprietary</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/ARC_(processor)" title="ARC (processor)">ARC</a></li> <li><a href="/wiki/ARM_Cortex-M" title="ARM Cortex-M">ARM Cortex-M</a></li> <li><a href="/wiki/LEON" title="LEON">LEON</a></li> <li><a href="/wiki/LatticeMico8" title="LatticeMico8">LatticeMico8</a></li> <li><a href="/wiki/MicroBlaze" title="MicroBlaze">MicroBlaze</a></li> <li><a href="/wiki/PicoBlaze" title="PicoBlaze">PicoBlaze</a></li> <li><a href="/wiki/Nios_embedded_processor" title="Nios embedded processor">Nios</a></li> <li><a href="/wiki/Nios_II" title="Nios II">Nios II</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/Open-source_hardware" title="Open-source hardware">Open-source</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/Java_Optimized_Processor" title="Java Optimized Processor">JOP</a></li> <li><a href="/wiki/LatticeMico32" title="LatticeMico32">LatticeMico32</a></li> <li><a href="/wiki/OpenCores" title="OpenCores">OpenCores</a></li> <li><a href="/wiki/OpenRISC" title="OpenRISC">OpenRISC</a> <ul><li><a href="/wiki/OpenRISC_1200" title="OpenRISC 1200">1200</a></li></ul></li> <li><a href="/wiki/Power_ISA" title="Power ISA">Power ISA</a> <ul><li><a href="/wiki/Libre-SOC" title="Libre-SOC">Libre-SOC</a></li> <li><a href="/wiki/OpenPOWER_Microwatt" title="OpenPOWER Microwatt">Microwatt</a></li></ul></li> <li><a href="/wiki/RISC-V" title="RISC-V">RISC-V</a></li> <li><a href="/wiki/Zet_(hardware)" title="Zet (hardware)">Zet</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr></tbody></table><div></div></td></tr></tbody></table></div> <div class="navbox-styles"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1236075235"></div><div role="navigation" class="navbox" aria-labelledby="IEEE_standards" style="padding:3px"><table class="nowraplinks hlist mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1129693374"><link rel="mw-deduplicated-inline-style" href="mw-data:TemplateStyles:r1239400231"><div class="navbar plainlinks hlist navbar-mini"><ul><li class="nv-view"><a href="/wiki/Template:IEEE_standards" title="Template:IEEE standards"><abbr title="View this template">v</abbr></a></li><li class="nv-talk"><a href="/wiki/Template_talk:IEEE_standards" title="Template talk:IEEE standards"><abbr title="Discuss this template">t</abbr></a></li><li class="nv-edit"><a href="/wiki/Special:EditPage/Template:IEEE_standards" title="Special:EditPage/Template:IEEE standards"><abbr title="Edit this template">e</abbr></a></li></ul></div><div id="IEEE_standards" style="font-size:114%;margin:0 4em"><a href="/wiki/IEEE_Standards_Association" title="IEEE Standards Association">IEEE standards</a></div></th></tr><tr><th scope="row" class="navbox-group" style="width:1%">Current</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE-488" class="mw-redirect" title="IEEE-488">488</a></li> <li><a href="/wiki/IEEE_693" title="IEEE 693">693</a></li> <li><a href="/wiki/Software_quality_assurance" title="Software quality assurance">730</a></li> <li><a href="/wiki/IEEE_754" title="IEEE 754">754</a> <ul><li><a href="/wiki/IEEE_754-2008_revision" title="IEEE 754-2008 revision">Revision</a></li></ul></li> <li><a href="/wiki/IEEE_854-1987" title="IEEE 854-1987">854</a></li> <li><a href="/wiki/Software_configuration_management" title="Software configuration management">828</a></li> <li><a href="/wiki/Software_test_documentation" title="Software test documentation">829</a></li> <li><a href="/wiki/Futurebus" title="Futurebus">896</a></li> <li><a href="/wiki/Single_UNIX_Specification" title="Single UNIX Specification">1003</a></li> <li><a href="/wiki/VMEbus" title="VMEbus">1014</a></li> <li><a href="/wiki/Software_design_description" title="Software design description">1016</a></li> <li><a href="/wiki/VHDL" title="VHDL">1076</a></li> <li><a href="/wiki/JTAG" title="JTAG">1149.1</a></li> <li><a href="/wiki/PILOT" title="PILOT">1154</a></li> <li><a href="/wiki/IEEE_1164" title="IEEE 1164">1164</a></li> <li><a href="/wiki/Open_Firmware" title="Open Firmware">1275</a></li> <li><a href="/wiki/Distributed_Interactive_Simulation" title="Distributed Interactive Simulation">1278</a></li> <li><a href="/wiki/IEEE_1284" title="IEEE 1284">1284</a></li> <li><a href="/wiki/IEEE_1355" title="IEEE 1355">1355</a></li> <li><a href="/wiki/IEEE_1394" title="IEEE 1394">1394</a></li> <li><a href="/wiki/IEEE_1451" title="IEEE 1451">1451</a></li> <li><a href="/wiki/Standard_Delay_Format" title="Standard Delay Format">1497</a></li> <li><a href="/wiki/High-level_architecture" class="mw-redirect" title="High-level architecture">1516</a></li> <li><a href="/wiki/IEEE_1541-2002" class="mw-redirect" title="IEEE 1541-2002">1541</a></li> <li><a href="/wiki/IEEE_1547" title="IEEE 1547">1547</a></li> <li><a href="/wiki/IEEE_1584" title="IEEE 1584">1584</a></li> <li><a href="/wiki/Precision_Time_Protocol" title="Precision Time Protocol">1588</a></li> <li><a href="/wiki/Scalable_Coherent_Interface" title="Scalable Coherent Interface">1596</a></li> <li><a href="/wiki/Advanced_Library_Format" title="Advanced Library Format">1603</a></li> <li><a href="/wiki/IEEE_1613" title="IEEE 1613">1613</a></li> <li><a href="/wiki/IEEE_1619" class="mw-redirect" title="IEEE 1619">1619</a></li> <li><a href="/wiki/SystemC" title="SystemC">1666</a></li> <li><a href="/wiki/IEEE_1667" title="IEEE 1667">1667</a></li> <li><a href="/wiki/IEEE_1675-2008" title="IEEE 1675-2008">1675</a></li> <li><a href="/wiki/IP-XACT" title="IP-XACT">1685</a></li> <li><a href="/wiki/IEEE_1722" class="mw-redirect" title="IEEE 1722">1722</a></li> <li><a href="/wiki/IEEE_1733" class="mw-redirect" title="IEEE 1733">1733</a></li> <li><a href="/wiki/SystemVerilog" title="SystemVerilog">1800</a></li> <li><a href="/wiki/Unified_Power_Format" title="Unified Power Format">1801</a></li> <li><a href="/wiki/DNP3" title="DNP3">1815</a></li> <li><a href="/wiki/IEEE_1849" title="IEEE 1849">1849</a></li> <li><a class="mw-selflink selflink">1850</a></li> <li><a href="/wiki/IEEE_1855" title="IEEE 1855">1855</a></li> <li><a href="/wiki/DySPAN" title="DySPAN">1900</a></li> <li><a href="/wiki/IEEE_1901" title="IEEE 1901">1901</a></li> <li><a href="/wiki/RuBee" title="RuBee">1902</a></li> <li><a href="/wiki/Service_Interoperability_in_Ethernet_Passive_Optical_Networks" title="Service Interoperability in Ethernet Passive Optical Networks">1904</a></li> <li><a href="/wiki/IEEE_1905" title="IEEE 1905">1905</a></li> <li><a href="/wiki/IEEE_2030" title="IEEE 2030">2030</a></li> <li><a href="/wiki/Micro_T-Kernel" title="Micro T-Kernel">2050</a></li> <li><a href="/wiki/ISO/IEEE_11073" title="ISO/IEEE 11073">11073</a></li> <li><a href="/wiki/ISO/IEC_12207" title="ISO/IEC 12207">12207</a></li> <li><a href="/wiki/Software_maintenance" title="Software maintenance">14764</a></li> <li><a href="/wiki/Risk_management" title="Risk management">16085</a></li> <li><a href="/wiki/Project_management" title="Project management">16326</a></li> <li><a href="/wiki/Requirements_engineering" title="Requirements engineering">29148</a></li> <li><a href="/wiki/ISO/IEC_42010" title="ISO/IEC 42010">42010</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802" title="IEEE 802">802 series</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"></div><table class="nowraplinks navbox-subgroup" style="border-spacing:0"><tbody><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802" title="IEEE 802">802</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_802.2" title="IEEE 802.2">.2</a></li> <li><a href="/wiki/Token_bus_network" title="Token bus network">.4</a></li> <li><a href="/wiki/Token_Ring" title="Token Ring">.5</a></li> <li><a href="/wiki/IEEE_802.6" title="IEEE 802.6">.6</a></li> <li><a href="/wiki/IEEE_802.7" title="IEEE 802.7">.7</a></li> <li><a href="/wiki/IEEE_802.8" title="IEEE 802.8">.8</a></li> <li><a href="/wiki/IEEE_802.9" title="IEEE 802.9">.9</a></li> <li><a href="/wiki/IEEE_802.10" title="IEEE 802.10">.10</a></li> <li><a href="/wiki/100BaseVG" title="100BaseVG">.12</a></li> <li><a href="/wiki/Cable_modem#IEEE_802.14" title="Cable modem">.14</a></li> <li><a href="/wiki/IEEE_802.16" title="IEEE 802.16">.16</a> <ul><li><a href="/wiki/WiMAX" title="WiMAX">WiMAX · d · e</a></li></ul></li> <li><a href="/wiki/Resilient_Packet_Ring" title="Resilient Packet Ring">.17</a></li> <li><a href="/wiki/IEEE_802.18" title="IEEE 802.18">.18</a></li> <li><a href="/wiki/IEEE_802.20" title="IEEE 802.20">.20</a></li> <li><a href="/wiki/IEEE_802.21" title="IEEE 802.21">.21</a></li> <li><a href="/wiki/IEEE_802.22" title="IEEE 802.22">.22</a></li> <li><a href="/w/index.php?title=IEEE_802.24&action=edit&redlink=1" class="new" title="IEEE 802.24 (page does not exist)">.24</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802.1" title="IEEE 802.1">802.1</a></th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_802.1D" title="IEEE 802.1D">D</a></li> <li><a href="/wiki/IEEE_P802.1p" title="IEEE P802.1p">p</a></li> <li><a href="/wiki/IEEE_802.1Q" title="IEEE 802.1Q">Q</a></li> <li><a href="/wiki/IEEE_802.1Qav" class="mw-redirect" title="IEEE 802.1Qav">Qav</a></li> <li><a href="/wiki/Stream_Reservation_Protocol" title="Stream Reservation Protocol">Qat</a></li> <li><a href="/wiki/Provider_Backbone_Bridge_Traffic_Engineering" title="Provider Backbone Bridge Traffic Engineering">Qay</a></li> <li><a href="/wiki/Data_center_bridging#IEEE_Task_Group" title="Data center bridging">Qaz</a></li> <li><a href="/wiki/IEEE_802.1Qbb" class="mw-redirect" title="IEEE 802.1Qbb">Qbb</a></li> <li><a href="/wiki/Spanning_Tree_Protocol" title="Spanning Tree Protocol">w</a></li> <li><a href="/wiki/IEEE_802.1X" title="IEEE 802.1X">X</a></li> <li><a href="/wiki/Link_Layer_Discovery_Protocol" title="Link Layer Discovery Protocol">AB</a></li> <li><a href="/wiki/IEEE_802.1ad" title="IEEE 802.1ad">ad</a></li> <li><a href="/wiki/IEEE_802.1AE" title="IEEE 802.1AE">AE</a></li> <li><a href="/wiki/IEEE_802.1ag" title="IEEE 802.1ag">ag</a></li> <li><a href="/wiki/IEEE_802.1ah-2008" class="mw-redirect" title="IEEE 802.1ah-2008">ah</a></li> <li><a href="/wiki/Multiple_Registration_Protocol" title="Multiple Registration Protocol">ak</a></li> <li><a href="/wiki/IEEE_802.1aq" title="IEEE 802.1aq">aq</a></li> <li><a href="/wiki/IEEE_802.1AS" class="mw-redirect" title="IEEE 802.1AS">AS</a></li> <li><a href="/wiki/Link_aggregation" title="Link aggregation">AX</a> (<a href="/wiki/Link_Aggregation_Control_Protocol" class="mw-redirect" title="Link Aggregation Control Protocol">LACP</a>)</li> <li><a href="/wiki/Audio_Video_Bridging" title="Audio Video Bridging">BA</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802.3" title="IEEE 802.3">802.3</a> <br />(<a href="/wiki/Ethernet" title="Ethernet">Ethernet</a>)</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/10BASE5" title="10BASE5">-1983</a></li> <li><a href="/wiki/802.3a" class="mw-redirect" title="802.3a">a</a></li> <li><a href="/wiki/802.3b" class="mw-redirect" title="802.3b">b</a></li> <li><a href="/wiki/802.3d" class="mw-redirect" title="802.3d">d</a></li> <li><a href="/wiki/802.3e" class="mw-redirect" title="802.3e">e</a></li> <li><a href="/wiki/802.3i" class="mw-redirect" title="802.3i">i</a></li> <li><a href="/wiki/802.3j" class="mw-redirect" title="802.3j">j</a></li> <li><a href="/wiki/802.3u" class="mw-redirect" title="802.3u">u</a></li> <li><a href="/wiki/IEEE_802.3x" class="mw-redirect" title="IEEE 802.3x">x</a></li> <li><a href="/wiki/802.3y" class="mw-redirect" title="802.3y">y</a></li> <li><a href="/wiki/802.3z" class="mw-redirect" title="802.3z">z</a></li> <li><a href="/wiki/802.3ab" class="mw-redirect" title="802.3ab">ab</a></li> <li><a href="/wiki/802.3ac" class="mw-redirect" title="802.3ac">ac</a></li> <li><a href="/wiki/802.3ad" class="mw-redirect" title="802.3ad">ad</a></li> <li><a href="/wiki/802.3ae" class="mw-redirect" title="802.3ae">ae</a></li> <li><b><a href="/wiki/802.3af" class="mw-redirect" title="802.3af">af</a></b></li> <li><a href="/wiki/802.3ah" class="mw-redirect" title="802.3ah">ah</a></li> <li><a href="/wiki/802.3ak" class="mw-redirect" title="802.3ak">ak</a></li> <li><a href="/wiki/802.3an" class="mw-redirect" title="802.3an">an</a></li> <li><a href="/wiki/802.3aq" class="mw-redirect" title="802.3aq">aq</a></li> <li><b><a href="/wiki/802.3at" class="mw-redirect" title="802.3at">at</a></b></li> <li><a href="/wiki/802.3au" class="mw-redirect" title="802.3au">au</a></li> <li><a href="/wiki/802.3av" class="mw-redirect" title="802.3av">av</a></li> <li><a href="/wiki/802.3az" class="mw-redirect" title="802.3az">az</a></li> <li><a href="/wiki/802.3ba" class="mw-redirect" title="802.3ba">ba</a></li> <li><b><a href="/wiki/802.3bt" class="mw-redirect" title="802.3bt">bt</a></b></li> <li><a href="/wiki/802.3bu" class="mw-redirect" title="802.3bu">bu</a></li> <li><a href="/wiki/802.3by" class="mw-redirect" title="802.3by">by</a></li> <li><a href="/wiki/802.3bz" class="mw-redirect" title="802.3bz">bz</a></li> <li><a href="/w/index.php?title=802.3ca&action=edit&redlink=1" class="new" title="802.3ca (page does not exist)">ca</a></li> <li><a href="/w/index.php?title=802.3cb&action=edit&redlink=1" class="new" title="802.3cb (page does not exist)">cb</a></li> <li><a href="/w/index.php?title=802.3cc&action=edit&redlink=1" class="new" title="802.3cc (page does not exist)">cc</a></li> <li><a href="/w/index.php?title=802.3cd&action=edit&redlink=1" class="new" title="802.3cd (page does not exist)">cd</a></li> <li><a href="/w/index.php?title=802.3ce&action=edit&redlink=1" class="new" title="802.3ce (page does not exist)">ce</a></li> <li><a href="/wiki/802.3cg" class="mw-redirect" title="802.3cg">cg</a></li> <li><a href="/wiki/802.3ch" class="mw-redirect" title="802.3ch">ch</a></li> <li><a href="/w/index.php?title=802.3ck&action=edit&redlink=1" class="new" title="802.3ck (page does not exist)">ck</a></li> <li><a href="/w/index.php?title=802.3cm&action=edit&redlink=1" class="new" title="802.3cm (page does not exist)">cm</a></li> <li><a href="/w/index.php?title=802.3cn&action=edit&redlink=1" class="new" title="802.3cn (page does not exist)">cn</a></li> <li><a href="/w/index.php?title=802.3cp&action=edit&redlink=1" class="new" title="802.3cp (page does not exist)">cp</a></li> <li><a href="/wiki/802.3cq" class="mw-redirect" title="802.3cq">cq</a></li> <li><a href="/w/index.php?title=802.3cr&action=edit&redlink=1" class="new" title="802.3cr (page does not exist)">cr</a></li> <li><a href="/w/index.php?title=802.3cs&action=edit&redlink=1" class="new" title="802.3cs (page does not exist)">cs</a></li> <li><a href="/w/index.php?title=802.3ct&action=edit&redlink=1" class="new" title="802.3ct (page does not exist)">ct</a></li> <li><a href="/w/index.php?title=802.3cu&action=edit&redlink=1" class="new" title="802.3cu (page does not exist)">cu</a></li> <li><a href="/wiki/802.3cv" class="mw-redirect" title="802.3cv">cv</a></li> <li><a href="/w/index.php?title=802.3cw&action=edit&redlink=1" class="new" title="802.3cw (page does not exist)">cw</a></li> <li><a href="/w/index.php?title=802.3cx&action=edit&redlink=1" class="new" title="802.3cx (page does not exist)">cx</a></li> <li><a href="/w/index.php?title=802.3cy&action=edit&redlink=1" class="new" title="802.3cy (page does not exist)">cy</a></li> <li><a href="/w/index.php?title=802.3cz&action=edit&redlink=1" class="new" title="802.3cz (page does not exist)">cz</a></li> <li><a href="/w/index.php?title=802.3da&action=edit&redlink=1" class="new" title="802.3da (page does not exist)">da</a></li> <li><a href="/w/index.php?title=802.3db&action=edit&redlink=1" class="new" title="802.3db (page does not exist)">db</a></li> <li><a href="/wiki/802.3dd" class="mw-redirect" title="802.3dd">dd</a></li> <li><a href="/w/index.php?title=802.3de&action=edit&redlink=1" class="new" title="802.3de (page does not exist)">de</a></li> <li><a href="/w/index.php?title=802.3df&action=edit&redlink=1" class="new" title="802.3df (page does not exist)">df</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802.11" title="IEEE 802.11">802.11</a> <br />(<a href="/wiki/Wi-Fi" title="Wi-Fi">Wi-Fi</a>)</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_802.11-1997" class="mw-redirect" title="IEEE 802.11-1997">-1997</a></li> <li><a href="/wiki/IEEE_802.11_(legacy_mode)" title="IEEE 802.11 (legacy mode)">legacy mode</a></li> <li><a href="/wiki/IEEE_802.11a-1999" title="IEEE 802.11a-1999">a</a></li> <li><a href="/wiki/IEEE_802.11b-1999" title="IEEE 802.11b-1999">b</a></li> <li><a href="/wiki/IEEE_802.11c" title="IEEE 802.11c">c</a></li> <li><a href="/wiki/IEEE_802.11d-2001" title="IEEE 802.11d-2001">d</a></li> <li><a href="/wiki/IEEE_802.11e-2005" title="IEEE 802.11e-2005">e</a></li> <li><a href="/wiki/Inter-Access_Point_Protocol" title="Inter-Access Point Protocol">f</a></li> <li><a href="/wiki/IEEE_802.11g-2003" title="IEEE 802.11g-2003">g</a></li> <li><a href="/wiki/IEEE_802.11h-2003" title="IEEE 802.11h-2003">h</a></li> <li><a href="/wiki/IEEE_802.11i-2004" title="IEEE 802.11i-2004">i</a></li> <li><a href="/wiki/IEEE_802.11j-2004" title="IEEE 802.11j-2004">j</a></li> <li><a href="/wiki/IEEE_802.11k-2008" title="IEEE 802.11k-2008">k</a></li> <li><b><a href="/wiki/IEEE_802.11n-2009" title="IEEE 802.11n-2009">n</a></b> (<a href="/wiki/Wi-Fi_4" class="mw-redirect" title="Wi-Fi 4">Wi-Fi 4</a>)</li> <li><a href="/wiki/IEEE_802.11p" title="IEEE 802.11p">p</a></li> <li><a href="/wiki/IEEE_802.11r-2008" title="IEEE 802.11r-2008">r</a></li> <li><a href="/wiki/IEEE_802.11s" title="IEEE 802.11s">s</a></li> <li><a href="/wiki/IEEE_802.11u" title="IEEE 802.11u">u</a></li> <li><a href="/wiki/IEEE_802.11v" class="mw-redirect" title="IEEE 802.11v">v</a></li> <li><a href="/wiki/IEEE_802.11w-2009" title="IEEE 802.11w-2009">w</a></li> <li><a href="/wiki/IEEE_802.11y-2008" title="IEEE 802.11y-2008">y</a></li> <li><a href="/wiki/IEEE_802.11z" class="mw-redirect" title="IEEE 802.11z">z</a></li> <li>aa</li> <li><b><a href="/wiki/IEEE_802.11ac" class="mw-redirect" title="IEEE 802.11ac">ac</a></b> (<a href="/wiki/Wi-Fi_5" class="mw-redirect" title="Wi-Fi 5">Wi-Fi 5</a>)</li> <li><a href="/wiki/IEEE_802.11ad" title="IEEE 802.11ad">ad</a> (<a href="/wiki/WiGig" title="WiGig">WiGig</a>)</li> <li>ae</li> <li><a href="/wiki/IEEE_802.11af" title="IEEE 802.11af">af</a></li> <li><a href="/wiki/IEEE_802.11ah" title="IEEE 802.11ah">ah</a></li> <li><a href="/wiki/IEEE_802.11ai" title="IEEE 802.11ai">ai</a></li> <li><a href="/wiki/IEEE_802.11aj" class="mw-redirect" title="IEEE 802.11aj">aj</a></li> <li>ak</li> <li>aq</li> <li><b><a href="/wiki/IEEE_802.11ax" class="mw-redirect" title="IEEE 802.11ax">ax</a></b> (<a href="/wiki/Wi-Fi_6" title="Wi-Fi 6">Wi-Fi 6</a>)</li> <li><a href="/wiki/IEEE_802.11ay" title="IEEE 802.11ay">ay</a></li> <li>az</li> <li>ba</li> <li><a href="/wiki/IEEE_802.11bb" title="IEEE 802.11bb">bb</a></li> <li>bc</li> <li>bd</li> <li><b><a href="/wiki/IEEE_802.11be" class="mw-redirect" title="IEEE 802.11be">be</a></b> (<a href="/wiki/Wi-Fi_7" title="Wi-Fi 7">Wi-Fi 7</a>)</li> <li>bf</li> <li>bh</li> <li>bi</li> <li>bk</li> <li><b><a href="/wiki/IEEE_802.11bn" title="IEEE 802.11bn">bn</a></b> (<a href="/w/index.php?title=Wi-Fi_8&action=edit&redlink=1" class="new" title="Wi-Fi 8 (page does not exist)">Wi-Fi 8</a>)</li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%"><a href="/wiki/IEEE_802.15" title="IEEE 802.15">802.15</a></th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_802.15.1" class="mw-redirect" title="IEEE 802.15.1">.1</a> (<a href="/wiki/Bluetooth" title="Bluetooth">Bluetooth</a>)</li> <li><a href="/wiki/IEEE_802.15.2" class="mw-redirect" title="IEEE 802.15.2">.2</a></li> <li><a href="/wiki/IEEE_802.15.3" class="mw-redirect" title="IEEE 802.15.3">.3</a></li> <li><a href="/wiki/IEEE_802.15.4" title="IEEE 802.15.4">.4</a> (<a href="/wiki/Zigbee" title="Zigbee">Zigbee</a>)</li> <li><a href="/wiki/IEEE_802.15.4a" title="IEEE 802.15.4a">.4a</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4b&action=edit&redlink=1" class="new" title="IEEE 802.15.4b (page does not exist)">.4b</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4c&action=edit&redlink=1" class="new" title="IEEE 802.15.4c (page does not exist)">.4c</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4d&action=edit&redlink=1" class="new" title="IEEE 802.15.4d (page does not exist)">.4d</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4e&action=edit&redlink=1" class="new" title="IEEE 802.15.4e (page does not exist)">.4e</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4f&action=edit&redlink=1" class="new" title="IEEE 802.15.4f (page does not exist)">.4f</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4g&action=edit&redlink=1" class="new" title="IEEE 802.15.4g (page does not exist)">.4g</a></li> <li><a href="/w/index.php?title=IEEE_802.15.4z&action=edit&redlink=1" class="new" title="IEEE 802.15.4z (page does not exist)">.4z</a></li> <li><a href="/wiki/IEEE_802.15.5" class="mw-redirect" title="IEEE 802.15.5">.5</a></li> <li><a href="/wiki/IEEE_802.15.6" title="IEEE 802.15.6">.6</a></li> <li><a href="/wiki/IEEE_802.15.7" class="mw-redirect" title="IEEE 802.15.7">.7</a></li></ul> </div></td></tr></tbody></table><div></div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Proposed</th><td class="navbox-list-with-group navbox-list navbox-odd" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_P1363" title="IEEE P1363">P1363</a></li> <li><a href="/wiki/IEEE_P1619" title="IEEE P1619">P1619</a></li> <li><a href="/wiki/Rosetta-lang" title="Rosetta-lang">P1699</a></li> <li><a href="/wiki/Universal_Power_Adapter_for_Mobile_Devices" title="Universal Power Adapter for Mobile Devices">P1823</a></li> <li><a href="/wiki/IEEE_P1906.1" title="IEEE P1906.1">P1906.1</a></li></ul> </div></td></tr><tr><th scope="row" class="navbox-group" style="width:1%">Superseded</th><td class="navbox-list-with-group navbox-list navbox-even" style="width:100%;padding:0"><div style="padding:0 0.25em"> <ul><li><a href="/wiki/IEEE_754-1985" title="IEEE 754-1985">754-1985</a></li> <li><a href="/wiki/Software_requirements_specification" title="Software requirements specification">830</a></li> <li><a href="/wiki/IEEE_1219" class="mw-redirect" title="IEEE 1219">1219</a></li> <li><a href="/wiki/Software_requirements_specification" title="Software requirements specification">1233</a></li> <li><a href="/wiki/Concept_of_operations" title="Concept of operations">1362</a></li> <li><a href="/wiki/Verilog" title="Verilog">1364</a></li> <li><a href="/wiki/IEEE_1471" title="IEEE 1471">1471</a></li></ul> </div></td></tr><tr><td class="navbox-abovebelow" colspan="2"><div> <dl><dt><i>See also</i></dt> <dd><a href="/wiki/IEEE_Standards_Association" title="IEEE Standards Association">IEEE Standards Association</a></dd> <dd><a href="/wiki/Category:IEEE_standards" title="Category:IEEE standards">Category:IEEE standards</a></dd></dl> </div></td></tr></tbody></table></div>    </div><noscript><img src="https://login.wikimedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" width="1" height="1" style="border: none; position: absolute;"></noscript> <div class="printfooter" data-nosnippet="">Retrieved from "<a dir="ltr" href="https://en.wikipedia.org/w/index.php?title=Property_Specification_Language&oldid=1237719664">https://en.wikipedia.org/w/index.php?title=Property_Specification_Language&oldid=1237719664</a>"</div></div> <div id="catlinks" class="catlinks" data-mw="interface"><div id="mw-normal-catlinks" class="mw-normal-catlinks"><a href="/wiki/Help:Category" title="Help:Category">Categories</a>: <ul><li><a href="/w/index.php?title=Category:Pages_using_the_JsonConfig_extension&action=edit&redlink=1" class="new" title="Category:Pages using the JsonConfig extension (page does not exist)">Pages using the JsonConfig extension</a></li><li><a href="/wiki/Category:Hardware_verification_languages" title="Category:Hardware verification languages">Hardware verification languages</a></li><li><a href="/wiki/Category:Formal_specification_languages" title="Category:Formal specification languages">Formal specification languages</a></li><li><a href="/wiki/Category:IEEE_DASC_standards" title="Category:IEEE DASC standards">IEEE DASC standards</a></li><li><a href="/wiki/Category:IEC_standards" title="Category:IEC standards">IEC standards</a></li></ul></div></div> </div> </main> </div> <div class="mw-footer-container"> <footer id="footer" class="mw-footer" > <ul id="footer-info"> <li id="footer-info-lastmod"> This page was last edited on 31 July 2024, at 04:44<span class="anonymous-show"> (UTC)</span>.</li> <li id="footer-info-copyright">Text is available under the <a href="/wiki/Wikipedia:Text_of_the_Creative_Commons_Attribution-ShareAlike_4.0_International_License" title="Wikipedia:Text of the Creative Commons Attribution-ShareAlike 4.0 International License">Creative Commons Attribution-ShareAlike 4.0 License</a>; additional terms may apply. By using this site, you agree to the <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Terms_of_Use" class="extiw" title="foundation:Special:MyLanguage/Policy:Terms of Use">Terms of Use</a> and <a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy" class="extiw" title="foundation:Special:MyLanguage/Policy:Privacy policy">Privacy Policy</a>. Wikipedia® is a registered trademark of the <a rel="nofollow" class="external text" href="https://wikimediafoundation.org/">Wikimedia Foundation, Inc.</a>, a non-profit organization.</li> </ul> <ul id="footer-places"> <li id="footer-places-privacy"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Privacy_policy">Privacy policy</a></li> <li id="footer-places-about"><a href="/wiki/Wikipedia:About">About Wikipedia</a></li> <li id="footer-places-disclaimers"><a href="/wiki/Wikipedia:General_disclaimer">Disclaimers</a></li> <li id="footer-places-contact"><a href="//en.wikipedia.org/wiki/Wikipedia:Contact_us">Contact Wikipedia</a></li> <li id="footer-places-wm-codeofconduct"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Universal_Code_of_Conduct">Code of Conduct</a></li> <li id="footer-places-developers"><a href="https://developer.wikimedia.org">Developers</a></li> <li id="footer-places-statslink"><a href="https://stats.wikimedia.org/#/en.wikipedia.org">Statistics</a></li> <li id="footer-places-cookiestatement"><a href="https://foundation.wikimedia.org/wiki/Special:MyLanguage/Policy:Cookie_statement">Cookie statement</a></li> <li id="footer-places-mobileview"><a href="//en.m.wikipedia.org/w/index.php?title=Property_Specification_Language&mobileaction=toggle_view_mobile" class="noprint stopMobileRedirectToggle">Mobile view</a></li> </ul> <ul id="footer-icons" class="noprint"> <li id="footer-copyrightico"><a href="https://wikimediafoundation.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/static/images/footer/wikimedia-button.svg" width="84" height="29" alt="Wikimedia Foundation" loading="lazy"></a></li> <li id="footer-poweredbyico"><a href="https://www.mediawiki.org/" class="cdx-button cdx-button--fake-button cdx-button--size-large cdx-button--fake-button--enabled"><img src="/w/resources/assets/poweredby_mediawiki.svg" alt="Powered by MediaWiki" width="88" height="31" loading="lazy"></a></li> </ul> </footer> </div> </div> </div> <div class="vector-settings" id="p-dock-bottom"> <ul></ul> </div><script>(RLQ=window.RLQ||[]).push(function(){mw.config.set({"wgHostname":"mw-web.codfw.main-f69cdc8f6-b78pt","wgBackendResponseTime":147,"wgPageParseReport":{"limitreport":{"cputime":"0.352","walltime":"0.426","ppvisitednodes":{"value":2296,"limit":1000000},"postexpandincludesize":{"value":79514,"limit":2097152},"templateargumentsize":{"value":2649,"limit":2097152},"expansiondepth":{"value":8,"limit":100},"expensivefunctioncount":{"value":32,"limit":500},"unstrip-depth":{"value":0,"limit":20},"unstrip-size":{"value":42594,"limit":5000000},"entityaccesscount":{"value":0,"limit":400},"timingprofile":["100.00% 302.509 1 -total"," 43.82% 132.563 6 Template:Cite_book"," 41.17% 124.530 5 Template:Navbox"," 38.22% 115.609 1 Template:Programmable_Logic"," 8.41% 25.446 54 Template:Mono"," 6.03% 18.231 54 Template:Ifsubst"," 3.12% 9.425 19 Template:Code"," 2.89% 8.742 1 Template:IEEE_standards"]},"scribunto":{"limitreport-timeusage":{"value":"0.199","limit":"10.000"},"limitreport-memusage":{"value":3530104,"limit":52428800}},"cachereport":{"origin":"mw-api-int.codfw.main-6d49cf5db8-x57z8","timestamp":"20241025232039","ttl":2592000,"transientcontent":false}}});});</script> <script type="application/ld+json">{"@context":"https:\/\/schema.org","@type":"Article","name":"Property Specification Language","url":"https:\/\/en.wikipedia.org\/wiki\/Property_Specification_Language","sameAs":"http:\/\/www.wikidata.org\/entity\/Q751505","mainEntity":"http:\/\/www.wikidata.org\/entity\/Q751505","author":{"@type":"Organization","name":"Contributors to Wikimedia projects"},"publisher":{"@type":"Organization","name":"Wikimedia Foundation, Inc.","logo":{"@type":"ImageObject","url":"https:\/\/www.wikimedia.org\/static\/images\/wmf-hor-googpub.png"}},"datePublished":"2004-06-28T21:03:43Z","dateModified":"2024-07-31T04:44:08Z"}</script> </body> </html>