Verification of logical descriptions with functional indeterminacy
Liudmila D. Cheremisinova · Pomiary Automatyka Kontrola · 2012
Streszczenie W artykule omowiono problem sprawdzania, czy dany ukad cz eś ciowo okre ślonych funkcji Boole'owskich jest realizowany przez specyfikacj e logiczn ą z indeterminizmem funkcjonalnym, ktora jest przedstawiona jako system po¯ączonych blokow, z ktorych ka zdy odpowiada ukadowi ca¯- kiem albo cz eś ciowo okre ślonych funkcji Boole'owskich. Rozpatrzono metod e symulacyjn ą i metod e, bazującą na analizie spenialno ści funkcji. Pierwsza z tych metod symuluje struktur e, opisan ą przez drug ą specyfikacje, w dziedzinie pierwszej specyfikacji. Druga metoda s prowadza problem weryfikacji do problemu spenialno ści funkcji w postaci iloczynu sum. Przedstawiono wyniki komputerowych bada n skuteczno ści zaproponowa- nych metod. Sowa kluczowe : automatyzacja projektowania, weryfikacja, symulacja. Abstract 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 r epresented by a system of connected blocks each of which is specified by a system of completely or incompletely specified Boolean functions. Simula tion based and SAT based verification methods are considered. The firs t methods simulate the structure specified by the second description on th e domain of the first description. The second methods formulate the verif ication problem as checking satisfiability of a conjunctive normal for m. The results of com- puter investigation of the proposed methods are giv en.