Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems

# Lazy Arithmetic using Systolic Arrays for Closing the Verification Gap on Embedded Systems
Source: [https://arxiv.org/html/2607.15328](https://arxiv.org/html/2607.15328)
## 1\.Overview

As capabilities of deep neural network \(DNN\) models has grown – from computer vision systems to digital twins driving precision medicine – so has the interest in verifying these models for deployment in safety\-critical embedded devices\. However, the deployment of these models, even formally verified ones, has laid bare a key limitation: current software \(SW\) and hardware \(HW\) approaches for deploying edge DNNs are designed for increased throughput, not safety, correctness, nor fault\-tolerance\. As such, guarantees of model correctness are breaking\.

## 2\.Limitations of Current Verification Schemes

While a range of DNN verification schemes exist, they are largely perform model verification on “evaluation HW” \(computers, servers, etc\)\(Georgeet al\.,[2026](https://arxiv.org/html/2607.15328#bib.bib1); Narasimhamurthyet al\.,[2019](https://arxiv.org/html/2607.15328#bib.bib4); Wanget al\.,[2021](https://arxiv.org/html/2607.15328#bib.bib3); Duonget al\.,[2025](https://arxiv.org/html/2607.15328#bib.bib2)\)\. This presents challenges for embedded and edge device deployment due to numerical incompatibilities across HW platforms\. For example, in\(Jia and Rinard,[2021](https://arxiv.org/html/2607.15328#bib.bib47)\)the authors show that floating point errors can be exploited in the verification of DNNs, negating verification guarantees\. While they lay out ways to mitigate this issue the proposed solutions \(including large over\-approximates, relying on specific details of specific floating point base types, using heavily quantized for fixed point or even binary NN, and/or using exact real arithmetic\) all such solutions are currently far too inefficient for practical applications\. This results in a breaking of formally verified guarantees when porting models between HW platforms\.

## 3\.Deployment Breaks: Software Quantization

As full\-precision inference of DNNs with acceptable latency and memory use is often infeasible on edge devices, a common remedy is quantization\. This is the process of representing weights and activations with reduced and finite\-precision arithmetic to decrease compute and storage costs\. State\-of\-the\-art practice includes quantization\-aware training as well as post\-training quantization \(PTQ\); more recently, automated mixed\-precision PTQ methods have shown that per\-layer bit\-widths can be selected to reduce inference cost while providing provable error bounds under fixed modeling and operating assumptions\(Loharet al\.,[2023](https://arxiv.org/html/2607.15328#bib.bib14)\)\. However, existing approaches largely assume static bit\-width assignments, fixed input distributions/classes, and unchanging performance bounds, which limits applicability in real deployments where operating conditions and required accuracy can vary with input range, and operating environment\. In addition, we lack a principled framework to identify and reason about inputs that are most sensitive to quantization\-induced shifts, particularly those near decision boundaries where small numeric perturbations can change predicted classes and void formal verification guarantees\.

## 4\.Deployment Breaks: Edge Hardware

Even assuming a verified, sound, and efficient quantization scheme existed, current edge hardware such as GPUs, NPUs, and TPUs prioritize throughput and computational efficiency, rather than robustness against low\-level hardware attacks\. In particular, recent work has shown significant risk of embedded DNNs exhibiting “silent degradation” due to bit flips, either through fault\-injection \(FI\) attacks\(Leveugleet al\.,[2025](https://arxiv.org/html/2607.15328#bib.bib6)\)or benign single\-event upsets \(SEUs\) from environmental radiation\(Gutiérrez\-Zaballaet al\.,[2024](https://arxiv.org/html/2607.15328#bib.bib7)\)\. This breaks any formal guarantees of DNN model correctness as evaluated on a development platform\.

## 5\.Our Work and Proposal

As such, novel efficient and soundly verified quantization schemes as well as fault tolerant devices performing evaluations of neural networks on the edge are growing in need\. Herein we present two interwoven ideas: a SW approach for enabling real\-time adaptive\-precision quantization, along with the HW to support it\. The quantization algorithm dynamically adjusts precision online while performing sensitivity analysis to quantify and manage the risk of decision\-boundary crossings, enabling resource\-efficient inference with explicit, verified, reasoning about quantization impacts\. To achieve this we utilize a lazy left\-to\-right approach leveraging lazy multi\-word floats, continued fractions and continued logarithms\. This approach is not limited to DNNs, though we show how the specific architecture of DNNs can be leveraged for significant efficiency gains, passing the most\-significant blocks \(MSB\) – whether these are bits, floats, or other types – quickly, and removing unnecessary computations in real\-time\. Next we propose how systolic arrays can be designed to enable even stronger efficiency of this new quantization scheme, and use triplication to ensure resilience to bit flip attacks on the MSB\(Guilleméet al\.,[2026](https://arxiv.org/html/2607.15328#bib.bib45)\)\.

Together, these advances can close the gap between existing formal verification techniques for DNN algorithms, and their verified, space and memory efficient deployment onto embedded devices\. This submission is presented as work\-in\-progress, with SW implementations completed and HW in\-progress\.

## 6\.Verified and Sound Dynamic, Adaptive, Real\-Time Quantization \(DARQ\)

In a recent project, we showed three key contributions, detailed below which provide the basis for our quantization scheme, and systolic hardware idea\. Furthermore, we constructed a DNN evaluation framework which can both identify when and how various quantization schemes will affect DNN performance, as well as provide a sound left\-to\-right implementation for DNNs\.

### Quantization Error is Rare but Significant

By evaluating a suite of image classification DNNs, we have shown that when and where quantization error effects models is rare, difficult to predict, but very significant\. Existing results include a suite of models trained on fuzzy\-boundary Fashion\-MNIST dataset\(Xiaoet al\.,[2017](https://arxiv.org/html/2607.15328#bib.bib5)\), with others in progress\. This aligns with current standing that intensive quantization is generally OK, though in the case of DNNs where correctness is of the essence, such as safety\-critical systems, errors can be severely detrimental\. Furthermore, determining when and where these errors arise is non\-trivial, pointing to a unique benefit of our lazy arithmetic approach in identifying these points in real\-time\. Importantly, we are able to perform this across all operations within the DNN, not only at the output layer\.

### Lazy Computation is Possible

We show it is possible \(in theory and practice\) to utilize lazy ‘left\-to\-right” arithmetic to enable sound, power and memory efficient computation\. We have shown this potential in enabling the use of neural network based algorithms in complex environments and on resource\-limited hardware where performance guarantees are necessary\. This lays the groundwork for implementation on both existing and custom hardware, as with the systolic arrays\.

### Leveraging Neural Network Architectures for Significant Efficiency Gains:

While this is broadly useful for high assurance mathematics, graphical applications and signal processing, the architecture of DNN models is such that significant power and memory efficiency gains are possible through our lazy implementation using a lazy list of small floats: we find locations when upwards of 99% of computations are unused, and we can stop these operations quickly through lazy implementations, or target them for probabilistic optimization\. An example of one such DNN evaluated is provided in Table[1](https://arxiv.org/html/2607.15328#S6.T1), where it is evident that certain layer types \(such as Max Pool\) require both an average and worst\-case high number of MSBs to achieve sound evaluation \(mostly caused by true equalities of two separate but complex chain of arithmetic\), whereas other layer types such as Convolutions with ReLu‘s never require more than a depth of 2\.

Table 1\.Depth Analysis of MSBs \(utilizing a base FP8E5M2\) required for an example DNN evaluation, grouped by layer type\. Large max depths were true equalities\.

## 7\.Leveraging DNN Architecture for Systolic Array Hardware Efficiencies

Building from the final key contribution of our software quantization approach, we further define the particular aspects of DNNs which enable both software and hardware efficiency\. The foundational arithmetic used in DNNs relies on large matrix math operations followed by a non\-linear activation function\. These models are designed to be sparse, and as such often times these activation functions can be answered with very little information from the calculation just performed\. For example the rectified linear unit \(ReLU\) activation function simply checks if the function is positive or negative\. This information could be answered by simply checking the sign of the calculation performed\. In our noted DARQ work, we found that often a very small amount of information is actually needed for DNNs to evaluate – at times with upwards of 99% of computations able to be stopped after only 1 MSB \(Table[1](https://arxiv.org/html/2607.15328#S6.T1)\)\.

While we can currently evaluate DNNs using lazy arithmetic to calculate MSBs, there is significant overhead associated with these lazy computations done in software\. Thus we turn to novel HW and are currently working on lazy arithmetic system using systolic arrays in which the MSBs \(with a bit\-base\) are calculated first\. This allows for calculating activation functions quickly and efficiently, while also identifying the critical bits necessary to flow through a DNN to boost resilience to bit flip attacks\. These bits can be queued and pulled from for other calculations further down the DNN\. In order to accomplish this task we build upon the algorithms laid out in\(Ciaffaglione and Gianantonio,[1999](https://arxiv.org/html/2607.15328#bib.bib44)\), and detailed below\. We have chosen the algorithms in\(Ciaffaglione and Gianantonio,[1999](https://arxiv.org/html/2607.15328#bib.bib44)\)as a starting point due to it’s simplicity and for the fact that the algorithms allow for the ability to get down to MSBs with bit bases \(rather than floats or other types\)\.

## 8\.Real Number Algorithms for Systolic Arrays

In\(Ciaffaglione and Gianantonio,[1999](https://arxiv.org/html/2607.15328#bib.bib44)\), a lazy stream of ternary digits is used to represent the real numbers\. Addition of these streams is done by consuming one ternary digit from each stream, to create an initial state, and after that the algorithm produces the most significant digit by consuming one more from each, Figure[1](https://arxiv.org/html/2607.15328#S8.F1)\. Multiplication of scalars is similarly defined in\(Ciaffaglione and Gianantonio,[1999](https://arxiv.org/html/2607.15328#bib.bib44)\)\.

![Refer to caption](https://arxiv.org/html/2607.15328v1/addition-algo.png)Figure 1\.Addition algorithm for real number streams\(Ciaffaglione and Gianantonio,[1999](https://arxiv.org/html/2607.15328#bib.bib44)\)\.Currently we are generating a systolic implementation of this algorithm that breaks down two doubles into this format and produces the most significant digit first\. It does this by creating a queue of digits from each double, and then pumps them through the gate to get a single queue output, which has the most significant bit first\.

We are also exploring chaining these together to form general matrix multiply \(GeMM\) algorithms and multiply add \(MAD\) algorithms commonly used in DNN, which produces a queue of outputs with the MSB first\. The eventual end goal being a library of algorithms similar to that of\(Chetluret al\.,[2014](https://arxiv.org/html/2607.15328#bib.bib46)\)\.

## 9\.Significance and Conclusion

Together the SW and HW approaches presented herein fill a significant gap in verifying DNNs for use on embedded safety\-critical devices, by enhancing efficiency, soundness, and bridging the gap between reasoning with floating point numbers and reals\. If our work proves fruitful, it would allow reasoning directly with a real number implementation to allow for an easier verification story, and mitigate issues between algorithm verification and implementation on edge devices\. Furthermore, the novel implementation of the real numbers using systolic arrays which we are exploring is not only limited to DNNs, but generalizes across all high\-precision mathematics needs\. Lastly, the MSB targeted approach allows for robustness against bit flip attacks \(malicious or spurious\) which is of interest for edge devices\.

## Acknowledgments

This material is based upon work supported by the Defense Advanced Research Projects Agency \(DARPA\) and Naval Information Warfare Center Pacific \(NIWC Pacific\) under Contract No\. N66001\-21\-C\-4023\. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author\(s\) and do not necessarily reflect the views of DARPA and NIWC Pacific\. Distribution Statement A\. Approved for public release: distribution is unlimited\.

## References

- S\. Chetlur, C\. Woolley, P\. Vandermersch, J\. Cohen, J\. Tran, B\. Catanzaro, and E\. Shelhamer \(2014\)CuDNN: efficient primitives for deep learning\.pp\.\.Cited by:[§8](https://arxiv.org/html/2607.15328#S8.p3.1)\.
- A\. Ciaffaglione and P\. D\. Gianantonio \(1999\)A co\-inductive approach to real numbers\.InSelected Papers from the International Workshop on Types for Proofs and Programs,TYPES ’99,Berlin, Heidelberg,pp\. 114–130\.External Links:ISBN 3540415173Cited by:[§7](https://arxiv.org/html/2607.15328#S7.p2.1),[Figure 1](https://arxiv.org/html/2607.15328#S8.F1),[§8](https://arxiv.org/html/2607.15328#S8.p1.1)\.
- H\. Duong, T\. Nguyen, and M\. B\. Dwyer \(2025\)NeuralSAT: a high\-performance verification tool for deep neural networks\.InComputer Aided Verification,R\. Piskac and Z\. Rakamarić \(Eds\.\),Cham,pp\. 409–423\.External Links:ISBN 978\-3\-031\-98679\-6Cited by:[§2](https://arxiv.org/html/2607.15328#S2.p1.1)\.
- R\. J\. George, J\. Cruden, X\. Zhong, H\. Zhang, and A\. Anandkumar \(2026\)TorchLean: formalizing neural networks in lean\.arXiv preprint arXiv:2602\.22631\.Cited by:[§2](https://arxiv.org/html/2607.15328#S2.p1.1)\.
- W\. Guillemé, G\. Lounes, A\. Kritikakou, Y\. Helen, R\. Gerzaguet, M\. Gautier, C\. Killian, and D\. Chillet \(2026\)Selective triplication for fault\-tolerant systolic array processing elements\.InProceedings of the Rapid Simulation and Performance Evaluation for Design Workshop,RAPIDO ’26,New York, NY, USA,pp\. 8–13\.External Links:ISBN 9798400722875,[Link](https://doi.org/10.1145/3787501.3787503),[Document](https://dx.doi.org/10.1145/3787501.3787503)Cited by:[§5](https://arxiv.org/html/2607.15328#S5.p1.1)\.
- J\. Gutiérrez\-Zaballa, K\. Basterretxea, and J\. Echanobe \(2024\)Evaluating single event upsets in deep neural networks for semantic segmentation: an embedded system perspective\.Journal of Systems Architecture154,pp\. 103242\.External Links:[Document](https://dx.doi.org/https%3A//doi.org/10.1016/j.sysarc.2024.103242),ISSN 1383\-7621,[Link](https://www.sciencedirect.com/science/article/pii/S1383762124001796)Cited by:[§4](https://arxiv.org/html/2607.15328#S4.p1.1)\.
- K\. Jia and M\. Rinard \(2021\)Exploiting verified neural networks via floating point numerical error\.InStatic Analysis: 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17–19, 2021, Proceedings,Berlin, Heidelberg,pp\. 191–205\.External Links:ISBN 978\-3\-030\-88805\-3,[Link](https://doi.org/10.1007/978-3-030-88806-0_9),[Document](https://dx.doi.org/10.1007/978-3-030-88806-0%5F9)Cited by:[§2](https://arxiv.org/html/2607.15328#S2.p1.1)\.
- R\. Leveugle, A\. Al\-Kaf, and M\. Benabdenbi \(2025\)Edge ai trustworthiness: revisiting bit\-flip impacts and criticality conditions\.Electronics14\(16\),pp\. 3186\.External Links:[Document](https://dx.doi.org/10.3390/electronics14163186),ISSN 2079\-9292,[Link](http://dx.doi.org/10.3390/electronics14163186)Cited by:[§4](https://arxiv.org/html/2607.15328#S4.p1.1)\.
- D\. Lohar, C\. Jeangoudoux, A\. Volkova, and E\. Darulova \(2023\)Sound mixed fixed\-point quantization of neural networks\.ACM Transactions on Embedded Computing Systems22\(5s\),pp\. 1–26\.Cited by:[§3](https://arxiv.org/html/2607.15328#S3.p1.1)\.
- M\. Narasimhamurthy, T\. Kushner, S\. Dutta, and S\. Sankaranarayanan \(2019\)Verifying conformance of neural network models: invited paper\.2019 IEEE/ACM International Conference on Computer\-Aided Design \(ICCAD\),pp\. 1–8\.Cited by:[§2](https://arxiv.org/html/2607.15328#S2.p1.1)\.
- S\. Wang, H\. Zhang, K\. Xu, X\. Lin, S\. Jana, C\. Hsieh, and Z\. Kolter \(2021\)Beta\-crown: efficient bound propagation with per\-neuron split constraints for neural network robustness verification\.InProceedings of the 35th International Conference on Neural Information Processing Systems,NIPS ’21,Red Hook, NY, USA\.External Links:ISBN 9781713845393Cited by:[§2](https://arxiv.org/html/2607.15328#S2.p1.1)\.
- H\. Xiao, K\. Rasul, and R\. Vollgraf \(2017\)External Links:cs\.LG/1708\.07747Cited by:[§6](https://arxiv.org/html/2607.15328#S6.SS0.SSS0.Px1.p1.1)\.