Abstract:In the field of chip design, the use of model-driven FPGA design methods is currently a safer and more reliable method. However, model-driven FPGA design needs to prove the consistency of the FPGA design model and the generated Verilog/VHDL code. Further, the chip design correctness, performance, reliability, and safety are critical. At present, simulation methods are often used to verify the consistency of models and codes. It is difficult to ensure the reliability and safety of the design, and there are problems such as low verification efficiency and heavy workload. This study proposes a new method to verify the consistency of the design model and the generated code. This method uses the MSVL language to model the system, and propositional projection temporal logic (PPTL) formula to describe the properties of the system, then based on the principle of unified model checking, verifies whether the model meets the validity of the property. Furthermore, a signal light control system is used as a verification example to verify and explain the verification method.