Enhanced analysis of array-based netlists via phase abstraction
First Claim
1. A method, in a data processing system, for performing phase abstraction on an integrated circuit design with a memory array, the method comprising:
- receiving, by the data processing system, a netlist for an integrated circuit design, wherein the netlist comprises a memory array;
for a given memory array in the netlist, duplicating each write port of the given memory array for a plurality of time values up to an unfold degree to form a plurality of write ports and unfolding each enable pin, address pin, and data pin in each write port within the plurality of write ports;
for the given memory array in the netlist, duplicating each read port of the given memory array for the plurality of time values to form a plurality of read ports and unfolding each enable pin, address pin, and data pin in each read port within the plurality of read ports;
for each data pin of the plurality of read ports, creating a multiplexor structure to form a phase abstracted integrated circuit design, wherein the multiplexor structure selects an output of the data pin based on whether an address of the read port is out-of-bounds, whether the read port is enabled, and whether the memory array is a write-before-read array; and
outputting, by the data processing system, the phase abstracted integrated circuit design.
4 Assignments
0 Petitions
Accused Products
Abstract
A mechanism is provided for increasing the scalability of transformation-based formal verification solutions through enabling the use of phase abstraction on logic models that include memory arrays. The mechanism manipulates the array to create a plurality of copies of its read and write ports, representing the different modulo time frames. The mechanism converts all write-before-read arrays to read-before-write and adds a bypass path around the array from write ports to read ports to capture any necessary concurrent read and write forwarding. The mechanism uses an additional set of bypass paths to ensure that the proper write data that becomes effectively concurrent through the unfolding inherent in phase abstraction is forwarded to the proper read port. If a given read port is disabled or fetches out-of-bounds data, the mechanism applies randomized data to the read port data output.
80 Citations
20 Claims
-
1. A method, in a data processing system, for performing phase abstraction on an integrated circuit design with a memory array, the method comprising:
-
receiving, by the data processing system, a netlist for an integrated circuit design, wherein the netlist comprises a memory array; for a given memory array in the netlist, duplicating each write port of the given memory array for a plurality of time values up to an unfold degree to form a plurality of write ports and unfolding each enable pin, address pin, and data pin in each write port within the plurality of write ports; for the given memory array in the netlist, duplicating each read port of the given memory array for the plurality of time values to form a plurality of read ports and unfolding each enable pin, address pin, and data pin in each read port within the plurality of read ports; for each data pin of the plurality of read ports, creating a multiplexor structure to form a phase abstracted integrated circuit design, wherein the multiplexor structure selects an output of the data pin based on whether an address of the read port is out-of-bounds, whether the read port is enabled, and whether the memory array is a write-before-read array; and outputting, by the data processing system, the phase abstracted integrated circuit design. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8)
-
-
9. A computer program product comprising a non-transitory computer readable storage medium having a computer readable program stored therein, wherein the computer readable program, when executed on a computing device, causes the computing device to:
-
receive, by the computing device, a netlist for an integrated circuit design, wherein the netlist comprises a memory array; for a given memory array in the netlist, duplicate each write port of the given memory array for a plurality of time values up to an unfold degree to form a plurality of write ports and unfold each enable pin, address pin, and data pin in each write port within the plurality of write ports; for the given memory array in the netlist, duplicate each read port of the given memory array for the plurality of time values to form a plurality of read ports and unfold each enable pin, address pin, and data pin in each read port within the plurality of read ports; for each data pin of the plurality of read ports, create a multiplexor structure to form a phase abstracted integrated circuit design, wherein the multiplexor structure selects an output of the data pin based on whether an address of the read port is out-of-bounds, whether the read port is enabled, and whether the memory array is a write-before-read array; and output, by the computing device, the phase abstracted integrated circuit design. - View Dependent Claims (10, 11, 12, 13, 14, 15, 16)
-
-
17. An apparatus, comprising:
-
a processor; and a memory coupled to the processor, wherein the memory comprises instructions which, when executed by the processor, cause the processor to; receive a netlist for an integrated circuit design, wherein the netlist comprises a memory array; for a given memory array in the netlist, duplicate each write port of the given memory array for a plurality of time values up to an unfold degree to form a plurality of write ports and unfold each enable pin, address pin, and data pin in each write port within the plurality of write ports; for the given memory array in the netlist, duplicate each read port of the given memory array for the plurality of time values to form a plurality of read ports-and unfold each enable pin, address pin, and data pin in each read port within the plurality of read ports; for each data pin of the plurality of read ports, create a multiplexor structure to form a phase abstracted integrated circuit design, wherein the multiplexor structure selects an output of the data pin based on whether an address of the read port is out-of-bounds, whether the read, port is enabled, and whether the memory array is a write-before-read array; and output the phase abstracted integrated circuit design. - View Dependent Claims (18, 19, 20)
-
Specification