Some confuse about pynq devicetree overlay

I’m learning how to use HDMI. In a tutorial(here), he set up the device tree like this:

/include/ "system-conf.dtsi"
#include <dt-bindings/gpio/gpio.h>
/* #include </home/rich/petalinux20242/rehsdZynq/xilinx-vip.h> */   /*this doesn't work!?*/
 / {
    model = "rehsd Zynq-7000 Board";
    compatible = "rehsd,zynq-7000", "xlnx,zynq-7000";
    chosen {
    };
    bootargs = "console=ttyPS0,115200 earlyprintk uio_pdrv_genirq.of_id=generic-uio";
    usb_phy0: usb_phy@0 {
        compatible = "ulpi-phy";
        #phy-cells = <0>;
        reg = <0xe0002000 0x1000>;
        view-port = <0x0170>;
        reset-gpios = <&gpio0 46 1>;
        drv-vbus;
    };
};
&gem0 {
    phy-handle = <&ethernet_phy>;
    ethernet_phy: ethernet-phy@0 {
        device_type = "ethernet-phy";
        reg = <0>;
        /* dt-bindings/phy/realtek.h */
        /* #define REALTEK_LED_LINK10              BIT(0)
           #define REALTEK_LED_LINK100             BIT(1)
           #define REALTEK_LED_LINK1000            BIT(3)
           #define REALTEK_LED_ACT                 BIT(4)
           #define REALTEK_LED_DEFAULT             BIT(7)
        */
        /* LED0=10+A, LED1=100+A, LED2=1000+A */
        realtek,leds-config = <0x11 0x12 0x18>;
    };
};
&usb0{
    status = "okay";
    dr_mode = "host";
    usb-phy = <&usb_phy0>;
};
&i2c0 {
    clock-frequency = <100000>;
    status = "okay";
};
&amba_pl {
    digilent_hdmi {
        compatible = "digilent,hdmi";
        clocks = <&axi_dynclk_0>;
        clock-names = "clk";
        digilent,edid-i2c = <&i2c0>;
        digilent,fmax = <150000>;
        port@0 {
            hdmi_ep: endpoint {
                remote-endpoint = <&pl_disp_ep>;
            };
        };
    };
    xlnx_pl_disp {
        compatible = "xlnx,pl-disp";
        dmas = <&axi_vdma_0 0>;
        dma-names = "dma0";
        /* xlnx,vtc = <&v_tc_0>; */
        /* dglnt,edid-i2c = <&i2c1 >; */
        xlnx,vformat = "XR24";
        xlnx,bridge = <&v_tc_0>;
        port@0 {
            pl_disp_ep: endpoint {
                remote-endpoint = <&hdmi_ep>;
            };
        };
    };
};
&axi_vdma_0 {
    dma-ranges = <0x00000000 0x00000000 0x40000000>;
};
&axi_dynclk_0 {
    compatible = "dglnt,axi-dynclk";
    #clock-cells = <0>;
    clocks = <&clkc 15>;
};
&v_tc_0 {
};
compatible = "xlnx,bridge-v-tc-6.1";
xlnx,pixels-per-clock = <1>;
/* clock-names = "s_axi_aclk", "clk"; */
/* clocks = <&clkc 15>, <&axi_dynclk_0>; */
&axi_gpio_hdmi {
    compatible = "generic-uio";
};

I’m not quite sure exactly how to write the DToverlay for Pynq. Based on my rough understanding, I have written the following content.

/*
 * CAUTION: This file is automatically generated by Xilinx.
 * Version: XSCT 2022.1
 * Today is: Tue Oct 28 14:00:25 2025
 */


