TECHNIQUE DE VÉRIFICATION EN TEMPS RÉEL DE CIRCUITS ARITHMÉTIQUES SANS MÉMOIRE BASÉS SUR LES MATHÉMATIQUES VÉDIQUES
DOI :
https://doi.org/10.59277/RRST-EE.2025.4.15Mots-clés :
Test, Vérification formelle, Mathématiques védiques, Circuits arithmétiques, Vecteurs de test, Intégration à très grande échelle (VLSI)Résumé
Cet article propose une nouvelle méthode de vérification des opérations arithmétiques dans les circuits, fondée sur le sutra (formule) mathématique védique « Gunita Samuccaya ». Selon ce sutra, notre méthode vérifie les opérations arithmétiques, par exemple c = a + b, en vérifiant que la somme des chiffres « a » et « b » est égale à la somme des chiffres de « c » pour un calcul correct. Contrairement aux schémas d'autotest intégrés (BIST), notre approche est plus simple, car elle élimine les générateurs de modèles de test traditionnels et les analyseurs de sortie, tout en atteignant une couverture des défauts de 100 % pour les opérations arithmétiques simples. Notre système, conçu dans le langage de description du matériel (HDL) Verilog, est en temps réel, sans mémoire et évolutif. Cette méthode de test proposée révolutionne la vérification des circuits arithmétiques, garantissant l'intégrité des systèmes numériques complexes où la précision mathématique est essentielle.
Références
(1) M. Kubo and M. Fujita, Debug methodology for arithmetic circuits on FPGAs, In IEEE International Conference on Field-Programmable Technology (FPT) Proceedings, Hong Kong, China, IEEE, pp. 236–242 (2002).
(2) R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore, S. Pandav, A. Slobodov´a, C. Taylor, V. Frolov, E. Reeber, and A. Naik, Replacing testing with formal verification in Intel® CoreTM i7 processor execution engine validation, In A. Bouajjani and O. Maler (eds.), Computer Aided Verification, Springer, Berlin, Heidelberg, Lecture Notes in Computer Science, vol. 5643 (2009).
(3) M.D. Aagard, R.B. Jones, R. Kaivola, K.R. Kohatsu, and C.H. Seger, Formal verification of iterative algorithms in microprocessors, Proceedings of the 37th ACM/IEEE Design Automation Conference (DAC 2000), ACM Press, Los Angeles, pp. 201–206 (2000).
(4) C.M. Kalaiselvi and R.S. Sabeenian, Design of area-speed efficient Anurupyena Vedic multiplier for deep learning applications, Analog Integr Circ Sig Process, 119, pp. 521–533 (2004).
(5) A. Biere, M. Kauers, and D. Ritirc, Challenges in verifying arithmetic circuits using computer algebra, In 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), Timisoara, Romania, IEEE, pp. 9–15 (2017).
(6) D. Kaufmann and A. Biere, Improving AMULET2 for verifying multiplier circuits using SAT solving and computer algebra, Int J Softw Tools Technol Transfer, 25, pp. 133–144 (2023).
(7) M. Barhoush, A. Mahzoon, and R. Drechsler, Polynomial word-level verification of arithmetic circuits, 19th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), Beijing, China, IEEE, pp. 1–9 (2021).
(8) S. Abed, M. AlMehteb, W. Mansoor, and A. Gawanmeh, Verification of non-linear arithmetic circuits using functionally reduced and-inverter-graph (FRAIG), Global Congress on Electrical Engineering (GC-ElecEng), Valencia, Spain, IEEE, pp. 118–123 (2020).
(9) A. Yasin, T. Su, S. Pillement, and M. Ciesielski, Functional verification of hardware dividers using algebraic model, IFIP/IEEE 27th International Conference on Very Large-Scale Integration (VLSI-SoC), Cuzco, Peru, IEEE, pp. 257–262 (2019).
(10) F. Farahmandi and P. Mishra, Automated Test generation for debugging multiple bugs in arithmetic circuits, IEEE Transactions on Computers, 68, 2, pp. 182–197 (2019).
(11) D. Ritirc, A. Biere, and M. Kauers, Column-wise verification of multipliers using computer algebra, Formal Methods in Computer Aided Design (FMCAD), Vienna, Austria, IEEE, pp. 23–30 (2017).
(12) B. Yu and M. Ciesielski, Formal verification using don't-care and vanishing polynomials, IEEE Computer Society Annual Symposium on VLSI (ISVLSI), Pittsburgh, PA, USA, IEEE, pp. 284–289 (2016).
(13) B. Yu, W. Brown, D. Liu, A. Rossi, and M. Ciesielski, Formal Verification of Arithmetic Circuits by Function Extraction, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35, 12, pp. 2131–2142 (2016).
(14) S. Ghandali, C. Yu, D. Liu, W. Brown, and M. Ciesielski, Logic Debugging of Arithmetic Circuits, In IEEE Computer Society Annual Symposium on VLSI, Montpellier, France, IEEE, pp. 113–118 (2015).
(15) O. Sarbishei, B. Alizadeh, and M. Fujita, Arithmetic circuits verification without looking for internal equivalences, 6th ACM/IEEE International Conference on Formal Methods and Models for Co-Design, Anaheim, CA, USA, IEEE, pp. 7–16 (2008).
(16) O. Sarbishei, M. Tabandeh, B. Alizadeh, and M. Fujita, A formal approach for debugging arithmetic circuits, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28, 5, pp. 742–754 (2009).
(17) M. Ciesielski, C. Yu, W. Brown, D. Liu, and A. Rossi, Verification of gate-level arithmetic circuits by function extraction, In 52nd ACM/EDAC/IEEE Design Automation Conference (DAC), San Francisco, CA, USA, IEEE, pp. 1–6 (2015).
(18) F. Farahmandi, B. Alizadeh, and Z. Navabi, Effective combination of algebraic techniques and decision diagrams to formally verify large arithmetic circuits, IEEE Computer Society Annual Symposium on VLSI, Tampa, FL, USA, IEEE, pp. 338–343 (2014).
(19) M.R. Kumar and R. Sundaram, Effective feature extraction method for unconstrained environment: local binary pattern or local ternary pattern, Rev. Roum. Sci. Techn. – Électrotechn. et Énerg., pp. 449–454 (2024).
(20) 20. P. Nagarajan, T. Kavitha, N.A. Kumar, Al.S. Edward, Power energy and power area product simulation analysis of master-slave flip-Flop, Rev. Roum. Sci. Techn. – Électrotechn. et Énerg., pp. 325–330 (2023).
(21) A. Ramaiah, P.D. Balasubramanian, A. Appathurai, and N.A. Muthukumaran, Detection of Parkinson’s disease via Clifford gradient-based recurrent neural network using multi-dimensional Data, Rev. Roum. Sci. Techn. – Électrotechn. et Énerg., 69, 1, pp. 103–108 (2024).
(22) L. Sriraman, K.S. Kumar, and T.N. Prabakar, Design and FPGA implementation of binary squarer using Vedic mathematics, Fourth International Conference on Computing, Communications and Networking Technologies (ICCCNT), pp. 1–5 (2013).
Téléchargements
Publiée
Numéro
Rubrique
Licence
(c) Copyright REVUE ROUMAINE DES SCIENCES TECHNIQUES — SÉRIE ÉLECTROTECHNIQUE ET ÉNERGÉTIQUE 2025
Ce travail est disponible sous licence Creative Commons Attribution - Pas d'Utilisation Commerciale - Pas de Modification 4.0 International.
