Method and apparatus for memory abstraction and verification using same
A computer implemented representation of a circuit design including memory is abstracted to a smaller netlist, which can be analyzed by standard verification tools and by other tools that operate on netlists. The correctness of such systems can require reasoning about a much smaller number of memory entries than exist in the circuit design, and by abstracting such memories to a smaller number of entries, the computational complexity of the verification problem is substantially reduced.
1. A method for processing a computer implemented representation of a circuit design, comprising:
representing the circuit design, as a data structure defining a netlist as a plurality of nodes;
identifying nodes representing a memory in the data structure, and processing the netlist using a data processor to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a pre-specified property of the circuit design using the substitute nodes.
2. The method of claim 1 , wherein the netlist comprises nodes arranged in a directed acyclic graph, including word-level nodes representing logical and arithmetic operators, word-level nodes representing multiplexer operators, word-level nodes representing concatenation operators, word-level nodes representing extraction operators, word-level nodes representing reads, word-level nodes representing writes, word-level nodes representing state variables and word-level nodes representing binary constants.
3. The method of claim 1 , wherein said identifying nodes representing a memory include determining for the memory and for the next state function for the memory that all read and write nodes addressing the memory, read and write data of the same width and use address nodes of the same width.
4. The method of claim 1 , wherein the pre-specified property is a safety definition.
5. The method of claim 1 , wherein the updated data structure comprises a netlist.
6. The method of claim 1 , including manufacturing an integrated circuit using said circuit design.
7. A method for processing a computer implemented representation of a circuit design, comprising:
representing the circuit design as a data structure defining a netlist as a plurality of nodes;
identifying nodes representing a memory in the data structure, and processing the netlist using a data processor to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist re representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a pre-specified property of the circuit design using the substitute nodes;
wherein said substituting replaces the memory with a set of substitute nodes, including
for each represented slot, current state and next state substitute nodes and current state and next state nodes identifying the represented slot, and
for nodes representing writes to a corresponding slot implementing a multiplexer updating the contents of a next state substitute node for the slot with write data if the write address matches an output of the current state node identifying the represented slot, or else updating the contents of a next state substitute node for the slot with contents of a current state substitute node for the slot, and
for nodes in the netlist representing reads to a corresponding slot implementing a multiplexer returning contents of the current state substitute node for the slot if the read address matches an output of the current state node identifying the represented slot, or else returning non-determinate data.
8. A method for processing a computer implemented representation of a circuit design, comprising:
representing the circuit design as a data structure defining a netlist as a plurality of nodes;
identifying nodes representing a memory in the data structure, and processing the netlist using a data processor to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist re representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a pre-specified property of the circuit design using the substitute nodes including implementing said verification condition by identifying abstraction pairs, said abstraction pairs including an abstracted node in the updated netlist corresponding to a current state substitute node in the updated netlist and a delay parameter indicating a cycle in which to read the current state substitute node using an output of the abstracted node, and establishing a set of nodes in the updated netlist that compares the abstracted node with the node identifying the represented slot for the corresponding current state substitute node in the indicated cycle, and if a match is indicated for the identified abstraction pairs, then checking a pre-specified property.
9. The method of claim 8 , including performing a counter-example guided refinement process to identify the abstraction pairs.
10. The method of claim 8 , including providing an initial updated netlist;
performing a model checking process over the initial updated netlist, and if the model checking fails in a particular state, then running a simulation using the input netlist based on a set of inputs and initial state variable assignments determined from the particular state; if the simulation passes, then finding erroneous reads responsible for the failure detected in the updated netlist, selecting abstraction pairs to address the erroneous reads and adding the selected abstraction pairs to the updated netlist.
11. A data processing system adapted to process a computer implemented representation of a circuit design, comprising:
a data processor and memory coupled to the data processor, the memory storing instructions executable by the data processor representing the circuit design in the memory as a data structure defining a netlist as a plurality of nodes; including instructions
to identify nodes representing a memory in the data structure, and to process the netlist to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a specified safety definition using the substitute nodes.
12. The data processing system of claim 11 , wherein the netlist comprises nodes arranged in a directed acyclic graph, including word-level nodes representing logical and arithmetic operators, word-level nodes representing multiplexer operators, word-level nodes representing concatenation operators, word-level nodes representing extraction operators, word-level nodes representing reads, word-level nodes representing writes, word-level nodes representing state variables and word-level nodes representing binary constants.
13. The data processing system of claim 11 , wherein said instruction to identify nodes representing a memory includes instructions to determine for the memory and for the next state function for the memory that all read and write nodes address the memory, read and write data of the same width and use address nodes of the same width.
14. The data processing system of claim 11 , wherein the pre-specified property is a safety definition.
15. The data processing system of claim 11 , wherein the updated data structure comprises a netlist.
16. A data processing system adapted to process a computer implemented representation of a circuit design, comprising;
a data processor and memory coupled to the data processor, the memory storing instructions executable by the data processor representing the circuit design in the memory as a data structure defining a netlist as a plurality of nodes; including instructions
to identify nodes representing a memory in the data structure and to process the netlist to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist re resenting the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a specified safety definition using the substitute nodes;
wherein said substituting replaces the memory with a set of substitute nodes for each represented slot, said set including current state and next state substitute nodes and current state and next state nodes identifying the represented slot, and for nodes representing writes to a corresponding slot implementing a multiplexer updating the contents of a next state substitute node for the slot with write data if the write address matches an output of the current state node identifying the represented slot, or else updating the contents of a next state substitute node for the slot with contents of a current state substitute node for the slot, and for nodes in the netlist representing reads to a corresponding slot implementing a multiplexer returning contents of the current state substitute node for the slot if the read address matches an output of the current state node identifying the represented slot, or else returning non-determinate data.
17. A data processing system adapted to process a computer implemented representation of a circuit design, comprising;
a data processor and memory coupled to the data processor, the memory storing instructions executable by the data processor representing the circuit design in the memory as a data structure defining a netlist as a plurality of nodes; including instructions
to identify nodes representing a memory in the data structure and to process the netlist to produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist re representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a specified safety definition using the substitute nodes;
said instructions implementing said verification condition by identifying abstraction pairs, said abstraction pairs including an abstracted node in the updated netlist corresponding to a current state substitute node in the updated netlist and a delay parameter indicating a cycle in which to read the current state substitute node using an output of the abstracted node, and establishing a set of nodes in the updated netlist that compares the abstracted node with the node identifying the represented slot for the corresponding current state substitute node in the indicated cycle, and if a match is indicated for the identified abstraction pairs, then checking a pre-specified property.
18. The data processing system of claim 17 , including instructions for performing a counter-example guided refinement process to identify the abstraction pairs.
19. The data processing system of claim 17 , including instructions
providing an initial updated netlist; and
performing a model checking process over the initial updated netlist, and if the model checking fails in a particular state, then running a simulation using the input netlist based on a set of inputs and initial state variable assignments determined from the particular state; if the simulation passes, then finding erroneous reads responsible for the failure detected in the updated netlist, selecting abstraction pairs to address the erroneous reads and adding the selected abstraction pairs to the updated netlist.
20. An article of manufacture providing software adapted to process a computer implemented representation of a circuit design, comprising:
a memory readable by a data processor, the memory storing instructions executable by the data processor representing the circuit design in the memory as a data structure defining a netlist as a plurality of nodes; and including instructions
to identify nodes representing a memory in the data structure, and to process the netlist produce an updated netlist, including
identifying a slot or slots in the memory for representation in the updated netlist;
substituting the nodes in the netlist representing the memory with substitute nodes implementing the identified slot or slots; and
implementing a verification condition for the circuit design that enables checking of a pre-specified property of the circuit design using the substitute nodes.