case PPC6xx_INPUT_CKSTP_IN:
             /* Level sensitive - active low */
             /* XXX: TODO: relay the signal to CKSTP_OUT pin */
+            /* XXX: Note that the only way to restart the CPU is to reset it */
             if (level) {
 #if defined(PPC_DEBUG_IRQ)
                 if (loglevel & CPU_LOG_INT) {
                 }
 #endif
                 env->halted = 1;
-            } else {
-#if defined(PPC_DEBUG_IRQ)
-                if (loglevel & CPU_LOG_INT) {
-                    fprintf(logfile, "%s: restart the CPU\n", __func__);
-                }
-#endif
-                env->halted = 0;
             }
             break;
         case PPC6xx_INPUT_HRESET:
 
         goto store_next;
     case POWERPC_EXCP_MCHECK:    /* Machine check exception                  */
         if (msr_me == 0) {
-            /* Machine check exception is not enabled */
-            /* XXX: we may just stop the processor here, to allow debugging */
-            excp = POWERPC_EXCP_RESET;
-            goto excp_reset;
+            /* Machine check exception is not enabled.
+             * Enter checkstop state.
+             */
+            if (loglevel != 0) {
+                fprintf(logfile, "Machine check while not allowed. "
+                        "Entering checkstop state\n");
+            } else {
+                fprintf(stderr, "Machine check while not allowed. "
+                        "Entering checkstop state\n");
+            }
+            env->halted = 1;
+            env->interrupt_request |= CPU_INTERRUPT_EXITTB;
         }
         msr_ri = 0;
         msr_me = 0;
 #if defined(TARGET_PPC64H)
         msr_hv = 1;
 #endif
-    excp_reset:
         goto store_next;
 #if defined(TARGET_PPC64)
     case POWERPC_EXCP_DSEG:      /* Data segment exception                   */