|
|
|
|
| LEADER |
03315nam a2200229uu 4500 |
| 005 |
20190305105423.0 |
| 008 |
s2006 ci a |||||||||| ||hrv|d |
| 035 |
|
|
|a HR-ZaFER 34183
|
| 040 |
|
|
|a HR-ZaFER
|b hrv
|c HR-ZaFER
|e ppiak
|
| 041 |
|
|
|a hrv
|
| 080 |
|
|
|a 681.3.06
|j SOFTVER
|9 1783
|
| 100 |
1 |
|
|9 31034
|a Grudenić, Igor
|
| 245 |
|
|
|a Paralelni algoritmi izgradnje i manipulacije binarnim dijagramima odlučivanja :
|b magistarski rad /
|c Igor Grudenić ; [mentor Nikola Bogunović]
|
| 260 |
|
|
|a Zagreb :
|b I. Grudenić ; Fakultet elektrotehnike i računarstva,
|c 2006.
|
| 300 |
|
|
|a II, 107 str. :
|b ilustr. ;
|c 30 cm +
|e CD
|
| 504 |
|
|
|a Bibliografija str. 97-101.
|
| 520 |
|
|
|a Binarni dijagrami odlučivanja (BDD) dijagrami omogućavaju učinkovit prikaz i formalnu verifikaciju digitalnih sustava. Postoje razne heuristike za optimizaciju formalne verifikacije BDD dijagramima. Jedan od načina za poboljšanje efikasnosti formalne verifikacije temeljene na BDD dijagramima je raspodijeljena izgradnja i manipulacija BDD dijagramima. Prednost raspodijeljene izgradnje BDD dijagrama leži u većoj procesorskoj snazi i većoj količini raspoloživog memorijskog prostora. Magistarski rad opisuje raspodijeljeni algoritam izgradnje i manipulacije BDD dijagramima namijenjen sustavu umreženih računala zasnovan na kombiniranom pristupu izgradnje BDD dijagrama. U radu je prikazana arhitektura i neki od detalja implementacije programskog ostvarenja tog algoritma. Mjerenja učinkovitosti algoritma provedena su izgradnjom BDD prikaza digitalnog množila i zbrajala zbog njihovog karakterističnog BDD prikaza. Mjerenja su izvedena na grozdu računala i dvoprocesorskom sustavu. U radu je dodatno analiziran utjecaj ostvarene priručne memorije na učinkovitost raspodijeljene izgradnje BDD dijagrama.
Ključne riječi:
Binarni dijagrami odlučivanja, paralelni algoritam, simbolička provjera modela, formalna verifikacija
|
| 520 |
|
|
|a Binary decision diagrams (BDDs) are data structures that enable efficient representation and formal verification of digital systems. There are different heuristics that can be employed in order to optimize BDD based formal verification process. In particular, distributed BDD construction and manipulation can be used to make formal verification of digital systems more efficient. The distribution benefits from additional CPU power and larger memory address space. The thesis describes distributed algorithm for BDD manipulation based on combined breadth-first and depth-first BDD construction techniques. The algorithm is targeted for execution on network of workstations. The implementation of algorithm is also given paying great attention to details. The measurement of the distributed BDD creation performance is accomplished by building BDD representation of digital adder and digital multiplier. These circuits are used because of the specific characteristics of their BDD representations. Performance of distributed algorithm is measured using two processor system and a computer cluster. Special analysis on performance impact of distributed computed cache is also given.
Keywords:
Binary Decision diagrams, parallel algorithm, symbolic model checking, formal verification
|
| 700 |
|
|
|4 ths
|9 9941
|a Bogunović, Nikola
|
| 942 |
|
|
|c M
|2 udc
|
| 990 |
|
|
|a 31978
|
| 999 |
|
|
|c 29783
|d 29783
|