Přístupnostní navigace
E-application
Search Search Close
Project detail
Duration: 1.1.2016 — 31.12.2018
Funding resources
Grantová agentura České republiky - Standardní projekty
- part funder (1. 1. 2016 - 31. 12. 2018)
On the project
Přibližné počítání je velmi slibným přístupem k vývoji energeticky úsporných výpočetních systémů. Využívá se při něm skutečnosti, že v řadě aplikací je možno tolerovat jistou chybu výsledků. Otevřeným problémem zůstává, jak efektivně vyvíjet aproximace systémů, které by byly dobrým kompromisem mezi mírou chybovosti, spotřebou a výkonem. Použití evolučního návrhu vedlo v této oblasti k prvním slibným výsledkům, ale naráží na problém se škálovatelností při vyhodnocování kandidátních řešení. K řešení tohoto problému, který označujeme jako ověřování přibližné shody, navrhujeme nový přístup: využití pokročilých technik formální verifikace zvlášť upravených k rychlému výpočtu vzdálenosti mezi kandidátními a referenčními řešeními. Projekt směřuje k následujícím přínosům: (1) návrh efektivních algoritmů pro ověřování přibližné shody kombinačních (bezestavových) i sekvenčních (stavových) systémů, (2) návrh aproximačních algoritmů založených na genetickém programování a na vyvinutých algoritmech ověřování přibližné shody a (3) experimentální vyhodnocení navržených metod.
Description in EnglishApproximate computing is a promising approach to obtain energy-efficient computer systems. It exploits the fact that many applications are error resilient, i.e., do not require a perfect output to be produced. An open problem is how to effectively obtain approximations that are good compromises between the error ratio, power consumption, and performance. Using evolutionary algorithms for the approximation has led to promising results, but it suffers from scalability problems in evaluating candidate solutions. For that, we propose a novel way: using advanced methods of formal verification redesigned to quickly calculate distances between candidate approximations and the reference implementation, which we call relaxed equivalence checking. The project seeks the following original contributions: (1) efficient algorithms for relaxed equivalence checking of combinational (stateless) and sequential (stateful) systems, (2) approximation algorithms based on genetic programming using the proposed relaxed equivalence checking, (3) experimental evaluation of the proposed approximation methods.
Keywords aproximativní počítání; genetické programování; vyvíjející se hardware; ověřování přibližné shody; automaty; logika
Key words in Englishapproximate computing; genetic programming; evolvable hardware; relaxed equivalence checking; automata; logic
Mark
GA16-17538S
Default language
Czech
People responsible
Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsibleHolík Lukáš, doc. Mgr., Ph.D. - fellow researcherLengál Ondřej, Ing., Ph.D. - fellow researcherRogalewicz Adam, doc. Mgr., Ph.D. - fellow researcherSekanina Lukáš, prof. Ing., Ph.D. - fellow researcherVašíček Zdeněk, doc. Ing., Ph.D. - fellow researcher
Units
Department of Intelligent Systems- responsible department (24.3.2015 - 31.12.2018)Department of Computer Systems- co-beneficiary (24.3.2015 - 31.12.2018)Department of Intelligent Systems- beneficiary (24.3.2015 - 31.12.2018)
Results
FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. arXiv:1701.06282: 2017. p. 0-0.Detail
ČEŠKA, M.; CALINESCU, R.; GERASIMOU, S.; KWIATKOWSKA, M.; PAOLETTI, N. Recent Advances in Designing Robust Probabilistic Systems. 2nd International Workshop on Design and Analysis of Robust Systems (Extended Abstract). Berlin: 2017. p. 1-3.Detail
HOLÍK, L.; LENGÁL, O.; ROGALEWICZ, A.; SEKANINA, L.; VAŠÍČEK, Z.; VOJNAR, T. Towards Formal Relaxed Equivalence Checking in Approximate Computing Methodology. 2nd Workshop on Approximate Computing (WAPCO 2016). Prague: 2016. p. 1-6.Detail
HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca: 2018. p. 1-23.Detail
HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata. In Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2018. p. 109-125. ISBN: 978-3-030-01089-8. ISSN: 0302-9743.Detail
CALINESCU, R.; ČEŠKA, M.; GERASIMOU, S.; KWIATKOWSKA, M.; PAOLETTI, N. Efficient Synthesis of Robust Models for Stochastic Systems. JOURNAL OF SYSTEMS AND SOFTWARE, 2018, vol. 2018, no. 143, p. 140-158. ISSN: 0164-1212.Detail
WIGLASZ, M.; SEKANINA, L. Cooperative Coevolutionary Approximation in HOG-based Human Detection Embedded System. In 2018 IEEE Symposium Series on Computational Intelligence (SSCI 2018). Bengaluru: Institute of Electrical and Electronics Engineers, 2018. p. 1313-1320. ISBN: 978-1-5386-9276-9.Detail
SEKANINA, L.; VAŠÍČEK, Z.; MRÁZEK, V. Automated Search-Based Functional Approximation for Digital Circuits. In Approximate Circuits - Methodologies and CAD. Heidelberg: Springer International Publishing, 2019. p. 175-203. ISBN: 978-3-319-99322-5.Detail
MRÁZEK, V.; VAŠÍČEK, Z.; SEKANINA, L.; JIANG, H.; HAN, J. Scalable Construction of Approximate Multipliers With Formally Guaranteed Worst Case Error. IEEE Trans. on VLSI Systems., 2018, vol. 26, no. 11, p. 2572-2576. ISSN: 1063-8210.Detail
MRÁZEK, V.; VAŠÍČEK, Z. Evolutionary Design of Large Approximate Adders Optimized for Various Error Criteria. In Proceedings of the Genetic and Evolutionary Computation Conference Companion (GECCO '18). Kyoto: Association for Computing Machinery, 2018. p. 294-295. ISBN: 978-1-4503-5764-7.Detail
HUSA, J.; KALKREUTH, R. A Comparative Study on Crossover in Cartesian Genetic Programming. In Genetic Programming 21st European Conference, EuroGP 2018, Proceedings. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2018. p. 203-219. ISBN: 978-3-319-77553-1. ISSN: 0302-9743.Detail
MRÁZEK, V.; VAŠÍČEK, Z.; HRBÁČEK, R. Role of circuit representation in evolutionary design of energy-efficient approximate circuits. IET Computers and Digital Techniques, 2018, vol. 2018, no. 4, p. 139-149. ISSN: 1751-8601.Detail
ČEŠKA, M.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proceedings of TACAS'18. Lecture Notes in Computer Science. Thessaloniki: Springer Verlag, 2018. p. 155-175. ISSN: 0302-9743.Detail
ČEŠKA, M.; CALINESCU, R.; GERASIMOU, S.; KWIATKOWSKA, M.; PAOLETTI, N. RODES: A Robust-Design Synthesis Tool for Probabilistic Systems. In Proceedings of 14th International Conference on Quantitative Evaluation of SysTems. Heidelberg: Springer Verlag, 2017. p. 304-308. ISBN: 978-3-319-66335-7.Detail
ČEŠKA, M.; CARDELLI, L.; FRANZLE, M.; KWIATKOWSKA, M.; LAURENTI, L.; PAOLETTI, N.; WHITBY, M. Syntax-Guided Optimal Synthesis for Chemical Reaction Networks. In Proceedings of the 29th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 375-395. ISBN: 978-3-319-63390-9.Detail
LENGÁL, O.; VOJNAR, T.; ENEA, C.; SIGHIREANU, M. Compositional Entailment Checking for a Fragment of Separation Logic. FORMAL METHODS IN SYSTEM DESIGN, 2017, vol. 2017, no. 51, p. 575-607. ISSN: 0925-9856.Detail
SEKANINA, L.; VAŠÍČEK, Z.; MRÁZEK, V. Approximate Circuits in Low-Power Image and Video Processing: The Approximate Median Filter. Radioengineering, 2017, vol. 26, no. 3, p. 623-632. ISSN: 1210-2512.Detail
ČEŠKA, M.; MATYÁŠ, J.; MRÁZEK, V.; VAŠÍČEK, Z.; SEKANINA, L.; VOJNAR, T. Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In Proceedings of 36th IEEE/ACM International Conference On Computer Aided Design (ICCAD). Irvine, CA: Institute of Electrical and Electronics Engineers, 2017. p. 416-423. ISBN: 978-1-5386-3093-8.Detail
VAŠÍČEK, Z. Relaxed equivalence checking: a new challenge in logic synthesis. In Proceedings 2017 IEEE 20th International Symposium on Design and Diagnotics of Electronic Circuit & Systems. Dresden: IEEE Computer Society, 2017. p. 1-6. ISBN: 978-1-5386-0472-4.Detail
ČEŠKA, M.; CALINESCU, R.; GERASIMOU, S.; KWIATKOWSKA, M.; PAOLETTI, N. Designing Robust Software Systems through Parametric Markov Chain Synthesis. In Proceedings of 14th IEEE International Conference On Software Architecture. New Jersey: IEEE Computer Society, 2017. p. 131-140. ISBN: 978-1-5090-5729-0.Detail
Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.