English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

This paper presents the main principles for building a symbolic transition system from a description written in a subset of VHDL'87 (temporal information is excluded and objects are restricted to bit, bit_vector and Boolean types). This transition system is used for formal verification of the VHDL description. It consist of a system of Boolean equations indicating the next state of the system in terms of its current state. It is automatically generated from an intermediate representation of the VHDL description by means of a Petri Net. The deterministic nature of VHDL 87 and the exclusion of temporal elements in the description permit us to abstract the behavior of the system: only one state per delta cycle is represented instead of all intermediate states encountered in simulation. This abstraction reduces the size of the transition system and the cost of subsequent analysis. The construction of the system of Boolean equations from the Petri Net is presented first, and then an example of verification of a temporal logic property illustrates its use for Symbolic Model Checking. Experimental results are given which demonstrate the feasibility of this approach.

A symbolic relation for a subset of VHDL'87 descriptions and its application to symbolic model checking