scholarly journals Syntax-Guided Quantifier Instantiation

2021 ◽  
pp. 145-163
Author(s):  
Aina Niemetz ◽  
Mathias Preiner ◽  
Andrew Reynolds ◽  
Clark Barrett ◽  
Cesare Tinelli
Keyword(s):  
State Of The Art ◽  
Satisfiability Modulo Theories ◽  
Floating Point ◽  
New Approach ◽  
Smt Solver ◽  
Floating Point Arithmetic ◽  
Novel Approach ◽  
Non Linear ◽  
Quantifier Instantiation ◽  
Point Arithmetic

AbstractThis paper presents a novel approach for quantifier instantiation in Satisfiability Modulo Theories (SMT) that leverages syntax-guided synthesis (SyGuS) to choose instantiation terms. It targets quantified constraints over background theories such as (non)linear integer, reals and floating-point arithmetic, bit-vectors, and their combinations. Unlike previous approaches for quantifier instantiation in these domains which rely on theory-specific strategies, the new approach can be applied to any (combined) theory, when provided with a grammar for instantiation terms for all sorts in the theory. We implement syntax-guided instantiation in the SMT solver CVC4, leveraging its support for enumerative SyGuS. Our experiments demonstrate the versatility of the approach, showing that it is competitive with or exceeds the performance of state-of-the-art solvers on a range of background theories.

A new approach for block floating-point arithmetic in recursive filters

1985 ◽  
Vol 32 (7) ◽  
pp. 719-722 ◽  
Author(s):  
D. Williamson ◽  
S. Sridharan ◽  
P. McCrea
Keyword(s):  
Floating Point ◽  
New Approach ◽  
Recursive Filters ◽  
Floating Point Arithmetic ◽  
Point Arithmetic

scholarly journals A Two-Phase Approach for Conditional Floating-Point Verification

2021 ◽  
pp. 43-63
Author(s):  
Debasmita Lohar ◽  
Clothilde Jeangoudoux ◽  
Joshua Sobel ◽  
Eva Darulova ◽  
Maria Christakis
Keyword(s):  
State Of The Art ◽  
Floating Point ◽  
Two Phase ◽  
Phase Approach ◽  
Special Values ◽  
Floating Point Arithmetic ◽  
Roundoff Errors ◽  
Dynamic Analyses ◽  
Point Arithmetic

AbstractTools that automatically prove the absence or detect the presence of large floating-point roundoff errors or the special values NaN and Infinity greatly help developers to reason about the unintuitive nature of floating-point arithmetic. We show that state-of-the-art tools, however, support or provide non-trivial results only for relatively short programs. We propose a framework for combining different static and dynamic analyses that allows to increase their reach beyond what they can do individually. Furthermore, we show how adaptations of existing dynamic and static techniques effectively trade some soundness guarantees for increased scalability, providing conditional verification of floating-point kernels in realistic programs.

A Novel FPGA based Leading One Anticipation Algorithm for Floating Point Arithmetic Units

2012 ◽  
Vol 1 (1) ◽  
pp. 19
Author(s):  
Ashwini Suresh Deshmukh
Keyword(s):  
High Speed ◽  
State Of The Art ◽  
Multimedia Systems ◽  
Floating Point ◽  
Silicon Area ◽  
Latency Reduction ◽  
Floating Point Arithmetic ◽  
Total Latency ◽  
Arithmetic Units ◽  
Point Arithmetic

In multimedia Systems-on-Chips, the design of specialized IEEE-754-compliant floating point arithmetic units (FPU) is critical with respect to both operating speed and silicon area demand. Leading one anticipation is a well-known issue in the implementation of high speed FPUs. We investigated a novel leading one anticipation algorithm allowing us to significantly reduce the anticipation failure rate with respect to the state-of the art. We embedded our technique into a complete FPU and compared its performance against existing solutions, definitely showing both area savings and total latency reduction.

scholarly journals Numerical algorithms for high-performance computational science

2020 ◽  
Vol 378 (2166) ◽  
pp. 20190066 ◽  
Author(s):  
Jack Dongarra ◽  
Laura Grigori ◽  
Nicholas J. Higham
Keyword(s):  
High Performance ◽  
Numerical Algorithms ◽  
Computational Science ◽  
Floating Point ◽  
Important Criterion ◽  
Data Movement ◽  
Floating Point Arithmetic ◽  
High Performance Computers ◽  
Point Arithmetic ◽  
Speed And Accuracy

A number of features of today’s high-performance computers make it challenging to exploit these machines fully for computational science. These include increasing core counts but stagnant clock frequencies; the high cost of data movement; use of accelerators (GPUs, FPGAs, coprocessors), making architectures increasingly heterogeneous; and multi- ple precisions of floating-point arithmetic, including half-precision. Moreover, as well as maximizing speed and accuracy, minimizing energy consumption is an important criterion. New generations of algorithms are needed to tackle these challenges. We discuss some approaches that we can take to develop numerical algorithms for high-performance computational science, with a view to exploiting the next generation of supercomputers. This article is part of a discussion meeting issue ‘Numerical algorithms for high-performance computational science’.

Fast and robust mesh arrangements using floating-point arithmetic

2020 ◽  
Vol 39 (6) ◽  
pp. 1-16
Author(s):  
Gianmarco Cherchi ◽  
Marco Livesu ◽  
Riccardo Scateni ◽  
Marco Attene
Keyword(s):  
Floating Point ◽  
Floating Point Arithmetic ◽  
Point Arithmetic

Floating-point arithmetic with 84-bit numbers

1964 ◽  
Vol 7 (1) ◽  
pp. 10-13 ◽  
Author(s):  
Robert T. Gregory ◽  
James L. Raney
Keyword(s):  
Floating Point ◽  
Floating Point Arithmetic ◽  
Point Arithmetic
Sign in / Sign up

Export Citation Format

Share Document