m0/model/m0.sml

488 val count = ref (0): Nat.nat ref
1130     val count = ref 0
1137              then count := (Nat.+((!count),1))
1139     ; (!count)
1386   ( BranchWritePC(BitsN.+(PC (),imm32)); count := (Nat.+((!count),3)) );
1389   ( BXWritePC(R m); count := (Nat.+((!count),3)) );
1397     ; count := (Nat.+((!count),4))
1408     ; count := (Nat.+((!count),3))
1436     ; count := (Nat.+((!count),1))
1448     ( ALUWritePC result; count := (Nat.+((!count),3)) )
1508     ; count := (Nat.+((!count),1))
1515   ; count := (Nat.+((!count),1))
1521   ; count := (Nat.+((!count),1))
1533     ; count := (Nat.+((!count),1))
1546     ; count := (Nat.+((!count),1))
1559     ; count := (Nat.+((!count),1))
1573     ( write'R(data,t); IncPC (); count := (Nat.+((!count),2)) )
1583     ; count := (Nat.+((!count),2))
1599     ; count := (Nat.+((!count),2))
1615     ; count := (Nat.+((!count),2))
1641                ; count := (Nat.+(Nat.+((!count),bitcount),4))
1643         else ( IncPC (); count := (Nat.+(Nat.+((!count),bitcount),1)) )
1666     ; count := (Nat.+((!count),2))
1685     ; count := (Nat.+((!count),2))
1704     ; count := (Nat.+((!count),2))
1740       ; count := (Nat.+(Nat.+((!count),bitcount),1))
1770       ; count := (Nat.+(Nat.+((!count),bitcount),1))
1776   ( CallSupervisor (); count := (Nat.+((!count),0)) );
1783   ; count := (Nat.+((!count),1))
1844   ; count := (Nat.+((!count),4))
1895     ; count := (Nat.+((!count),4))
1901 fun dfn'NoOperation () = ( IncPC (); count := (Nat.+((!count),1)) );
1903 fun dfn'Breakpoint imm32 = ( IncPC (); count := (Nat.+((!count),0)) );
1906   ( IncPC (); count := (Nat.+((!count),4)) );
1909   ( IncPC (); count := (Nat.+((!count),4)) );
1912   ( IncPC (); count := (Nat.+((!count),4)) );
1914 fun dfn'SendEvent () = ( IncPC (); count := (Nat.+((!count),1)) );
1916 fun dfn'WaitForEvent () = ( IncPC (); count := (Nat.+((!count),2)) );
1918 fun dfn'WaitForInterrupt () = ( IncPC (); count := (Nat.+((!count),2)) );
1920 fun dfn'Yield () = ( IncPC (); count := (Nat.+((!count),1)) );