skip to main content
research-article

Automata-based assertion-checker synthesis of PSL properties

Published: 06 February 2008 Publication History

Abstract

Assertion-based verification with languages such as PSL is gaining in importance. From assertions, one can generate hardware assertion checkers for use in emulation, simulation acceleration and silicon debug. We present techniques for checker generation of the complete set of PSL properties, including all variants of operators, both strong and weak. A full automata-based approach allows an entire assertion to be represented by a single automaton, hence allowing optimizations that can not be done in a modular approach where subcircuits are created only for individual operators. For this purpose, automata algorithms are developed for the base cases, and a complete set of rewrite rules is derived for other operators. Automata splitting is introduced for an efficient implementation of the eventually! operator.

References

[1]
Abarbanel, Y., Beer, I., Glushovsky, L., Keidar, S., and Wolfsthal, Y. 2000. FoCs: Automatic generation of simulation checkers from formal specifications. Conference on Computer Aided Verification. 538--542.
[2]
Borrione, D., Liu, M., Morin-Allory, K., Ostier, P., and Fesquet, L. 2005. Online assertion-based verification with proven correct monitors. In Proceedings of the 3rd ITI International Conference on Information & Communications Technology (ICICT). 123--143.
[3]
Boulé, M., Chenard, J., and Zilic, Z. 2006. Adding debug enhancements to assertion checkers for hardware emulation and silicon debug. In Proceedings of the 24th IEEE International Conference on Computer Design (ICCD). 294--299.
[4]
Boulé, M. and Zilic, Z. 2006. Efficient automata-based assertion-checker synthesis of PSL properties. In Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT). 69--76.
[5]
Boulé, M. and Zilic, Z. 2007. Efficient automata-based assertion-checker synthesis of SEREs for hardware emulation. In Proceedings of the 12th Asia and South Pacific Design Automation Conference (ASP-DAC). 324--329.
[6]
Claessen, K. and Martensson, J. 2004. An operational semantics for weak PSL. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD). 337--351.
[7]
Cohen, B., Venkataramanan, S., and Kumari, A. 2004. Using PSL/Sugar for formal and dynamic verification. VhdlCohen Publishing, Los Angeles, CA.
[8]
Das, S., Mohanty, R., Dasgupta, P., and Chakrabarti, P. 2006. Synthesis of system verilog assertions. In Proceedings of the Conference on Design Automation and Test in Europe (DATE). 70--75.
[9]
Foster, H., Krolnik, A., and Lacey, D. 2004. Assertion-Based Design, 2nd Ed. Kluwer Academic Publishers.
[10]
Gheorghita, S. and Grigore, R. 2005. Constructing checkers from PSL properties. In Proceedings of the 15th International Conference on Control Systems and Computer Science (CSCS) 2, 757--762.
[11]
Gordon, M., Hurd, J., and Slind, K. 2003. Executing the formal semantics of the accelera property specification language by mechanised theorem proving. Lecture Notes in Computer Science, vol. 2860, 200--215.
[12]
Hopcroft, J., Motwani, R., and Ullman, J. 2000. Introduction to Automata Theory, Languages and Computation, 2nd Ed. Addison-Wesley.
[13]
IBM AlphaWorks. 2006. FoCs Property Checkers Generator, version 2.04. www.alphaworks. ibm.com/tech/FoCs.
[14]
IEEE Std. 1850. 2005. IEEE Standard for Property Specification Language (PSL). Institute of Electrical and Electronic Engineers, Inc., New York, NY.
[15]
Morin-Allory, K. and Borrione, D. 2006a. Online monitoring of properties built on regular expression sequences. Forum on Specification Design Languages (FDL).
[16]
Morin-Allory, K. and Borrione, D. 2006b. Proven correct monitors from PSL specifications. In Proceedings of the Conference on Design Automation and Test in Europe (DATE). 1246--1251.
[17]
Ziv, A. 2003. Cross-product functional coverage measurement with temporal properties-based assertions. In Proceedings of the Conference on Design Automation and Test in Europe (DATE), 834--839.

Cited By

View all
  • (2024)Exploring the Abyss? Unveiling Systems-on-Chip Hardware Vulnerabilities Beneath SoftwareIEEE Transactions on Information Forensics and Security10.1109/TIFS.2024.337280019(3914-3926)Online publication date: 4-Mar-2024
  • (2024)SCARF: Securing Chips With a Robust Framework Against Fabrication-Time Hardware TrojansIEEE Transactions on Computers10.1109/TC.2024.344908273:12(2761-2775)Online publication date: Dec-2024
  • (2024)Efficient Offline Monitoring for Dynamic Metric Temporal LogicRuntime Verification10.1007/978-3-031-74234-7_8(128-149)Online publication date: 14-Oct-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Design Automation of Electronic Systems
ACM Transactions on Design Automation of Electronic Systems  Volume 13, Issue 1
January 2008
496 pages
ISSN:1084-4309
EISSN:1557-7309
DOI:10.1145/1297666
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

Publication History

Published: 06 February 2008
Accepted: 01 July 2007
Revised: 01 May 2007
Received: 01 May 2006
Published in TODAES Volume 13, Issue 1

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Assertion-Based Verification
  2. PSL
  3. assertion checkers
  4. automata
  5. emulation
  6. hardware

Qualifiers

  • Research-article
  • Research
  • Refereed

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)47
  • Downloads (Last 6 weeks)2
Reflects downloads up to 15 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)Exploring the Abyss? Unveiling Systems-on-Chip Hardware Vulnerabilities Beneath SoftwareIEEE Transactions on Information Forensics and Security10.1109/TIFS.2024.337280019(3914-3926)Online publication date: 4-Mar-2024
  • (2024)SCARF: Securing Chips With a Robust Framework Against Fabrication-Time Hardware TrojansIEEE Transactions on Computers10.1109/TC.2024.344908273:12(2761-2775)Online publication date: Dec-2024
  • (2024)Efficient Offline Monitoring for Dynamic Metric Temporal LogicRuntime Verification10.1007/978-3-031-74234-7_8(128-149)Online publication date: 14-Oct-2024
  • (2024)faRM-LTL: A Domain-Specific Architecture for Flexible and Accelerated Runtime Monitoring of LTL PropertiesRuntime Verification10.1007/978-3-031-74234-7_7(109-127)Online publication date: 14-Oct-2024
  • (2023)SoC Protocol Implementation Verification Using Instruction-Level Abstraction SpecificationsACM Transactions on Design Automation of Electronic Systems10.1145/361029228:6(1-24)Online publication date: 16-Oct-2023
  • (2022)The Future of FPGA Acceleration in Datacenters and the CloudACM Transactions on Reconfigurable Technology and Systems10.1145/350671315:3(1-42)Online publication date: 4-Feb-2022
  • (2022)Runtime Monitoring of c-LTL Specifications on FPGAs Using HLS2022 18th International Conference on Synthesis, Modeling, Analysis and Simulation Methods and Applications to Circuit Design (SMACD)10.1109/SMACD55068.2022.9816308(1-4)Online publication date: 12-Jun-2022
  • (2022)Reusing Verification Assertions as Security Checkers for Hardware Trojan Detection2022 23rd International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED54688.2022.9806292(1-6)Online publication date: 6-Apr-2022
  • (2022)Network-on-Chip Trust Validation Using Security AssertionsJournal of Hardware and Systems Security10.1007/s41635-022-00129-56:3-4(79-94)Online publication date: 7-Dec-2022
  • (2021)SoC Trust Validation Using Assertion-Based Security Monitors2021 22nd International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED51717.2021.9424363(496-503)Online publication date: 7-Apr-2021
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media