Word-Level Sequential Memory Abstraction for Model Checking

el Sequential Memory Abstraction for Model Checking Per Bjesse Advanced Technology Group Synopsys Inc. Many designs intermingle large memories with wide data paths and nontrivial control. Verifying such systems is challenging, and users often get little traction when applying model checking to decide full or partial end-to-end correctness of such designs. Interestingly, a subclass of these systems can be proven correct by reasoning only about a small number of the memory entries at a limited number of time points. In this e leverage this fact to abstract certain memories in a y, and we demonstrate how our memory abstraction with an abstraction refinement algorithm can be used to prove correctness properties for three challenging designs from industry and academia. Key features of our approach are that we operate on standard safety property verification problems, that we proceed completely automatically without for abstraction hints, that we can use any bit-level model checker as a back...

• Type: Conference
• Year: 2008
• Where: FMCAD
• Authors: Per Bjesse
• Keywords: FMCAD 2008, Formal Methods, Memory Abstraction, Model Checking, Sequential Memory Abstraction