Sciweavers

DAC
2008
ACM

Optimizing automatic abstraction refinement for generalized symbolic trajectory evaluation

14 years 4 months ago
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 chenyan@cs.pdx.edu Fei Xie Dept. of Computer Science Portland State University Portland, OR, 97207 xie@cs.pdx.edu Jin Yang Strategic CAD Labs, DTS Intel Corporation Hillsboro, OR 97124 jin.yang@intel.com 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...
Yan Chen, Fei Xie, Jin Yang
Added 12 Nov 2009
Updated 12 Nov 2009
Type Conference
Year 2008
Where DAC
Authors Yan Chen, Fei Xie, Jin Yang
Comments (0)