How to write an awk script that catch ping's time

In this line:

Reply from 10.11.12.13 time=1035ms

how to write an awk script which brings out just 1035.

You can use for example:

ping host | awk 'BEGIN {FS="[=]|[ ]"} {print $11}'

or, better to stop ping after sending one or more packets:

ping -c 1 host | awk 'BEGIN {FS="[=]|[ ]"} NR==2 {print $11}'

or

ping -c 5 host | awk 'BEGIN {FS="[=]|[ ]"} NR>=2&&NR<=6 {print $11}'

If you refer at this string: "Reply from 10.11.12.13 time=1035ms" and not at the output of ping command, you can use:

echo "Reply from 10.11.12.13 time=1035ms" | awk 'BEGIN {FS="[=]|ms"} {print $2}'

Assuming the time is always reported in milliseconds:

$ echo "Reply from 10.11.12.13 time=1035ms" | grep -oP '\d+(?=ms)'
1035

Using GNU awk, print the digits after the first =:

gawk 'match($0, /=([[:digit:]]+)/, a) {print a[1]}'