Verification of logical descriptions with functional indeterminacy

The problem under discussion is to check whether a given system of incompletely specified Boolean functions is implemented by a logical description with functional indeterminacy that is represented by a system of connected blocks. Each of blocks is specified by a system of completely or incompletely specified Boolean functions. Simulation based and SAT based verification methods is considered. The first method simulates the structure specified by the second description on the domain of the first description. The second method formulates the verification problem as checking satisfiability of a conjunctive normal form. The results of computer investigation of the proposed methods are given.

W artykule omówiono problem sprawdzania, czy dany układ częściowo określonych funkcji Boole'owskich jest realizowany przez specyfikację logiczną z indeterminizmem funkcjonalnym. Ta specyfikacja jest przedstawiona jako system połączonych bloków, z których każdy odpowiada układowi całkiem albo częściowo określonych funkcji Boole'owskich. Rozpatrzono metodę symulacyjną i metodę bazującą na analizie spełnialności funkcji. Pierwsza z tych metod symuluje strukturę, opisaną przez drugą specyfikację, w dziedzinie pierwszej specyfikacji. Druga metoda sprowadza problem weryfikacji do problemu spełnialności funkcji w postaci iloczynu sum. Przedstawiono wyniki komputerowych badań skuteczności zaproponowanych metod.