基于队列的树形加法优化认证器  

Queue-Based Tree Addition Optimization Authenticator

作　　者：冯天烁 史美琦 齐爽 江建国[1] 

机构地区：[1]辽宁师范大学数学学院,辽宁 大连

出　　处：《计算机科学与应用》2023年第10期1837-1845,共9页Computer Science and Application

摘　　要：目前验证乘法器电路依然是一个极其重要的问题,形式验证给出系统的正确性,但为了增加形式验证结果的可靠性,我们在验证过后加入了认证过程,以检验其结果的正确性。同时运用Amulet工具生成Nullstellensatz (NSS)证明来提高对自动化推理的信心,并由独立的认证器Nuss-Checker进行检查。本文在认证器生成规范多项式过程中,运用基于队列的树形加法优化该认证器,降低了求和过程中形成多项式的项的数目,提高了认证器的检查效率。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.

关 键 词：形式验证 认证器 NSS证明 队列 树形加法 

分 类 号：TP3[自动化与计算机技术—计算机科学与技术]