The Experts below are selected from a list of 5631 Experts worldwide ranked by ideXlab platform
Sofiène Tahar - One of the best experts on this subject based on the ideXlab platform.
-
Formalization of Fixed-Point Arithmetic in HOL
Formal Methods in System Design, 2005Co-Authors: Behzad Akbarpour, Sofiène Tahar, Abdelkader DekdoukAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic. We encoded the Fixed-Point number system and specified the different quantization modes in Fixed-Point Arithmetic such as the directed and even quantization modes. We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the quantized result after carrying out basic Arithmetic operations, such as addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from floating-Point to Fixed-Point algorithmic level in the signal processing design flow.
-
modeling systemc Fixed Point Arithmetic in hol
International Conference on Formal Engineering Methods, 2003Co-Authors: Behzad Akbarpour, Sofiène TaharAbstract:SystemC is a new C-based system level design language whose ultimate objective is to enable System-on-a-Chip (SoC) design and verification. Fixed-Point design based on the SystemC data types is rapidly becoming the standard for optimizing DSP systems. In this paper, we propose to create a formalization of SystemC Fixed-Point Arithmetic in the HOL theorem proving environment. The SystemC Fixed-Point number representation which contains a new generalized format and different rounding and overflow modes is described, and then it is formalized in higher-order logic. This formalization is then compared with the formalization of IEEE standard based floating-Point Arithmetic in HOL. A set of theorems are proved to bound the error in Fixed-Point rounding and to verify the Fixed-Point Arithmetic operations against their abstract mathematical counterparts. Finally, we show by an example how this formalization can be used in verification of the translation from floating-Point and Fixed-Point algorithmic, down to register transfer and netlist gate levels in the design flow of SoC systems.
-
ICFEM - Modeling SystemC Fixed-Point Arithmetic in HOL
Formal Methods and Software Engineering, 2003Co-Authors: Behzad Akbarpour, Sofiène TaharAbstract:SystemC is a new C-based system level design language whose ultimate objective is to enable System-on-a-Chip (SoC) design and verification. Fixed-Point design based on the SystemC data types is rapidly becoming the standard for optimizing DSP systems. In this paper, we propose to create a formalization of SystemC Fixed-Point Arithmetic in the HOL theorem proving environment. The SystemC Fixed-Point number representation which contains a new generalized format and different rounding and overflow modes is described, and then it is formalized in higher-order logic. This formalization is then compared with the formalization of IEEE standard based floating-Point Arithmetic in HOL. A set of theorems are proved to bound the error in Fixed-Point rounding and to verify the Fixed-Point Arithmetic operations against their abstract mathematical counterparts. Finally, we show by an example how this formalization can be used in verification of the translation from floating-Point and Fixed-Point algorithmic, down to register transfer and netlist gate levels in the design flow of SoC systems.
-
IFM - Formalization of Cadence SPW Fixed-Point Arithmetic in HOL
Lecture Notes in Computer Science, 2002Co-Authors: Behzad Akbarpour, Abdelkader Dekdouk, Sofiène TaharAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic based on the SPW (Signal Processing WorkSystem) tool. We encoded the Fixed-Point number system and specified the different rounding modes in Fixed-Point Arithmetic such as the directed and even rounding modes.We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the rounding and to verify the basic Arithmetic operations, addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from the floating-Point to Fixed-Point algorithmic levels in the design flow of signal processors.
-
Formalization of cadence SPW Fixed-Point Arithmetic in HOL
Lecture Notes in Computer Science, 2002Co-Authors: Behzad Akbarpour, Abdelkader Dekdouk, Sofiène TaharAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic based on the SPW (Signal Processing WorkSystem) tool. We encoded the Fixed-Point number system and specified the different rounding modes in Fixed-Point Arithmetic such as the directed and even rounding modes. We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the rounding and to verify the basic Arithmetic operations, addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from the floating-Point to Fixed-Point algorithmic levels in the design flow of signal processors.
Zvonimir Rakamaric - One of the best experts on this subject based on the ideXlab platform.
-
an smt theory of Fixed Point Arithmetic
International Joint Conference on Automated Reasoning, 2020Co-Authors: Marek S Baranowski, Mathias Lechner, Thanh Son Nguyen, Zvonimir RakamaricAbstract:Fixed-Point Arithmetic is a popular alternative to floating-Point Arithmetic on embedded systems. Existing work on the verification of Fixed-Point programs relies on custom formalizations of Fixed-Point Arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of Fixed-Point Arithmetic. We present an intuitive yet comprehensive syntax of the Fixed-Point theory, and provide formal semantics for it based on rational Arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.
Marek S Baranowski - One of the best experts on this subject based on the ideXlab platform.
-
an smt theory of Fixed Point Arithmetic
International Joint Conference on Automated Reasoning, 2020Co-Authors: Marek S Baranowski, Mathias Lechner, Thanh Son Nguyen, Zvonimir RakamaricAbstract:Fixed-Point Arithmetic is a popular alternative to floating-Point Arithmetic on embedded systems. Existing work on the verification of Fixed-Point programs relies on custom formalizations of Fixed-Point Arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of Fixed-Point Arithmetic. We present an intuitive yet comprehensive syntax of the Fixed-Point theory, and provide formal semantics for it based on rational Arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.
-
IJCAR (1) - An SMT Theory of Fixed-Point Arithmetic
Automated Reasoning, 2020Co-Authors: Marek S Baranowski, Mathias Lechner, Thanh Son Nguyen, Zvonimir RakamarićAbstract:Fixed-Point Arithmetic is a popular alternative to floating-Point Arithmetic on embedded systems. Existing work on the verification of Fixed-Point programs relies on custom formalizations of Fixed-Point Arithmetic, which makes it hard to compare the described techniques or reuse the implementations. In this paper, we address this issue by proposing and formalizing an SMT theory of Fixed-Point Arithmetic. We present an intuitive yet comprehensive syntax of the Fixed-Point theory, and provide formal semantics for it based on rational Arithmetic. We also describe two decision procedures for this theory: one based on the theory of bit-vectors and the other on the theory of reals. We implement the two decision procedures, and evaluate our implementations using existing mature SMT solvers on a benchmark suite we created. Finally, we perform a case study of using the theory we propose to verify properties of quantized neural networks.
Behzad Akbarpour - One of the best experts on this subject based on the ideXlab platform.
-
Formalization of Fixed-Point Arithmetic in HOL
Formal Methods in System Design, 2005Co-Authors: Behzad Akbarpour, Sofiène Tahar, Abdelkader DekdoukAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic. We encoded the Fixed-Point number system and specified the different quantization modes in Fixed-Point Arithmetic such as the directed and even quantization modes. We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the quantized result after carrying out basic Arithmetic operations, such as addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from floating-Point to Fixed-Point algorithmic level in the signal processing design flow.
-
modeling systemc Fixed Point Arithmetic in hol
International Conference on Formal Engineering Methods, 2003Co-Authors: Behzad Akbarpour, Sofiène TaharAbstract:SystemC is a new C-based system level design language whose ultimate objective is to enable System-on-a-Chip (SoC) design and verification. Fixed-Point design based on the SystemC data types is rapidly becoming the standard for optimizing DSP systems. In this paper, we propose to create a formalization of SystemC Fixed-Point Arithmetic in the HOL theorem proving environment. The SystemC Fixed-Point number representation which contains a new generalized format and different rounding and overflow modes is described, and then it is formalized in higher-order logic. This formalization is then compared with the formalization of IEEE standard based floating-Point Arithmetic in HOL. A set of theorems are proved to bound the error in Fixed-Point rounding and to verify the Fixed-Point Arithmetic operations against their abstract mathematical counterparts. Finally, we show by an example how this formalization can be used in verification of the translation from floating-Point and Fixed-Point algorithmic, down to register transfer and netlist gate levels in the design flow of SoC systems.
-
ICFEM - Modeling SystemC Fixed-Point Arithmetic in HOL
Formal Methods and Software Engineering, 2003Co-Authors: Behzad Akbarpour, Sofiène TaharAbstract:SystemC is a new C-based system level design language whose ultimate objective is to enable System-on-a-Chip (SoC) design and verification. Fixed-Point design based on the SystemC data types is rapidly becoming the standard for optimizing DSP systems. In this paper, we propose to create a formalization of SystemC Fixed-Point Arithmetic in the HOL theorem proving environment. The SystemC Fixed-Point number representation which contains a new generalized format and different rounding and overflow modes is described, and then it is formalized in higher-order logic. This formalization is then compared with the formalization of IEEE standard based floating-Point Arithmetic in HOL. A set of theorems are proved to bound the error in Fixed-Point rounding and to verify the Fixed-Point Arithmetic operations against their abstract mathematical counterparts. Finally, we show by an example how this formalization can be used in verification of the translation from floating-Point and Fixed-Point algorithmic, down to register transfer and netlist gate levels in the design flow of SoC systems.
-
IFM - Formalization of Cadence SPW Fixed-Point Arithmetic in HOL
Lecture Notes in Computer Science, 2002Co-Authors: Behzad Akbarpour, Abdelkader Dekdouk, Sofiène TaharAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic based on the SPW (Signal Processing WorkSystem) tool. We encoded the Fixed-Point number system and specified the different rounding modes in Fixed-Point Arithmetic such as the directed and even rounding modes.We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the rounding and to verify the basic Arithmetic operations, addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from the floating-Point to Fixed-Point algorithmic levels in the design flow of signal processors.
-
Formalization of cadence SPW Fixed-Point Arithmetic in HOL
Lecture Notes in Computer Science, 2002Co-Authors: Behzad Akbarpour, Abdelkader Dekdouk, Sofiène TaharAbstract:This paper addresses the formalization in higher-order logic of Fixed-Point Arithmetic based on the SPW (Signal Processing WorkSystem) tool. We encoded the Fixed-Point number system and specified the different rounding modes in Fixed-Point Arithmetic such as the directed and even rounding modes. We also considered the formalization of exceptions detection and their handling like overflow and invalid operation. An error analysis is then performed to check the correctness of the rounding and to verify the basic Arithmetic operations, addition, subtraction, multiplication and division against their mathematical counterparts. Finally, we showed by an example how this formalization can be used to enable the verification of the transition from the floating-Point to Fixed-Point algorithmic levels in the design flow of signal processors.
Mikel Lujan - One of the best experts on this subject based on the ideXlab platform.
-
accuracy evaluation of deep belief networks with Fixed Point Arithmetic
2014Co-Authors: Jiang Jingfei, Mikel Lujan, Hu Rongdong, Dou YongAbstract:Deep Belief Networks (DBNs) are state-of-art Machine Learning techniques and one of the most important unsupervised learning algorithms. Training DBNs is computationally intensive which naturally leads to investigate FPGA acceleration. Fixed-Point Arithmetic can be used when implementing DBNs in FPGAs to reduce execution time, but it is not clear the implications for accuracy. Previous studies have focused only on accelerators using some Fixed bit-widths. A contribution of this paper is to demonstrate the bit-width effect on various configurations of DBNs in a comprehensive way by experimental evaluation. Explicit performance changing Points are found using various bit-widths. The impact of sigmoid function approximation, required part of DBNs, is evaluated. A solution of mixed bit-widths DBN is proposed, fitting the bit-widths of FPGA primitives and gaining similar performance to the software implementation. Our results provide a guide to inform the design choices on bit-widths when implementing DBNs in FPGAs documenting clearly the trade-off in accuracy.
-
empirical evaluation of Fixed Point Arithmetic for deep belief networks
Applied Reconfigurable Computing, 2013Co-Authors: Jingfei Jiang, Mikel Lujan, Yong DouAbstract:Deep Belief Networks (DBNs) are state-of-art Machine Learning techniques and one of the most important unsupervised learning algorithms. Training DBNs is computationally intensive which naturally leads to investigate FPGA acceleration. Fixed-Point Arithmetic can be used when implementing DBNs in FPGAs to reduce execution time, but it is not clear the implications for accuracy. Previous studies have focused only on accelerators using some Fixed bit-widths. A contribution of this paper is to demonstrate the bit-width effect on various configurations of DBNs in a comprehensive way by experimental evaluation. Our work is inspired by the original DBN built on a subset of neural networks known as Restricted Boltzmann Machine (RBM) and the idea of Stacked Denoising Auto-Encoder (SDAE). We modified the floating-Point versions of the original DBN and the denoising DBN (dDN) into Fixed-Point versions and compared their performance. Explicit performance changing Points are found using various bit-widths. The results indicate that different configurations of DBNs have different performance changing Points. The performance variations of three layers DBNs are a little larger than one layer DBNs because of the better sensitivity of deeper DBN. Sigmoid function approximation methods must be used when implementing DBNs in FPGA. The impacts of Piecewise Linear Approximation of nonlinearity algorithms (PLA) with two different precisions are evaluated quantitatively in our experiments. Modern FPGAs supply built-in primitives to support matrix operations including multiplications, accumulations and additions, which are the main operations of DBNs. A solution of mixed bit-widths DBN is proposed that a narrower bitwidth can be used for neural units and a wider one can be used for weights, thus fitting the bit-widths of FPGA primitives and gaining similar performance to the software implementation. Our results provide a guide to inform the design choices on bit-widths when implementing DBNs in FPGAs documenting clearly the trade-off in accuracy.
-
effect of Fixed Point Arithmetic on deep belief networks abstract only
Field Programmable Gate Arrays, 2013Co-Authors: Jingfei Jiang, Mikel LujanAbstract:Deep Belief Networks (DBNs) are state-of-the-art learning algorithms building on a subset of neural networks, Restricted Boltzmann Machine (RBM). DBNs are computationally intensive posing the question of whether DBNs can be FPGA accelerated. Fixed-Point Arithmetic can have an important influence on the execution time and prediction accuracy of a DBN. Previous studies have focused only on customized RBM accelerators with a Fixed data-width. Our results experiments demonstrate that variable data-widths can obtain similar performance levels. We can also observe that the most suitable data-widths for different types of DBN are not unique or Fixed. From this we conclude that a DBN accelerator should support various data-widths rather than only Fixed one as done in previous work. The processing performance of DBN accelerators in FPGA is almost always constrained not by the capacity of the processing units, but by their on-chip RAM capacity and speed. We propose an efficient memory sub-system combining junction and padding methods to reduce bandwidth usage for DBN accelerators, which shows that supporting various data-widths is not as difficult as it may sound. The cost is only little in hardware terms and does not affect the critical path. We design a generation tool to help users reconfiguring the memory sub-system with arbitrary data-width flexibly. Our tool can also be used as an advanced IP core generator above FPGA memory controller supporting parallel memory access in irregular data-width for other applications.
-
A Flexible Memory Controller Supporting Deep Belief Networks with Fixed-Point Arithmetic
2013 IEEE International Symposium on Parallel & Distributed Processing Workshops and Phd Forum, 2013Co-Authors: Jingfei Jiang, Rongdong Hu, Mikel LujanAbstract:Deep Belief Networks (DBNs) are state-of-art Machine Learning techniques and one of the most important unsupervised learning algorithms. Training DBNs is computationally intensive which naturally leads to investigate FPGA acceleration. Fixed-Point Arithmetic can have an important influence on the execution time and prediction accuracy of a DBN. Previous studies have focused only on customized DBN accelerators with a Fixed data-width. Our results experiments demonstrate that supporting various data-widths in different DBN configurations and application environments does make sense for achieving acceptable performance. From this we conclude that a DBN accelerator should support various data-widths rather than the Fixed one as done in previous work. The processing performance of DBN accelerators in FPGA is almost always constrained not by the capacity of the processing units, but by their on-chip RAM capacity and speed. We propose an efficient memory controller for DBN accelerators, which shows that supporting various data-widths is not as difficult as it may sound. The cost is only little in hardware terms and does not affect the critical path. We have designed a tool to help users reconfiguring the memory controller with arbitrary data-width flexibly.
-
IPDPS Workshops - A Flexible Memory Controller Supporting Deep Belief Networks with Fixed-Point Arithmetic
2013 IEEE International Symposium on Parallel & Distributed Processing Workshops and Phd Forum, 2013Co-Authors: Jingfei Jiang, Mikel LujanAbstract:Deep Belief Networks (DBNs) are state-of-art Machine Learning techniques and one of the most important unsupervised learning algorithms. Training DBNs is computationally intensive which naturally leads to investigate FPGA acceleration. Fixed-Point Arithmetic can have an important influence on the execution time and prediction accuracy of a DBN. Previous studies have focused only on customized DBN accelerators with a Fixed data-width. Our results experiments demonstrate that supporting various data-widths in different DBN configurations and application environments does make sense for achieving acceptable performance. From this we conclude that a DBN accelerator should support various data-widths rather than the Fixed one as done in previous work. The processing performance of DBN accelerators in FPGA is almost always constrained not by the capacity of the processing units, but by their on-chip RAM capacity and speed. We propose an efficient memory controller for DBN accelerators, which shows that supporting various data-widths is not as difficult as it may sound. The cost is only little in hardware terms and does not affect the critical path. We have designed a tool to help users reconfiguring the memory controller with arbitrary data-width flexibly.