/dts-v1/;
/plugin/;
/ {
	fragment@2 {
		target = <&amba>;
		overlay2: __overlay__ {
			#address-cells = <1>;
			#size-cells = <1>;
			axi_dynclk_0: axi_dynclk@43c00000 {
				/* This is a place holder node for a custom IP, user may need to update the entries */
				clock-names = "REF_CLK_I", "s00_axi_aclk";
				clocks = <&clkc 15>, <&clkc 15>;
				compatible = "dglnt,axi-dynclk";
				reg = <0x43c00000 0x10000>;
				xlnx,s00-axi-addr-width = <0x5>;
				xlnx,s00-axi-data-width = <0x20>;
			};
			axi_intc_0: interrupt-controller@41800000 {
				#interrupt-cells = <2>;
				clock-names = "s_axi_aclk";
				clocks = <&clkc 15>;
				compatible = "xlnx,axi-intc-4.1", "xlnx,xps-intc-1.00.a";
				interrupt-controller ;
				interrupt-names = "irq";
				interrupt-parent = <&intc>;
				interrupts = <0 29 4>;
				reg = <0x41800000 0x10000>;
				xlnx,kind-of-intr = <0x0>;
				xlnx,num-intr-inputs = <0x3>;
			};
			axi_vdma_0: dma@43000000 {
				#dma-cells = <1>;
				clock-names = "s_axi_lite_aclk", "m_axi_mm2s_aclk", "m_axis_mm2s_aclk";
				clocks = <&clkc 15>, <&clkc 15>, <&clkc 15>;
				compatible = "xlnx,axi-vdma-6.3", "xlnx,axi-vdma-1.00.a";
				interrupt-names = "mm2s_introut";
				interrupt-parent = <&axi_intc_0>;
				interrupts = <0 2>;
				reg = <0x43000000 0x10000>;
				xlnx,addrwidth = <0x20>;
				xlnx,flush-fsync = <0x1>;
				xlnx,num-fstores = <0x3>;
				dma-channel@43000000 {
					compatible = "xlnx,axi-vdma-mm2s-channel";
					interrupts = <0 2>;
					xlnx,datawidth = <0x18>;
					xlnx,device-id = <0x0>;
					xlnx,genlock-mode ;
				};
			};
			hdmi_out_hpd_video: gpio@41200000 {
				#gpio-cells = <2>;
				#interrupt-cells = <2>;
				clock-names = "s_axi_aclk";
				clocks = <&clkc 15>;
				compatible = "generic-uio";
				gpio-controller ;
				interrupt-controller ;
				interrupt-names = "ip2intc_irpt";
				interrupt-parent = <&axi_intc_0>;
				interrupts = <2 2>;
				reg = <0x41200000 0x10000>;
				xlnx,all-inputs = <0x0>;
				xlnx,all-inputs-2 = <0x0>;
				xlnx,all-outputs = <0x0>;
				xlnx,all-outputs-2 = <0x0>;
				xlnx,dout-default = <0x00000000>;
				xlnx,dout-default-2 = <0x00000000>;
				xlnx,gpio-width = <0x1>;
				xlnx,gpio2-width = <0x20>;
				xlnx,interrupt-present = <0x1>;
				xlnx,is-dual = <0x0>;
				xlnx,tri-default = <0xFFFFFFFF>;
				xlnx,tri-default-2 = <0xFFFFFFFF>;
			};
			vtc_out: v_tc@43c10000 {
				clock-names = "clk", "s_axi_aclk";
				clocks = <&misc_clk_0>, <&clkc 15>;
				compatible = "xlnx,v-tc-6.2", "xlnx,v-tc-6.1";
				interrupt-names = "irq";
				interrupt-parent = <&axi_intc_0>;
				interrupts = <1 2>;
				reg = <0x43c10000 0x10000>;
				xlnx,generator ;
			};
			misc_clk_0: misc_clk_0 {
				#clock-cells = <0>;
				clock-frequency = <100000000>;
				compatible = "fixed-clock";
			};
			
			digilent_hdmi {
                compatible = "digilent,hdmi";
                
                clocks = <&axi_dynclk_0>;
                clock-names = "clk";
                
                digilent,edid-i2c = <&i2c0>;
                digilent,fmax = <150000>;
                
                port@0 {
                    hdmi_ep: endpoint {
                        remote-endpoint = <&pl_disp_ep>;
                    };
                };
            };
			xlnx_pl_disp {
                compatible = "xlnx,pl-disp";
                
                dmas = <&axi_vdma_0 0>;
                dma-names = "dma0";
                
                /* xlnx,vtc = <&v_tc_0>; */
                /* dglnt,edid-i2c = <&i2c1 >; */
                
                xlnx,vformat = "XR24";
                xlnx,bridge = <&vtc_out>;
                port@0 {
                    pl_disp_ep: endpoint {
                        remote-endpoint = <&hdmi_ep>;
                    };
                };
            };
		};
	};
};

Is my code writing method correct? Regular Petalinx can directly modify the PL device tree, but the PYNQ sdbuild process removed the PL device tree. There aren’t enough specific examples to show me how to handle this difference.

I think if the Digilent HDMI driver requires the VDMA IP information, then VDMA should be included in the device tree. Pynq does not automatically handle these tasks. Am I correct in my understanding?