基于队列的树形加法优化认证器
Queue-Based Tree Addition Optimization Authenticator
DOI: 10.12677/CSA.2023.1310182, PDF,   
作者: 冯天烁, 史美琦, 齐 爽, 江建国*：辽宁师范大学数学学院，辽宁 大连
关键词: 形式验证；认证器；NSS证明；队列；树形加法；Formal Verification； Authenticator； NSS Proof； Queue； Tree Addition
摘要: 目前验证乘法器电路依然是一个极其重要的问题，形式验证给出系统的正确性，但为了增加形式验证结果的可靠性，我们在验证过后加入了认证过程，以检验其结果的正确性。同时运用Amulet工具生成Nullstellensatz (NSS)证明来提高对自动化推理的信心，并由独立的认证器Nuss-Checker进行检查。本文在认证器生成规范多项式过程中，运用基于队列的树形加法优化该认证器，降低了求和过程中形成多项式的项的数目，提高了认证器的检查效率。
Abstract: At present, the verification of the multiplier circuit is still an extremely important problem. The formal verification gives the correctness of the system, but in order to increase the reliability of the formal verification results, we add the authentication process after the verification to check the correctness of the results. The AMULET tool is also used to generate Nullstellensatz (NSS) proofs to increase confidence in automated reasoning and to be checked by the independent certifier USS Checker. In this paper, the authenticator is optimized by tree addition based on queue, which reduces the number of polynomials and improves the checking efficiency of the authenticator.
文章引用：冯天烁, 史美琦, 齐爽, 江建国. 基于队列的树形加法优化认证器[J]. 计算机科学与应用, 2023, 13(10): 1837-1845. https://doi.org/10.12677/CSA.2023.1310182

参考文献

[1] Kaufmann, D., Biere, A. and Kauers, M. (2019) Verifying Large Multipliers by Combining SAT and Computer Algebra. 2019 Formal Methods in Computer Aided Design (FMCAD), San Jose, 22-25 October 2019, 28-36. [Google Scholar] [CrossRef] 
[2] Parhami, B. (2000) Computer Arithmetic—Algorithms and Hardware Designs. Oxford University Press, Oxford.
[3] Heule, M.J.H., Kauers, M. and Seidl, M. (2019) Local Search for Fast Matrix Multiplication. In: Janota, M. and Lynce, I., Eds., Theory and Applications of Satisfiability Testing, Vol. 11628, Springer, Cham, Berlin, 155-163. [Google Scholar] [CrossRef] 
[4] Bright, C., Kotsireas, I. and Ganesh, V. (2019) SAT Solvers and Computer Algebra Systems: A Powerful Combination for Mathematics.
[5] Bright, C., Kotsireas, I. and Ganesh, V. (2019) Applying Computer Algebra Systems and SAT Solvers to the Williamson Conjecture. Journal of Symbolic Computation, 100, 187-209. [Google Scholar] [CrossRef] 
[6] Beame, P., Impagliazzo, R., Krajíček, J., Pitassi, T. and Pudlák, P. (1996) Lower Bounds on Hilbert’s Nullstellensatz and Propositional Proofs. The Proceedings of the London Mathematical Society, s3-73, 1-26. [Google Scholar] [CrossRef] 
[7] Ritirc, D., Biere, A. and Kauers, M. (2018) A Practical Polynomial Calculus for Arithmetic Circuit Verifification. CEUR-WS, 61-76.
[8] Kaufmann, D. (2021) Nullstellensatz-Proofs for Multiplier Verifification. http://fmv.jku.at/nussproofs
[9] Mahzoon, A., Große, D., Scholl, C. and Drechsler, R. (2020) Towards Formal Verifification of Optimized and Industrial Multipliers. 2020 Design, Automation & Test in Europe Conference & Exhibition, Grenoble, 9-13 March 2020, 544-549. [Google Scholar] [CrossRef] 
[10] Buchberger, B. (1965) Ein Algorithmus zum Auffifinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. Ph.D. Thesis, Uni-versity of Innsbruck, Innsbruck.
[11] Kuehlmann, A., Paruthi, V., Krohm, F. and Ganai, M. (2002) Robust Boolean Reasoning for Equivalence Checking and Functional Property Verifification. IEEE Transactions on Computer-Aided De-sign of Integrated Circuits and Systems, 21, 1377-1394. [Google Scholar] [CrossRef] 
[12] Lichtblau, D. (2012) Effective Computation of Strong Gröbner Bases over Euclidean Domains. Illinois Journal of Mathematics, 56, 177-194. [Google Scholar] [CrossRef] 
[13] Niemetz, A., Preiner, M., Wolf, C. and Biere, A. (2018) BTOR2, BtorMC and Boolector 3.0. In: Chockler, H. and Weis-senbacher, G., Eds., Lecture Notes in Computer Science, Vol. 10981, Springer, Berlin, 587-595. [Google Scholar] [CrossRef] 
[14] Homma, N., Watanabe, Y., Aoki, T. and Higuchi. T. (2006) Formal Design of Arithmetic Circuits Based on Arithmetic Description Language. IEICE Transactions, E89-A, 3500-3509. [Google Scholar] [CrossRef]