Analyzing WMSOL Definable Properties on Sum-Like Weighted Labeled Trees

Modern software and hardware designs are mostly hierarchical. Moreover, while the design specification is defined up-down, the design implementation and verification are done down-up. In such a case, as a rule, coverage properties for simulation-based verification are defined inconsistently for different stages of the design flow. The fact leads to the well known explosion of bug rate, when we pass from the lower design stage to the upper one. In this paper, we propose a new approach that allows propagation of quantitative properties from the upper stage of the design flow to the lower ones and their incremental computation on the components. The approach may be applied to any design, modeled as a Finite State Machine (FSM) or other formalisms, which eventually lead to weighted labeled trees. We use Weighted Monadic-Second Order Logic (WMSOL) to describe the desired families of quantitative properties and sum-like weighted labeled trees to describe the decomposition of the behaviour of the FSM. The last notion is based on a generalization of disjoint unions of structures with additional links between the components. Our approach shows how computation of a quantitative property, definable as a WMSOL formula on the upper stage of the design may be reduced for certain cost to incremental computations of effectively derivable WMSOL-definable properties on the components. We provide several examples of families of such properties and discuss different aspects, related to the applicability of our approach. The approach is new and provides a uniform theoretical basis for analyzing WMSOL-definable properties on hierarchical structures.