Automatic Extraction of Non-Iterated System Behavior from Verilog Specifications

In this paper we present an algorithm for automatic extraction of system behavior from a structural Verilog specification. The algorithm generates a series-parallel poset expression for the behavior of the system, which is then used for verification purposes in the context of the SPPV Formal Verification Environment. The issues of correctness and time complexity of the algorithm are briefly discussed. A small example is presented to illustrate the conversion process from specification to a series-parallel poset expression.

• Type: Conference
• Year: 2004
• Where: CSREAESA
• Authors: Lubomir Ivanov
• Keywords: CSREAESA 2004, CSREAESA 2007, Series-parallel Poset Expression, SPPV Formal Verification, Structural Verilog Specification