For the most recent entries see the Petri Nets Newsletter.

Verification of bounded delay asynchronous circuits with timed traces.

Yoneda, T.; Zhou, B.; Schlingloff, B.-H.

In: Lecture Notes in Computer Science, Vol. 1548: Algebraic Methodology and Software Technology, pages 59-73. Springer-Verlag, 1999.

Abstract: This paper extends the verification method based on the failure semantics of process algebra and the resulting trace theory by Dill at al. for bounded delay asynchronous circuits. A timed conformance relation between trace structures is defined which allows to express both safety and responsiveness properties. In the proposed approach, bounded delay circuits as well as their real-time properties are modeled by time Petri nets. An explicit state exploration algorithm is given to determine whether an implementation conforms to a specification. Since for IO conflict-free specification the conformance relation is transitive, this algorithm can be used for hierarchical verification of large asynchronous circuits. The paper describes the implementation of the proposed method and gives some experimental results which demonstrate its efficiency.

Keywords: asynchronous circuits, conformance checking, delay analysis, failure analysis, hardware verification, real-time systems, time Petri nets, timed traces.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography