This paper defines a quantitative metric of the completeness of a formal specification. A "good" (formal) specification is already needed in the beginning of the development process to prevent cost-intensive corrections of errors found in the late phases of a design process. A quantitative analysis method is presented to evaluate whether a specification is "good". The method considers only the formal specification, an implementation (design) is not necessary. Thus, an analysis of a specification can be directly done. The properties of the specification are transformed into a normal form to calculate the metric. Experimental results of the analysis method are given, e. g., metrics for specifications of the AMBA AHB bus.

Assertions are advocated as a means to specify high-level models of a design. Assertions are translated into executable behavioral models ("cando-objects"). The cando-objects reflect the intended non-determinism of assertions as well as the non-determinism caused by the incompleteness of a set of assertions. The approach supports significant design methodological concepts like refinement and compositionality.

A method for the fully automatic equivalence verification of a design before and after the scheduling step of high-level synthesis is presented. The technique is applicable to the results of advanced scheduling methods like AFAP and DLS, which work on cyclic control flows, as well as to pipelined designs.

The problem of the optimization of complex data-paths relative to a repertoire of specified operations is discussed.Data-paths can be simplified if interconnections are functionally redundant.Redundancy is detected by means of the universal quantification of ROBDD representations of the data-path and of the specified operations.The full logical complexity of ALU's described at the gate-level is considered.A O-1 ILP formulation of the minimization problem is given and solved by means of ROBDD 's.A solution of the prelogic rectification problem for control-signals is present ed.