FermaT is an industrial strength program transformation system targeted at reverse engineering, program comprehension and migration between programming languages. The system is currently being used in several migration projects to translate IBM 370 Assembler modules into equivalent readable and maintainable C and COBOL programs.
With some user intervention, it is possible to transform all the way to specifications (as expressed in the WSL language; see Figure 1).
The technology is available commercially through the company Software Migrations Limited. They seem to offer migrations and analysis from embedded assembly language code (in addition to the original IBM 370 assembly language).
The FermaT transformation engine is free software avaiable under the GPL license. This allows the transformation of WSL (Wide Spectrum Language) code to other WSL code (but you still need to translate your programs into and out of the WSL language). The SML web page indicates that evaluation versions of the FermaT Assembler Comprehension Workbench are available (but not the migration engine, which translates assembly language to WSL, and WSL to C or COBOL).
See http://www.dur.ac.uk/martin.ward.
Figure 1. An example specification in WSL.
From "Reverse Engineering from Assembler to Formal Specifications via Program Transformations", Proc. WCRE2000
(see Martin Ward's papers).