Verification of logical descriptions with functional indeterminacy

• Autorzy: Cheremisinova L.

Warianty tytułu

PL

Weryfikacja specyfikacji logicznych z indeterminizmem funkcjonalnym

• Języki publikacji: EN

Abstrakty

EN

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.

PL

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.

Słowa kluczowe

EN

design automation; formal verification; simulation

PL

automatyzacja projektowania; formalna weryfikacja; symulacja

• Wydawca: Wydawnictwo PAK
• Czasopismo: Pomiary Automatyka Kontrola
• Rocznik: 2012
• Tom: R. 58, nr 6
• Strony: 519--513
• Opis fizyczny: Bibliogr. 11 poz., rys., wzory

Twórcy

autor

Cheremisinova L.

• The United Institute of Informatics Problems of NAS of Belarus, ul. Surganova 6, 220012 Minsk,

Bibliografia

• [1] Cheremisinova L., Novikov D.: International Journal “Information Theories & Applications”. FOI ITHEA, Bulgaria, V. 15, No. 3, 2008.
• [2] Cheremisinova L. D., Novikov D. Ya.: Proceedings of the NAS of Belarus, physical-technical series, Minsk, No 2, 2009 (in Russian).
• [3] Kunz W., Marques Silva J., Malik S.: Logic synthesis and Verification (Ed. S. Hassoun, T. Sasao and R. K.Brayton). Kluwer Academic Publishers, 2002.
• [4] The MiniSat Page / http://minisat.se/MiniSat.html
• [5] Cheremisinova L., Novikov D.: Proceedings of 8th Intern. Workchop on Boolean problems, Freiberg (Sachsen), Sept. 18-19, 2008.
• [6] Cheremisinova L., Novikov D.: Proc. of IEEE East-West Design and Test Symposium (EWDTS’09), Moscow, Russia, Sept. 18-21, 2009.
• [7] Cheremisinova L., Novikov D.: International book series “Information science and computing”. FOI ITHEA, Bulgaria, No. 15, 2009.
• [8] Cheremisinova L. D., Novikov D. Ya.: Automatic Control and Computer Sciences. Allerton Press, Inc., Vol. 44, No. 1, 2010.
• [9] Novikov D. Ya., Cheremisinova L. D.: Informatika. The United Institute of Informatics Problems of NAS of Belarus, No. 3, 2010 (in Russian).
• [10] Cheremisinova L., Novikov D.: Proc. of 9th Int.. Workshop on Boolean problems, Freiberg (Sachsen), Sept. 16-17, 2010.
• [11] Cheremisinova L. D., Novikov D. Ya.: Automatic Control and Computer Sciences, Allerton Press, Inc., Vol. 45, No. 4, 2011.