SynPSL: Behavioral Synthesis of PSL Assertions

Florian Eibensteiner, Rainer Leonhard Findenig, Markus Pfaff

Research output: Chapter in Book/Report/Conference proceedingsConference contribution

4 Citations (Scopus)

Abstract

The effort of verifying state-of-the-art hardware designs undeviatingly increases with the complexity of those designs. The design's state space, directly related to its complexity, grows exponentially, while the computational performance for verifying the design grows only linearly. This so-called verification gap can, for example, be met by using methods such as assertion-based verification (ABV), which can be used for both specifying the system's properties as well as verifying the relating implementation during simulation phase. In this paper, we present an open-source tool which generates synthesizable HDL code from assertions specified in the Property Specification Language (PSL). This is done by first reducing the PSL formulas into base cases, called PSLmin, and then generating automata which can be transformed to synthesizable HDL code and therefore into hardware.
Original languageEnglish
Title of host publicationComputer Aided Systems Theory, EUROCAST 2009 - 12th International Conference, Revised Selected Papers
Pages69-74
Number of pages6
DOIs
Publication statusPublished - 2009
EventTwelve International Conference on Computer Aided Systems Theory 2009 - Las Palmas, Spain
Duration: 15 Feb 200920 Feb 2009
http://www.iuctc.ulpgc.es/spain/eurocast2009/index.html

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5717 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceTwelve International Conference on Computer Aided Systems Theory 2009
CountrySpain
CityLas Palmas
Period15.02.200920.02.2009
Internet address

Keywords

  • Assertion-based verification
  • PSL
  • Synthesis

Fingerprint Dive into the research topics of 'SynPSL: Behavioral Synthesis of PSL Assertions'. Together they form a unique fingerprint.

Cite this