instruction reordering in vellvm

​Hi.
I understand from [1] (part 4.4) that instruction reordering is verified in vellvm.
I download vellvm, but I dont know where instruction reordering has considered. And I would like to apply just that to my input.
Can anyone help me? I am unfamiliar with coq and newbie in formal methods.

[1] http://www.cis.upenn.edu/~stevez/papers/ZNMZ12.pdf