The derivation of microcode by symbolic execution
John Wade Ulrich · ACM SIGMICRO newsletter/SIGMICRO newsletter/SIGMICRO, TCMICRO newsletter · 1980
Given a description of a computer called the “target” and a micro processor called the “host” we would like to generate a micro program which when executed by the host will simulate the target. We accomplish this by first breaking the target down into a set of small segments. Then, logical conditions for an appropriate microcode are generated for each segment by a combination of symbolic execution and simplification. When completed, the segments are assembled into a working code by solving the set of logical conditions.