Browse Prior Art Database

MEMORY ARRAY STATE NODE IDENTIFICATION TOOL

IP.com Disclosure Number: IPCOM000007619D
Original Publication Date: 1996-May-01
Included in the Prior Art Database: 2002-Apr-10
Document File: 3 page(s) / 160K

Publishing Venue

Motorola

Related People

Manish Pandey: AUTHOR [+2]

Abstract

Memory arrays in this document refer to a SBAM or DRAM core with at least one write port. Exam- ples of such arrays include multi-ported register files, cache memory SRAM core and cache tag arrays. Identification of state nodes in a memory array is an important prerequisite for many simulation and for- mal verification tasks. Circuit properties are usually expressed in terms of these nodes. Also, for simula- tion, we can initialize the circuit to a given state by setting the internal state nodes to certain values.

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 40% of the total text.

Page 1 of 3

0 M

MolylRoLA Technical Developments

MEMORY ARRAY STATE NODE IDENTIFICATION TOOL

by Manish Pandey and Randal E. Bryant

identify state nodes in a switch-level network. In both approaches, the number of boolean variables used in the FSM extraction process equals to or exceeds the number of state nodes in the circuit. Since a memory array contains a large number of state nodes, both extraction techniques can poten- tially generate very large Ordered Binary Decision Diagrams (OBDDs) [I].

  Our technique, in contrast, does not suffer horn any of the above disadvantages. It can handle static storage structures, and for a memory with n words of m bits each, it requires only log(n) + M boolean variables to operate.

1 INTRODUCTION

  Memory arrays in this document refer to a SBAM or DRAM core with at least one write port. Exam- ples of such arrays include multi-ported register files, cache memory SRAM core and cache tag arrays. Identification of state nodes in a memory array is an important prerequisite for many simulation and for- mal verification tasks. Circuit properties are usually expressed in terms of these nodes. Also, for simula- tion, we can initialize the circuit to a given state by setting the internal state nodes to certain values.

  A memory array modeled at the switch-level typ- ically contains a huge number of circuit nodes and only a fraction of these are the actual memory stor- age nodes. It is tedious, if not impossible, to identify all such nodes and the memory location they repre- sent manually. A large variety of storage structures are possible in a switch-level network. So, often it is not feasible to identify state nodes by pattern matching for storage structures.

3 METHODOLOGY
3.1 BACKGROUND

2 PREVIOUS WORK

  Previous work in this area has focussed on extrac- tion of finite state machines (FSMs) from switch- level networks. In the process of extracting a FSM, the state nodes of the network are identified. The FSM extraction work by Kam and Subramaniyam
[4] uses Anamos to derive the network excitation function and extracts the FSM by a fixed-point com- putation. This approach does not work for static stor- age structures. Another approach described in [5] extracts FSMs from a switch-level network by sym- bolic simulation, but this approach does not identify the state nodes in the switch-level network. Instead, it identifies state nodes in a gate-level network which is derived from the switch-level network.

  Kam and Subramaniyam's work does not work for static storage structures, which is a serious short- coming of their approach. The work in [S] does not

  We use symbolic simulation [3] to simulate the switch-level network for the memory array. Sym- bolic simulation is a modified form of simulation where circuit nodes can take on symbolic values over the 0, 1, X ternary domain, including 0, 1, Xvalues themselves.

  For example, in a 2-input AND gate, if the two inputs are set to the symbolic values a and 6, the output ofthe gate w...