(* ********************************************************************** *)
(* Progetto FreeScale *)
(* *)
-(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *)
-(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Ultima modifica: 05/08/2009 *)
(* *)
(* ********************************************************************** *)
include "freescale/memory_abs.ma".
include "freescale/opcode_base.ma".
-include "freescale/prod.ma".
(* *********************************** *)
(* STATUS INTERNO DEL PROCESSORE (ALU) *)
| Some c1' ⇒ match c2 with
[ None ⇒ false | Some c2' ⇒ (eq_b8 (fst5T … c1') (fst5T … c2')) ⊗
(eq_anyop m (snd5T … c1') (snd5T … c2')) ⊗
- (eq_instrmode (thd5T … c1') (thd5T … c2')) ⊗
+ (eq_im (thd5T … c1') (thd5T … c2')) ⊗
(eq_b8 (frth5T … c1') (frth5T … c2')) ⊗
(eq_w16 (ffth5T … c1') (ffth5T … c2')) ]
].