Synthesizing SVA Local Variables for Formal Verification

This paper describes techniques for efficiently subset of System Verilog Assertion (SVA) safety properties with local variables in formal verification. The techniques produce checker circuits using datapath logic and pipeline registers for handling the local variables where the datapath logic and pipeline registers scales lineally to the size of the property expressed in the SVA abstract grammar.