[r9550684]

don't forget that besides microcode much of the lisp machine logic was implemented with PALs, which were themselves programmed in Lisp. the simple gates, mixers and flip-flops were describe with lisp code, so that the logic could be tested on the lisp machine. I don't know if they built the test tables using the lisp code, or wrote them out manually, but you essentially had multiple sources of truth that could be mutually verified: lisp code, test tables, and the behavior of the specific PAL.