In developing a microprogrammed control unit for a processor, it is important to prove the correctness of the microprogram. In order to validate microprogram through testing, methodology for selecting test data is needed.
In this thesis, an automated test data generation system is implemented. This system symbolically executes microprogram and extracts path condition for a given path, and generates test data by solving path conditions. To generate test data using symbolic execution, only linear path condition is allowed. But bitwise logical operators, which appear frequently in the microprogram, are not linear. In this thesis, the linearization methods are proposed which transform bitwise logical operators into linear forms, and these methods are proved correct.
