port-full/tamarack2/tamarackScript.sml

87           (mem,mar,pc,acc,ir,arg,buf)) =
98             REG ((warg,gnd,bus,bus,arg),P) /\
99             ALU (n+3) (alu0,alu1,arg,bus,alu) /\
189          `Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) =
199               (mem,mar,pc,acc,ir,arg,buf))`;
321 ``!n mpc mem mar pc acc ir arg buf.
322   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
334 ``!n mpc mem mar pc acc ir arg buf.
335   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
347 ``!n mpc mem mar pc acc ir arg buf.
348   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
363 ``!n mpc mem mar pc acc ir arg buf.
364   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
375 ``!n mpc mem mar pc acc ir arg buf.
376   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
388 ``!n mpc mem mar pc acc ir arg buf.
389   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
393     ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) =
401 ``!n mpc mem mar pc acc ir arg buf.
402   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
406     ((mpc (t+1),mem (t+1),mar (t+1),pc (t+1),acc (t+1),arg (t+1)) =
414 ``!n mpc mem mar pc acc ir arg buf.
415   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
427 ``!n mpc mem mar pc acc ir arg buf.
428   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
440 ``!n mpc mem mar pc acc ir arg buf.
441   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
454 ``!n mpc mem mar pc acc ir arg buf.
455   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
467 ``!n mpc mem mar pc acc ir arg buf.
468   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
480 ``!n mpc mem mar pc acc ir arg buf.
481   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
487       ADDn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``,
494 ``!n mpc mem mar pc acc ir arg buf.
495   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
501       SUBn (n+3) (arg t,mem t (Bits (0,n) (mar t)))))``,
507 ``!n mpc mem mar pc acc ir arg buf.
508   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
519 ``!n mpc mem mar pc acc ir arg buf.
520   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
536    ``!n mpc mem mar pc acc ir arg buf.
537           Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) <=>
543                 (arg (t + 1) = arg t) /\
544                 (buf (t + 1) = ADDn (n + 3) (arg t,mar (t + 1)))
550                 (arg (t + 1) = arg t) /\
552                  ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t))))
557                 (mar (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\
558                 (buf (t + 1) = ADDn (n + 3) (arg t,mar (t + 1)))
563                 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\
564                 ?bus. buf (t + 1) = ADDn (n + 3) (arg t,bus)
569                 (arg (t + 1) = arg t) /\
570                 (buf (t + 1) = ADDn (n + 3) (arg t,pc (t + 1)))
575                 (arg (t + 1) = acc t) /\
576                 (buf (t + 1) = ADDn (n + 3) (arg t,acc t))
581                 (arg (t + 1) = acc t) /\
582                 (buf (t + 1) = ADDn (n + 3) (arg t,acc t))
587                 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\
589                  ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t))))
595                 (arg (t + 1) = arg t) /\
596                 (buf (t + 1) = ADDn (n + 3) (arg t,acc t))
601                 (arg (t + 1) = arg t) /\
602                 ?bus. buf (t + 1) = ADDn (n + 3) (arg t, bus)
607                 (arg (t + 1) = arg t) /\ (buf (t + 1) = INCn (n + 3) (pc t))
611                 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\
612                 (buf (t + 1) = ADDn (n + 3) (arg t,pc (t + 1))) /\
618                 (arg (t + 1) = arg t) /\
620                  ADDn (n + 3) (arg t,mem t (Bits (0,n) (mar t))))
625                 (arg (t + 1) = arg t) /\
627                  SUBn (n + 3) (arg t,mem t (Bits (0,n) (mar t))))
631                 (ir (t + 1) = ir t) /\ (arg (t + 1) = arg t) /\
632                 (buf (t + 1) = ADDn (n + 3) (arg t,acc (t + 1))) /\
638                 (arg (t + 1) = arg t) /\
639                 ?bus. buf (t + 1) = ADDn (n + 3) (arg t,bus)``,
690 ``!n mpc mem mar pc acc ir arg buf.
691   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
707 ``!n mpc mem mar pc acc ir arg buf.
708   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
724 ``!n mpc mem mar pc acc ir arg buf.
725   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
740 ``!n mpc mem mar pc acc ir arg buf.
741   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
757 ``!n mpc mem mar pc acc ir arg buf.
758   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
774 ``!n mpc mem mar pc acc ir arg buf.
775   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
791 ``!n mpc mem mar pc acc ir arg buf.
792   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
808 ``!n mpc mem mar pc acc ir arg buf.
809   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
825 ``!n mpc mem mar pc acc ir arg buf.
826   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
864 ``!n mpc mem mar pc acc ir arg buf.
865   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf)
896 ``!n mpc mem mar pc acc ir arg buf.
897   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) /\
909 ``!n mpc mem mar pc acc ir arg buf.
910   Tamarack n (mpc,mem,mar,pc,acc,ir,arg,buf) /\