Wyniki 1-7 spośród 7 dla zapytania: authorDesc:"Andrzej Pułka"

Strategia weryfikacji systemu na chipie oparta na mechaniźmie FDL

Czytaj za darmo! »

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 etradycyjnejf 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[...]

An effective SAT-Solving mechanism with backtrack controlled by FDL


  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[...]

Generacja cykli fundamentalnych metodą dynamicznego budowania drzewa grafu

Czytaj za darmo! »

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[...]

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

Czytaj za darmo! »

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[...]

Timing analysis of multitask systems in SystemC environment


  Hardware Description Languages (HDLs) have been developed for several years in the field of electronic design automation and tools based on them gave new abilities to designers. However today, when the complexity of design problems grows exponentially every year, these tools seem to be not sufficient. Now engineers needs tools working on higher levels of abstraction allowing modeling of the entire system i.e. without initial, manual partitioning it into the hardware and software [1]. The terms of system level design, codesign and co-simulation have been well recognized and defined for several years now [2] and new tools: SystemC [3, 4] and SystemVerilog [5, 6] have appeared since the beginning of the 21st century. The approach presented within the paper is based on SystemC language, a tool that combines HDL with programming language and supports many new techniques of communication modeling. SystemC has been proposed by OSCI group [4] as a natural extension of the object-oriented programming language C++ supporting the system level specification language demands [1]. SystemC combines two design domains: hardware and software within a single environment. It defines many communication and synchronization issues (timers, mutexes, semaphores, FIFOs) that are very useful in system level modeling. SystemC introduces also abstract term: the model of computation (MoC) [11], which means that each module can have various (different) implementations within the model. The working group of the SystemC - WG OSCI [1] unified the modeling methodology and suggested transaction level modeling technique (TLM). This modeling philosophy (TLM) has been introduced by Cai and Gajski [7] and it divides the entire design process into small tasks. The term “transaction" within the embedded electronic system is defined as: “the exchange of data or an event between two components of a modeled and simulated system". Moreover, because the detai[...]

Synteza i implementacja układu sterowania w strukturze FPGA opisanego językiem SFC zgodnego z IEC61131 DOI:10.15199/ELE-2014-213


  Sterownik programowalny PLC jest komputerem przemysłowym używanym od wczesnych lat 70 XX wieku. Został on zaprojektowany w celu zastąpienia przekaźnikowych systemów sterowania. Dzięki rozwojowi i standaryzacji języków programowania budowa systemów sterowania uległa istotnemu uproszczeniu. Realizacja programu sterowania ma charakter szeregoweo-cyklicznego przetwarzania instrukcji [5, 7]. Jest to istotnym czynnikiem ograniczającym wydajność, podczas gdy wiele fragmentów programu sterowania nie jest wzajemnie zależnych i może zostać wykonane w sposób równoległy [2, 10]. A. Alternatywna koncepcja implementacji sterownika Technologia FPGA umożliwia dokonanie oceny własności złożonych dedykowanych układów obliczeniowych i przetwarzających takich jak sterowniki PLC. Prowadzone badania [2] pozwoliły wprowadzić znaczące udoskonalenia w architekturze jednostek centralnych PLC, wykorzystując w niewielkim stopniu sprzętowe zrównoleglenie wykonywanych operacji (np. jednostki dwurdzeniowe bitowo-bajtowe). Bardziej pożądanym rozwiązaniem jest przeprowadzenie pełnej syntezy sprzętowego układu sterowania charakteryzującego się równoległym przetwarzaniem programu. Wykorzystuje się tutaj możliwość programowego dostosowania architektury sprzętowej układu FPGA. Złożoność procesu implementacji wymaga zbudowania narzędzi automatycznych dla standardowych języków programowania [7]. Poprzednie implementacje kompilatorów dokonywały bezpośredniej zamiany konstrukcji językowych na elementy sprzętowe. Prowadziło to do niezgodności odpowiedzi, która została zauważona w kilku pracach np. [6, 10]. Próbę jej rozwiązania ograniczono jedynie do operacji logicznych. Implementacja operacji arytmetycznych wymaga rozwiązania zagadnień związanych z kolejnością przetwarzania oraz ograniczonymi zasobami sprzętowymi dostępnymi w układzie [6]. W pracy [3] zaproponowano dokonanie kompilacji programu sterowania do opisu w języku C, przekazywanego do komercyjnie dostęp[...]

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

Czytaj za darmo! »

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[...]

 Strona 1