Title :
Optimizing automatic abstraction refinement for Generalized Symbolic Trajectory Evaluation
Author :
Chen, Yan ; Xie, Fei ; Yang, Jin
Author_Institution :
Dept. of Comput. Sci., Portland State Univ., Portland, OR
Abstract :
In this paper, we present a suite of optimizations targeting automatic abstraction 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 improvements in verification involving abstraction refinement.
Keywords :
circuit optimisation; electronic engineering computing; logic design; program verification; AutoGSTE; automatic abstraction refinement; benchmark circuits; generalized symbolic trajectory evaluation; model refinement; spec refinement; Algorithm design and analysis; Circuit analysis; Computer science; Design optimization; Error analysis; Hardware; Logic design; State-space methods; Trajectory; Automatic Abstraction Refinement; Generalized Symbolic Trajectory Evaluation; Model Checking;
Conference_Titel :
Design Automation Conference, 2008. DAC 2008. 45th ACM/IEEE
Conference_Location :
Anaheim, CA
Print_ISBN :
978-1-60558-115-6
