<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE article PUBLIC "-//TaxonX//DTD Taxonomic Treatment Publishing DTD v0 20100105//EN" "../../nlm/tax-treatment-NS0.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:tp="http://www.plazi.org/taxpub" article-type="research-article" dtd-version="3.0" xml:lang="en">
  <front>
    <journal-meta>
      <journal-id journal-id-type="publisher-id">109</journal-id>
      <journal-id journal-id-type="index">urn:lsid:arphahub.com:pub:3dc5f44e-8666-58db-bc76-a455210e8891</journal-id>
      <journal-title-group>
        <journal-title xml:lang="en">JUCS - Journal of Universal Computer Science</journal-title>
        <abbrev-journal-title xml:lang="en">jucs</abbrev-journal-title>
      </journal-title-group>
      <issn pub-type="ppub">0948-695X</issn>
      <issn pub-type="epub">0948-6968</issn>
      <publisher>
        <publisher-name>Journal of Universal Computer Science</publisher-name>
      </publisher>
    </journal-meta>
    <article-meta>
      <article-id pub-id-type="doi">10.3217/jucs-009-02-0120</article-id>
      <article-id pub-id-type="publisher-id">27931</article-id>
      <article-categories>
        <subj-group subj-group-type="heading">
          <subject>Research Article</subject>
        </subj-group>
        <subj-group subj-group-type="scientific_subject">
          <subject>B.8.1 - Reliability</subject>
          <subject> Testing</subject>
          <subject> and Fault-Tolerance</subject>
          <subject>I.6.6 - Simulation Output Analysis</subject>
        </subj-group>
      </article-categories>
      <title-group>
        <article-title>Optimized Temporal Logic Compilation</article-title>
      </title-group>
      <contrib-group content-type="authors">
        <contrib contrib-type="author" corresp="yes">
          <name name-style="western">
            <surname>Krebs</surname>
            <given-names>Andreas</given-names>
          </name>
          <email xlink:type="simple">wsi@krebs-net.de</email>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
        <contrib contrib-type="author" corresp="no">
          <name name-style="western">
            <surname>Ruf</surname>
            <given-names>Jürgen</given-names>
          </name>
          <xref ref-type="aff" rid="A1">1</xref>
        </contrib>
      </contrib-group>
      <aff id="A1">
        <label>1</label>
        <addr-line content-type="verbatim">University of Tübingen, Tübingen, Germany</addr-line>
        <institution>University of Tübingen</institution>
        <addr-line content-type="city">Tübingen</addr-line>
        <country>Germany</country>
      </aff>
      <author-notes>
        <fn fn-type="corresp">
          <p>Corresponding author: Andreas Krebs (<email xlink:type="simple">wsi@krebs-net.de</email>).</p>
        </fn>
        <fn fn-type="edited-by">
          <p>Academic editor: </p>
        </fn>
      </author-notes>
      <pub-date pub-type="collection">
        <year>2003</year>
      </pub-date>
      <pub-date pub-type="epub">
        <day>28</day>
        <month>02</month>
        <year>2003</year>
      </pub-date>
      <volume>9</volume>
      <issue>2</issue>
      <fpage>120</fpage>
      <lpage>137</lpage>
      <uri content-type="arpha" xlink:href="http://openbiodiv.net/E3A21577-01C8-5D20-AEE4-052ACF156303">E3A21577-01C8-5D20-AEE4-052ACF156303</uri>
      <uri content-type="zenodo_dep_id" xlink:href="https://zenodo.org/record/6996276">6996276</uri>
      <permissions>
        <copyright-statement>Andreas Krebs, Jürgen Ruf</copyright-statement>
        <license license-type="creative-commons-attribution" xlink:href="" xlink:type="simple">
          <license-p>This article is freely available under the J.UCS Open Content License.</license-p>
        </license>
      </permissions>
      <abstract>
        <label>Abstract</label>
        <p>Verification and validation are the major tasks during the design of digital hardware/software systems. Often more than 70% of the development time is spent for locating and correcting errors in the design. Therefore, many techniques have been developed to support the debugging process. Recently, simulation and test methods have been accompanied by formal methods such as equivalence checking and property checking. However, their industrial applicability is currently restricted to small or medium sized designs or to a specific phase in the design process. Therefore, simulation is still the most commonly applied verification technique.  In this paper, we present a method for asserting temporal properties during simulation and also during emulation of hardware prototypes. The properties under verification are efficiently translated into an intermediate language (of a virtual machine). This intermediate representation can then be interpreted during simulation. We may also produce executable checkers running in parallel to the simulation. Furthermore, we are able to translate the properties into synthesizable hardware modules which can then be used during system emulation on FPGA-based emulators or as self test components checking the functionality during the lifetime of the system.</p>
      </abstract>
    </article-meta>
  </front>
</article>
