if you used a 16bit timer interrupt (say the timer is preloaded with (65536 -7 -10000 )) and its clock source the 10mhz osc that would give you a 1khz signal .
if that was incremented into a word var and subtracted from 1000 on an edge signal of the pps you would then have a + or minus error signal .
but how you could use that error to vary the vco is another story and would the resolution be fine enough ?