Formal descriptions, semantics and verification of VLSI array processors

The authors present two description languages for specifying algorithms and describing implementations in ARREST - a diagram environment for VLSI array architectures. They then define their operational semantics based on feedback products of sequential machines, which provide a precise and intuitive meaning of concurrency and composition. Next the authors develop a formal specification language based on modal functions for describing the behavior of abstract product machines, which formally interprets both of the languages defined before and provides the basis for formal verification in ARREST. Finally, they classify the correctness and equivalence properties to be verified, define eight important types of equivalence, and discuss their relations with the stuttering-equivalence in the semantics