ANDRZEJ PUŁKA- zobacz i pobierz wszystkie publikacje autora ANDRZEJ PUŁKA w naszych czasopismach

Wyniki 1-5 spośród 5 dla zapytania: authorDesc:"ANDRZEJ PUŁKA"

» Strategia weryfikacji systemu na chipie oparta na mechaniźmie FDL

Proces projektowania z.o.onych, nowoczesnych elektronicznych systemow wbudowanych wymaga zastosowania wielu nowych, efektywnych technik oraz metod pozwalaj.cych na zredukowanie czasu oraz zweryfikowanie koncepcji projektowych na wczesnych etapach produkcji. Te techniki wymagaj. stosowania abstrakcyjnych modeli systemu, tzw. modeli systemowych. Od wspo.czesnego in.yniera elektronika wymaga si., aby by. sprawnym programist., ktory zna zasady pracy systemow operacyjnych na rowni ze sprz.tem. Modele z.o.onych systemow powinny by. precyzyjne czasowo i funkcjonalnie, a wi.c projektanci musz. mie. dost.p do odpowiednich, wyrafinowanych narz.dzi pozwalaj.cych zweryfikowa. jako.. projektu. Niniejsza publikacja dotyczy zagadnienia modelowania i weryfikacji z.o.onych systemow cyfrowych (SoC). W dziedzinie weryfikacji formalnej istnieje bardzo wiele metod, podej.. i narz.dzi [1.5] oraz [9], ktore nieustannie ewoluuj. wraz z rozwojem narz.dzi i standardow automatycznego projektowania [8] oraz [12]. Jak ju. wspomniano istnieje wiele technik weryfikacji formalnej, niektore opieraj. si. na metodach sztucznej inteligencji [2], inne bazuj. na metodach formalnych (Transformation- Based Verification, Temporal Logic, SAT Solvers, BDDs [6], Constraint Programming [5]), technikach modelowania (Timed Automata, assercje, PSL, ATPG, SystemVerilog [12] lub SystemC Verification Standard [8]). Pewna grupa metod korzysta z wynikow symulacji; natomiast inna grupa metod jest bli.sza klasycznej etradycyjnejf definicji problemu, tzn. stara si. w sposob formalny dowie.. (w matematycznym lub logicznym sensie), .e zaproponowana implementacja spe.nia opis wej.ciowy i ..dan. funckcjonalno... Jednak, gdy stopie. skomplikowania systemu ro.nie, musimy stosowa. kombinacje ro.nych metod [6]. Abstrakcyjne modele z.o.onych systemow W z.o.onych systemach cyfrowych, ca.kowita weryfikacja wszystkich mo.liwych stanow nie jest mo.liwa w rozs.dnym (realnym) prz[...] więcej»
w zeszycie ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA 2010/12

KUP TERAZ » KUP TERAZ (SMS) »

» An effective SAT-Solving mechanism with backtrack controlled by FDL

Andrzej Pułka

The problem of Boolean satisfiability (SAT) has been recognized since the beginning of logical circuits existence and belongs to one of the most studied issues in the field of combinatorial search and minimization as well as Artificial Intelligence problems. Many works devoted to SAT solvers [1, 2, 5-8, 10, 11], i.e. methods and algorithms for solving the Boolean satisfiablity tasks bore fruits in practical applications as packages embedded into Electronic Design Automation (EDA) tools. Sat solvers are commonly used for testing in automated test patterns generators [13]. The presented paper introduces some modifications to existing approaches in a for of a new original SAT-solving algorithm supported with optimal selection of variables and backtrack search controlling mechanisms based on the technique borrowed from AI - fuzzy default logic (FDL). Problem description and related works The problem of Boolean satisfiability (SAT) can be formulated as follows: verify and prove that there exists (or does not exist) an assignment (of variables) for a given Boolean function F for which the function is satisfied (evaluates to true). Usually a SAT task belongs to NP-complete problems and its solving is not trivial. The problem specification Usually the SAT problems are presented in standard conjunctive normal form (CNF), i.e. as a conjunction of clauses Ci, where every clause is given as a disjunction of literals. Each literal comprises the elementary logical unit of a given Boolean function F (problem), being merely an instance of a variable or its complement. Formally, for a given Boolean function F(x1,…, xN) of variables X = {x1, ¬x1,…, xN, ¬xN} (where symbol ¬xi denotes the complemented variable), we can express the function F in CNF form as: (1) The main advantage of such a formulation (CNF) of the problem is the practical meaning (reduction) of SAT. In order to prove the satisfiability of a given CNF[...] więcej»
w zeszycie ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA 2011/12

