Optimizing automatic abstraction refinement for generalized symbolic trajectory evaluation

ng Automatic Abstraction Refinement for Generalized Symbolic Trajectory Evaluation Yan Chen Dept. of Computer Science Portland State University Portland, OR, 97207 [e-mail] Fei Xie Dept. of Computer Science Portland State University Portland, OR, 97207 [e-mail] Jin Yang Strategic CAD Labs, DTS Intel Corporation Hillsboro, OR 97124 [e-mail] In this paper, we present a suite of optimizations targeting autostraction refinement for Generalized Symbolic Trajectory Evaluation (GSTE). We optimize both model refinement and spec refinement supported by AutoGSTE: a counterexample-guided refinement loop for GSTE. Experiments on a family of benchmark circuits have shown that our optimizations lead to major efficiency ents in verification involving abstraction refinement. Categories and Subject Descriptors B.6.3 [Logic Design]: Design Aids--Verification, Optimization General Terms Verification, Performance, Algorithms Keywords Model Checking, Generalized Symbolic Trajecto...

• Type: Conference
• Year: 2008
• Where: DAC
• Authors: Yan Chen, Fei Xie, Jin Yang
• Keywords: Automatic Abstraction Refinement, Counterexample-guided Refinement Loop, DAC 2008, Design Automation, Symbolic Trajectory Evaluation