Project Details

Přibližná ekvivalence pro aproximativní počítání

Project Period: 1. 1. 2016 – 31. 12. 2018

Project Type: grant

Code: GA16-17538S

Agency: Czech Science Foundation

Program: Standardní projekty

English title
Relaxed equivalence checking for approximate computing
Type
grant
Keywords

approximate computing; genetic programming; evolvable hardware; relaxed equivalence checking; automata; logic

Abstract

Approximate 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.

Team members
Vojnar Tomáš, prof. Ing., Ph.D. (DITS) – research leader
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Sekanina Lukáš, prof. Ing., Ph.D. (DCSY)
Vašíček Zdeněk, doc. Ing., Ph.D. (DCSY)
Publications

2019

  • 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

2018

  • 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
  • Č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
  • 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
  • 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. 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
  • 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
  • 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
  • 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

2017

  • Č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
  • Č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
  • Č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
  • Č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
  • 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
  • FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 407-425. ISBN: 978-3-662-54576-8. ISSN: 0302-9743. 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
  • MINAŘÍK, M.; SEKANINA, L. On Evolutionary Approximation of Sigmoid Function for HW/SW Embedded Systems. In 20th European Conference on Genetic Programming, EuroGP 2017. Lecture Notes in Computer Science. Berlin: Springer International Publishing, 2017. p. 343-358. ISBN: 978-3-319-55696-3. Detail
  • MRÁZEK, V.; HRBÁČEK, R.; VAŠÍČEK, Z.; SEKANINA, L. EvoApprox8b: Library of Approximate Adders and Multipliers for Circuit Design and Benchmarking of Approximation Methods. In Proc. of the 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE). Lausanne: European Design and Automation Association, 2017. p. 258-261. ISBN: 978-3-9815370-9-3. 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
  • 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
  • VAŠÍČEK, Z.; MRÁZEK, V.; SEKANINA, L. Towards Low Power Approximate DCT Architecture for HEVC Standard. In Proc. of the 2017 Design, Automation & Test in Europe Conference & Exhibition (DATE). Lausanne: European Design and Automation Association, 2017. p. 1576-1581. ISBN: 978-3-9815370-9-3. Detail

2016

  • ABATE, A.; ČEŠKA, M.; KWIATKOWSKA, M. Approximate Policy Iteration for Markov Decision Processes via Quantitative Adaptive Aggregations. In Proceedings of 14th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2016. p. 13-31. ISBN: 978-3-319-46519-7. Detail
  • CHEN, Y.; HSIEH, C.; LENGÁL, O.; LII, T.; TSAI, M.; WANG, B.; WANG, F. PAC Learning-Based Verification and Model Synthesis. In Proceedings of the 38th International Conference on Software Engineering. Austin, TX: Association for Computing Machinery, 2016. p. 714-724. ISBN: 978-1-4503-3900-1. Detail
  • DVOŘÁČEK, P.; SEKANINA, L. Evolutionary Approximation of Edge Detection Circuits. In 19th European Conference on Genetic programming. Lecture Notes in Computer Science. Berlin: Springer International Publishing, 2016. p. 19-34. ISBN: 978-3-319-30667-4. 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
  • HRBÁČEK, R.; MRÁZEK, V.; VAŠÍČEK, Z. Automatic Design of Approximate Circuits by Means of Multi-Objective Evolutionary Algorithms. In Proceedings of the 11th International Conference on Design & Technology of Integrated Systems in Nanoscale Era. Istanbul: Istanbul Sehir University, 2016. p. 239-244. ISBN: 978-1-5090-0335-8. Detail
  • MRÁZEK, V.; VAŠÍČEK, Z. Automatic Design of Arbitrary-Size Approximate Sorting Networks with Error Guarantee. In Power and Timing Modeling, Optimization and Simulation (PATMOS), 2016 26rd International Workshop on. Bremen: Institute of Electrical and Electronics Engineers, 2016. p. 221-228. ISBN: 978-1-5090-0733-2. Detail
  • SEKANINA, L.; KAPUSTA, V. Visualisation and Analysis of Genetic Records Produced by Cartesian Genetic Programming. In GECCO'16 Companion. New York: Association for Computing Machinery, 2016. p. 1411-1418. ISBN: 978-1-4503-4323-7. Detail
  • VAŠÍČEK, Z.; MRÁZEK, V.; SEKANINA, L. Evolutionary Functional Approximation of Circuits Implemented into FPGAs. In 2016 IEEE Symposium Series on Computational Intelligence. Athens: Institute of Electrical and Electronics Engineers, 2016. p. 1-8. ISBN: 978-1-5090-4240-1. Detail
  • VAVERKA, F.; HRBÁČEK, R.; SEKANINA, L. Evolving Component Library for Approximate High Level Synthesis. In 2016 IEEE Symposium Series on Computational Intelligence. Athens: IEEE Computational Intelligence Society, 2016. p. 1-8. ISBN: 978-1-5090-4240-1. Detail
Back to top