KUP TERAZ » KUP TERAZ (SMS) »

» Generacja cykli fundamentalnych metodą dynamicznego budowania drzewa grafu

ANDRZEJ PUŁKA

ŁUKASZ GOLLY

Wyszukiwanie minimalnych cykli fundamentalnych jest mocno związane z analizą układów elektronicznych i elektrycznych [8], jak również z ich testowaniem [6]. Podstawowym problemem przy wyznaczaniu takich cykli jest określenie odpowiedniego drzewa grafu. Zgodnie z zależnością Cayleya ilość możliwych drzew w grafie o k węzłach osi k k-2. Przeanalizowanie wszystkich możliwych drzew, a następnie sprawdzenie, który zbiór cykli fundamentalnych zawiera najmniejszą liczbę gałęzi przy grafach o dużej liczbie gałęzi, mogłoby trwać bardzo długo, a w niektórych przypadkach stać się nie możliwe. W literaturze znane są podejścia, w których wyszukuje się optymalne drzewo grafu poprzez zastosowanie algorytmów DFS(deep-first search) [1], BFS (breadth-first search) [3], and MS (mixed search) [2]. Interesująca modyfikacją algorytmu BFS z heurystycznym wyborem kolejnego wierzchołka została przedstawiona w [4]. Kolejne ciekawe podejście polegające na zamianie gałęzi drzewa z gałęziami łączącymi przedstawiono w [7]. Prezentowany algorytm nie opiera się na znajdowaniu optymalnego drzewa grafu a na dopasowaniu struktury drzewa do zestawu najmniejszych cykli. Proponowany algorytm Niech G = (V, E) będzie grafem nieskierowanym zawierającym n gałęzi i k węzłów. Definiujemy drzewo grafu jako podgraf T grafu G, który jest acyklicznym grafem zawierającym k-1 gałęzi zwanych gałęziami drzewa. Dołożenie dowolnej gałęzi ze zbioru G\T (gałęzie łączące) spowoduje, że pod-graf T będzie zawierał dokładnie jeden cykl. Cyklem fundamentalnym nazywamy zbiór cykli zawierających dokładnie jedną gałąź łączącą i dowolną liczbę gałęzi drzewa. Liczba cykli fundamentalnych wynosi n-k+1. Zdefiniowano także dwa dodatkowe pojęcia gałęzie charakterystyczne i gałęzie nadmiarowe. Gałęzie charakterystyczne to zbiór gałęzi unikalnych dla danego cyklu (nie występują w żadnym innym cyklu). Gałęzie nadmiarowe to zbiór gałęzi określonych jako różnica pomiędzy sumą gałęzi w wyznaczon[...] więcej»
w zeszycie ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA 2010/12

KUP TERAZ » KUP TERAZ (SMS) »

» Dynamiczna rekonfiguracja wątków w systemach czasu rzeczywistego pracujących w warunkach pełnej powtarzalności czasowej

ANDRZEJ PUŁKA

ADAM MILIK

