Synthesizing SVA local variables for formal verification
Jiang Qi Long, Andrew Seawright · Proceedings - ACM IEEE Design Automation Conference · 2007
This paper describes techniques for efficiently handling a 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.