Cloud-basd digital verification system and method
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.
1. A method for formal verification of a digital circuit comprising:
extracting a proof problem from data representing a register-transfer level functionality of the digital circuit with a local processor by removing timing aspects from data representing the register-transfer level functionality of the digital circuit;
reducing said proof problem to proof relevant data by removing all signals that are not inputs or states of the digital circuit;
anonymizing with a translation table and encrypting said reduced proof problem;
transmitting said anonymized and encrypted reduced proof problem to a remote server;
decrypting said anonymized and encrypted reduced proof problem at said remote server;
storing said anonymized reduced proof problem in a memory at said remote server;
running a proof for verification of the design of the digital circuit on said anonymized reduced proof problem at said remote server to generate an anonymized proof result;
encrypting said anonymized proof result at said remote server;
transmitting said anonymized and encrypted proof result to said local processor;
de-anonymizing and decrypting said anonymized and encrypted proof result at said local processor; and
reconstructing a verification result of said digital circuit design at said local processor using the inputs and the states from said de-anonymized and decrypted proof result.
2. A method for formal verification of a digital circuit according to claim 1 , wherein said extracted proof problem comprises a reformulation of the HDL representation of the design of the digital circuit.
3. A method for formal verification of a digital circuit according to claim 1 , further comprising compressing said encrypted reduced proof problem prior to transmitting it to said remote server.
4. A method for formal verification of a digital circuit according to claim 1 , further comprising compressing said encrypted reduced proof result prior to transmitting it to said local processor.
5. A method for formal verification of a digital circuit comprising:
extracting a proof problem from data representing a register-transfer level functionality of the digital circuit with a local processor by removing timing aspects from the data representing the register-transfer level functionality of the digital circuit;
reducing said proof problem to proof relevant data by removing all signals that are not inputs or states of the digital circuit;
encrypting said reduced proof problem;
transmitting said encrypted reduced proof problem to a remote server;
storing said reduced proof problem in a memory at said remote server;
running a proof for verification of the design of the digital circuit on said reduced proof problem at said remote server to generate a proof result;
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 the inputs and states from said decrypted proof result.
6. A method for formal verification of a digital circuit according to claim 5 , wherein said extracted proof problem comprises a reformulation of the HDL representation of the design of the digital circuit.
7. A method for formal verification of a digital circuit according to claim 5 , further comprising compressing said encrypted reduced proof problem prior to transmitting it to said remote server.
8. A method for formal verification of a digital circuit according to claim 5 , further comprising compressing said encrypted reduced proof result prior to transmitting it to said local processor.