A Practical Introduction to PSL (Hardcover)

Description

This book describes the Property Specification Language PSL, recently standardized as IEEE Standard 1850-2005. PSL was developed to fulfill the following requirements: easy to learn, write, and read; concise syntax; rigorously well-defined formal semantics; expressive power, permitting the specification for a large class of real world design properties; known efficient underlying algorithms in simulation, as well as formal verification. Basic features are covered, as well as advanced topics such as the use of PSL in multiply-clocked designs. A full chapter is devoted to common errors, gathered through the authors' many years of experience in using and teaching the language.

 

Foreword.- Preface.- Introduction.- Basic Temporal Properties.- Some Philosophy.- Weak vs. Strong Temporal Operators.- SERE Style.- Clocks.- Aborting a Property.- Some Convenient Constructs.- The Simple Subset.- The Boolean, Modeling and Verification Layers.- Advanced Topics.- More Philosophy -- High vs. Low Level Assertions.- Common Errors.- Mulitply-clocked Designs.- Syntax Rule Summary.- Formal Syntax and Semantics.- Operator Precedence.- Quick Reference.- Bibliographic Notes.- References.- Index.

描述

本書介紹了最近作為IEEE標準1850-2005標準化的屬性規範語言PSL。PSL的開發是為了滿足以下要求：易於學習、書寫和閱讀；簡潔的語法；嚴格明確的形式語義；表達能力強，可以規範大量現實世界的設計屬性；在模擬和形式驗證中具有已知的高效底層算法。本書涵蓋了基本功能，以及高級主題，如在多時鐘設計中使用PSL。全書的一個章節專門介紹了常見的錯誤，這些錯誤是作者多年使用和教授該語言的經驗所積累的。

目錄

前言- 前言- 簡介- 基本時間屬性- 一些哲學- 弱對強時間運算符- SERE風格- 時鐘- 中止屬性- 一些方便的構造- 簡單子集- 布爾、建模和驗證層- 高級主題- 更多哲學- 高級對低級斷言- 常見錯誤- 多時鐘設計- 語法規則摘要- 形式語法和語義- 運算符優先順序- 快速參考- 參考文獻- 索引。