Du.a konkurencja na rynku z.o.onych, elektronicznych systemow wbudowanych wymusza na producentach stosowania coraz to nowych rozwi.za.. Rosn.ce oczekiwania odbiorcow s. rownie. czynnikiem stymuluj.cym rozwoj rynku producentow takich systemow. Jednym z najistotniejszych wska.nikow jest ca.kowita wydajno.. systemu, jednak.e bardzo cz.sto du.e znaczenie ma powtarzalno.. i przewidywalno.. czasowa systemu. Zaprezentowany artyku. rozwa.a zagadnienia takiej powtarzalno.ci czasowej i prezentuje odpowiednie rozwi.zania architektoniczne systemu wielozadaniowego. Zasadnicze za.o.enia systemow PRET Systemy czasu rzeczywistego wprowadzaj. wiele wymaga. i ogranicze. czasowych: zadania musz. by. wykonywane w .ci.le okre.lonej kolejno.ci oraz w dok.adnych chwilach czasu. Cz.sto mowimy, .e zadania musz. by. realizowane wed.ug dok.adnego harmonogramu. Ide. systemow wbudowanych typu PRET (ang. Precision Time Machines), o przewidywalnej i powtarzalnej charakterystyce czasowej wprowadzili po raz pierwszy Edwards i Lee [7]. Idea PRET jest punktem wyj.cia dla autorow niniejszej pracy, ktorzy zaproponowali architektur. systemu wielozadaniowego spe.niaj.cego za.o.enie przewidywalno.ci czasowej. Oryginalne rozwi.zanie wprowadzone na Uniwersytecie Berkeley [8] zawieraj.ce, tzw. przeplot w.tkow [1] zosta.o zmodyfikowane i usprawnione dzi.ki wprowadzeniu dodatkowych rozwi.za.. Problem przewidywalno.ci i powtarzalno.ci czasowej nie jest zagadnieniem nowym i by. ju. szeroko analizowany w literaturze .wiatowej. Wprowadzenie procesorow RISC o zredukowanej li.cie rozkazow [2] i przetwarzania potokowego [1] przyczyni.o si. do przy.pieszenia czasow przetwarzania nowoczesnych systemow cyfrowych. W pracy [3] rozwa.ono analiz. najgorszego przypadku zastosowa. opartych na architekturach typu RISC. Thiele i Wilhelm [4] sformu.owali wiele wskazowek dla tworcow systemow programowo-sprz.towych, wskazuj.c na wspo.zale.no.. wielu zagadnie., aspektow i poziomow reprez[...] więcej»
w zeszycie ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA 2010/12

KUP TERAZ » KUP TERAZ (SMS) »

» Analiza efektywności i kosztów sprzętowej realizacji filtrów cyfrowych o zadanej liniowej charakterystyce fazowej

ADAM MILIK

ANDRZEJ PUŁKA

JACEK KONOPACKI

Jedną z pierwszych decyzji, jaką należy podjąć projektując filtr cyfrowy jest wybór typu filtru, tzn. czy ma to być filtr o nieskończonej odpowiedzi impulsowej (NOI), czy filtr o skończonej odpowiedzi impulsowej (SOI). O tym, która struktura zostanie ostatecznie wybrana, powinny decydować jej szczególne właściwości (wady i zalety), zwykle związane z konkretną aplikacją. W ostatnim czasie można zaobserwować, że filtry SOI są chętniej stosowane od filtrów NOI. Decydują o tym takie zalety filtrów SOI, jak: łatwość uzyskania liniowej charakterystyki fazowej oraz stabilność filtru. Ich główna wada, jaką jest większa liczba współczynników w porównaniu z odpowiednikiem typu NOI, traci w wielu przypadkach na znaczeniu, gdyż dostępne dziś maszyny cyfrowe (procesory sygnałowe) charakteryzują się bardzo dużą wydajnością obliczeniową, a czas wykonywania operacji mnożenia i dodawania jest praktycznie taki sam. Nowoczesne metody projektowania filtrów NOI pozwalają również otrzymać w przybliżeniu liniową charakterystykę fazową, ale uzyskuje się to kosztem zwiększenia rzędu filtru. W rezultacie sumaryczna liczba operacji mnożenia oraz dodawania potrzebna do wyliczenia jednej próbki wyjściowej takiego filtru (definiowana jako złożoność obliczeniowa) jest w niektórych przypadkach podobna jak dla filtrach SOI. W pracach [2, 3] porównano teoretycznie złożoność obliczeniową algorytmów realizujących wybrane filtry cyfrowe. Porównanie przeprowadzono dla filtrów o równomiernie falistej lub quasirównofalistej aproksymacji pożądanej charakterystyki częstotliwościowej, zrealizowanych za pomocą struktury bezpośredniej typu SOI lub NOI. Pokazano, że dla filtrów NOI, opisanych transmitancją o niewielkiej liczbie niezerowych biegunów, istnieje graniczna wartość szerokości pasma przejściowego (ωt), dla której złożoność obliczeniowa algorytmów realizujących filtry NOI jest mniejsza niż dla odpowiedników SOI. Rys. 1. Kaskadowa struktura typu SOI złożona[...] więcej»
w zeszycie ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA 2010/9

KUP TERAZ » KUP TERAZ (SMS) »

Strona 1

r e k l a m a