| With developments in the field of integrated circuit design, chip integration was getting higher and higher with more and more powerful functions, and more and more important verification. The equivalent checking in the formal verification was through the whole of digital circuit back-end design, such as: the comparison between RTL and netlist; the one between netlist and layout.The paper completed the equivalence check about macphydl communication accelerator model. Firstly, the check prepared the information of codes and netlist. In the netlist, there were models area report and the report of the logic, such as: and gate, or gate, latch-up, register... in the codes library (startliblphvt9t), showed all kindes of model areas and counts.Secondly, the paper did the verification flow: 1. in the preparation, created the scripts of flow and compilation, the directory in the system linux. 2. in the extract, got the compiled codes from model codes, and compilation scripts. 3. about compilation, checked codes and netlist, and the gat files. 4. for running, checked the outputs and next-states after making the initial values for inputs and states, with constraints. If we had the all equivalence, the work had been done. Otherwise, read the report results: if the design was OK, the work was done, or repeat doing with modifying constraints.At last there were unequivalent information 5000 outputs and 8000 next-states. 1. modifying the netlist to solve the connection errors between signals. 2. removing the redundant clock gating in the constraints of netlist to finish the equivalence. 3. gave the values to the undriven nets to done the equivalence. 4. maching the pins by manual to solve the equivalence. In the conclusion, the verification had gotten the whole of the equivalence for 5176 outputs and 10062 next-states. |
