In dieser Arbeit wird ein in SystemC modellierter Mikroprozessor inklusive seines Befehlssatzes vollständig formal verifiziert. Dadurch kann die korrekte Ab- arbeitung von Assemblerprogrammen auf dem Mikroprozessor sichergestellt werden. Durch die Verwendung eines SystemC Modells wird der kombinierte Hardware/Software Entwurfsprozess drastisch vereinfacht.