Logical Correctness by Construction

A novel methodological approach to the design of large-scale-integrated systems proposed correctness by construction. By using a restricted repertoire of admissible combination rules, it is possible to guarantee that only designs suitable for implementation are generated. This paper addresses the complementary issue of logical correctness by construction - prohibiting "meaningless" constructs from occurring. The presented approach is based on defining "meaning" in terms of a catalog of standard operators. Admissible compositions are restricted so that only constructs belonging to this catalog may be generated. This approach is mainly intended for the data-path of digital systems. There, repetitive and regular compositions provide a suitable environment for using catalogs of operators. The paper focuses on the description of operators relevant to the design at Register Transfer Level. Manipulation rules are used for describing their properties. Rules basic to logical correctness by construction are shown to be: contractions, expansions and transformations into canonical forms.