Detail

Formal Methods for Approximate Computing in Arithmetic Circuits and Hardware-Accelerated Network Traffic Filtering

The talk covers two recent results where formal methods were used to approximate different computing tasks. Namely, we start with a presentation of an approach that combines genetic algorithms and formal verification to obtain approximations of arithmetic circuits (multipliers, adders, multiply-accumulate circuits, etc.) that trade some precision for a much smaller size and power consumption of the circuits. Such approximate circuits are very well suitable for various tasks (e.g., in data mining, image filtering, or machine learning) where exact computations are not needed. Still, it is usually good if the error stays within some bounds, which the use of formal methods can guarantee. In the second part of the talk, we will briefly touch upon another application of formal methods for approximate computing. In this case, we will speak about approximate reduction of non-deterministic finite automata used in hardware-accelerated network traffic filtering (aimed, e.g., at filtering out network attacks). For the price of changing the language of the automata, the proposed approach can squeeze the size of the automata much more than classical language-preserving reductions. Consequently, it is possible to use the current FPGA technology for FPGA-accelerated filtering at speeds of 100–400 Gbps while keeping the misclassification ratio rather low on real traffic.

The talk is based on the following papers and it is a result of collaboration with the co-authors of these papers:

* M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished. In Proc. of 36th International Conference On Computer Aided Design—ICCAD’17, IEEE CS, 2017. A bronze medal in the 2018 Human-Competitive Awards: “Humies”.

* M. Ceska, V. Havlena, L. Holik, O. Lengal, and T. Vojnar. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. In Proc. of 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems—TACAS’18, LNCS 10806, Springer-Verlag, 2018.

* M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, and T. Vojnar. ADAC: Automated Design of Approximate Circuits. Inn Proc. of 30th International Conference on Computer Aided Verification—CAV’18, LNCS 10981, Springer-Verlag, 2018.