公开(公告)号：EP2797017B1

公开(公告)日：2020-04-01

申请号：EP14166051.4

申请日：2014-04-25

申请人： OneSpin Solutions GmbH

发明人： Straßer, Dominik ,  Niesler, Gerrit ,  Fit, Mirko ,  Brinkmann, Raik

IPC分类号： G06F17/50

公开(公告)号：EP2797017A1

公开(公告)日：2014-10-29

申请号：EP14166051.4

申请日：2014-04-25

申请人： OneSpin Solutions GmbH

发明人： Straßer, Dominik ,  Niesler, Gerrit ,  Fit, Mirko ,  Brinkmann, Raik

IPC分类号： G06F17/50

摘要： A method for formal verification of a digital circuit using a cloud-based verification engine. The method comprises extracting a proof problem from a design of a digital circuit with a local processor, reducing said proof problem to proof relevant data, encrypting said reduced proof problem, transmitting said encrypted reduced proof problem to a remote server, decrypting said encrypted reduced proof problem at said remote server, storing said reduced proof problem in a memory at said remote server, running a proof on said reduced proof problem at said remote server to generate a proof result; encrypting said proof result at said remote server; transmitting said encrypted proof result to said local processor; decrypting said encrypted proof result at said local processor; and reconstructing a verification result of said digital circuit design at said local processor using said decrypted proof result.

摘要翻译： 一种使用基于云的验证引擎对数字电路进行形式验证的方法。 该方法包括：利用本地处理器从数字电路的设计中提取证明问题，减少所述证明问题以证明相关数据，加密所述减少验证问题，将所述加密的减少验证问题发送给远程服务器，解密所述加密的减少证明 在所述远程服务器上存储所述减少验证问题到所述远程服务器的存储器中，对所述远程服务器上的所述减少验证问题进行证明，以生成验证结果; 在所述远程服务器上加密所述验证结果; 将所述加密验证结果发送到所述本地处理器; 在所述本地处理器处解密所述加密验证结果; 以及使用所述解密证明结果在所述本地处理器处重构所述数字电路设计的验证结果。