An Abstraction Algorithm for the Verification of Level-Sensitive Latch-Based Netlists

被引:0
作者
Jason Baumgartner
Tamir Heyman
Vigyan Singhal
Adnan Aziz
机构
[1] IBM Enterprise Systems Group,
[2] IBM Haifa Research Laboratory,undefined
[3] Tempus Fugit,undefined
[4] Inc.,undefined
[5] The University of Texas,undefined
来源
Formal Methods in System Design | 2003年 / 23卷
关键词
phase abstraction; automatic abstraction; model reduction; bisimulation; CTL model checking; level-sensitive latch;
D O I
暂无
中图分类号
学科分类号
摘要
High-performance hardware designs often intersperse combinational logic freely between level-sensitive latch layers (wherein each layer is transparent during only one clock phase), rather than utilizing master-slave latch pairs with no combinational logic between. While such designs may generally achieve much faster clock speeds, this design style poses a challenge to verification. In particular, unless the k-phase netlist N is abstracted to a full-cycle register-based netlist N′, verification of N requires k times (or greater) as many state variables as would be necessary to obtain equivalent verification of N′. We present algorithms to automatically identify and abstract k-phase netlists—i.e., to perform phase abstraction—by selectively eliminating latches. The abstraction is valid for model checking CTL* formulae which reason solely about latches of a single phase. This algorithm has been implemented in the model checker RuleBase, and used to enhance the model checking of IBM's Gigahertz Processor, which would not have been feasible otherwise due to computational constraints. This abstraction has furthermore allowed verification engineers to write properties and environments more efficiently.
引用
收藏
页码:39 / 65
页数:26
相关论文
共 18 条
  • [1] Browne M.C.(1988)Characterizing finite kripke structures in propositional temporal logic Theoretical Computer Science 59 115-131
  • [2] Clarke E.M.(1989)Analysis of preflow push algorithms for maximum network flow SIAM Journal on Computing 18 1057-1086
  • [3] Grumberg O.(1986)Automatic verification of finite-state concurrent systems using temporal logic specifications ACM Transactions on Programming Languages and Systems 8 244-263
  • [4] Cheriyan J.(1986)Sometimes and not never revisited: On branching time versus linear time temporal logic Journal of the ACM 33 151-178
  • [5] Maheshwari S.N.(1994)Module checking and modular verification ACM Transactions on Programming Languages and Systems 16 843-871
  • [6] Clarke E.M.(1983)Optimizing synchronous systems Journal of VLSI and Computer Systems 1 41-67
  • [7] Emerson E.A.(1991)Retiming synchronous circuitry Algorithmica 6 5-35
  • [8] Sistla A.P.(1993)Computing the initial states of retimed circuits IEEE Transactions on Computer-Aided Design 12 157-162
  • [9] Emerson E.A.(undefined)undefined undefined undefined undefined-undefined
  • [10] Halpern J.Y.(undefined)undefined undefined undefined undefined-undefined