It’s certainly possible, though it comes with a different set of challenges to software verification. Here’s a recent paper in this direction, proving the correctness of a RISC-V CPU: http://plv.csail.mit.edu/kami/papers/icfp17.pdf
Polyhedral optimisation is cool (Facebook has been using it to great effect for ML kernels recently [1]), but it’s not the end of the story. It’s complementary to this paper, which seems to be about learning an effective and transferrable cost model to guide the optimisation process (you could use that learned cost model in a polyhedral optimiser).
Running on a Zedboard is quite well documented; only took me a couple of hours to do it from scratch following their instructions: https://github.com/ucb-bar/fpga-zynq
Intel last year released a preview of their Control-flow Enforcement Technology instructions, which appear to implement these proposed extensions (shadow stack + indirect branch tracking): https://software.intel.com/sites/default/files/managed/4d/2a...