Not sure if you'll see this, but I did run across a preprint with a few Rockwell authors that might be of interest, "Development of a Translator from LLVM to ACL2" (http://arxiv.org/abs/1406.1566)
Still added it to my collection as it might come in handy for future ACL2 work. :)