/* 
 * 3Com 3c509 - Laddie IO Specification
 * Author: Lea Wittie
 * Copyright (c) 2007 Bucknell University
 *
 * Permission is hereby granted, free of charge, to any individual or
 * institution obtaining a copy of this software and associated
 * documentation files (the "Software"), to use, copy, modify, and
 * distribute without restriction, provided that this copyright and
 * permission notice is maintained, intact, in all copies and supporting
 * documentation.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
 * IN NO EVENT SHALL BUCKNELL UNIVERSITY BE LIABLE FOR ANY CLAIM, DAMAGES
 * OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
 * OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE
 * OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 */

// 3c509 device state
integer Window [0:6]; // device window
integer RxQUsed;  // used space in the Rx queue (that needs to be read)
integer TxQFree;  // free space in the Tx queue (that we can fill)
boolean Busy; // is device busy
boolean InterruptsEnabled;
boolean StatsEnabled;
// Note: RxQUsed and TxQFree are conservative estimates to prevent
// the PIO data read from over or underrunning the FIFO queues

// Command port: write only. takes an argument and a command
// Different commands require different arguments.
// Not all command values are possible.
port  0x0E {
  name = command;
  size = 2;
  access = write;
	  
  // Fields
  [0:10] arg ; 
  [11:15] cmd ;
  enum  {GlobalReset, SelectRegWindow, StartCoaxTransciever, RXDisable,
	 RXEnable, RxReset, RxDiscard=8, TXEnable,
	 TXDisable, TXReset, ReqInterrupt, AcknowledgeInterrupt,SetIntMask, 
	 SetReadZeroMask,
	 SetRXFilter, SetRXEarlyThresh, SetTXAvailThresh, SetTXStartThresh,
	 StatsEnable=21, StatsDisable, StopCoaxTrans, SetTXRecThresh};

  // Usage constraints
  requires Busy==false; // && Wait==0;
  requires switch cmd {
    GlobalReset : arg == 0; // 1ms
    SelectRegWindow : arg>=0 && arg<=6;
    StartCoaxTransciever : arg==0;
    RXDisable : arg==0;
    RXEnable : arg==0;
    RxReset : arg==0;
    RxDiscard : arg==0;
    TXEnable : arg==0;
    TXDisable : arg==0;
    TXReset : arg==0;
    SetIntMask : arg>=0 && arg<129;
    SetReadZeroMask :  arg>=0 && arg<129;	
    SetRXFilter : arg>=0 && arg<15;
    StatsEnable : arg==0;
    StatsDisable : arg==0;
    StopCoaxTrans : arg==0;
  }

  ensures switch cmd {
    GlobalReset : Busy==true;
    SelectRegWindow : Window==arg;
    //StartCoaxTransciever: Wait==old(Wait)+800; // 800us
    //StopCoaxTrans: Wait==old(Wait)+800; // 800us
    RxDiscard : Busy==true;
    TXReset : Busy==true;
    StatsEnable : StatsEnabled==true;
    StatsDisable : StatsEnabled==false;
    SetIntMask : (arg==0 && InterruptsEnabled==false) 
      || (arg!=0 && InterruptsEnabled==true);
  }

  test_input Busy=false, cmd=0, arg=0;
}

port  0x0e{
  name = status;
  size = 2;
  access = read;

  [15:13] win;
  [12]    IP;
  [11:8]  reserved;
  [7]     US;
  [6]     IR;
  [5]     RE;
  [4]     RC;
  [3]     TA;
  [2]     TC;
  [1]     AF;
  [0]     IL;

  ensures {
    Window == win;
    (old(InterruptsEnabled)==false && Busy == IP) 
      || (old(InterruptsEnabled)==true);
    InterruptsEnabled==old(InterruptsEnabled);
  }
  
  test_input InterruptsEnabled=true;
}

port  0x08{
  name = RXStatus;
  size = 2;
  access = read;

  [15]    IC;
  [14]    ER;
  [13:11] code;
  [10:0]  RXbytes;

  requires Window == 1 && Busy==false;     
  ensures RxQUsed == RXbytes;
  test_input Window=1, Busy=false;
}

// manual error pg 6-18, "Writing this register...Read only"
port 0x0B {
  name = TXStatus;
  size = 1;

  [7]   CM;
  [6]   IS;
  [5]   JB;
  [4]   UN;
  [3]   MC;
  [2]   OF;
  [1]   RE;

  requires
    Window == 1 && Busy==false;
  test_input Window=1, Busy=false;
}

port  0x00 {
  name = RXPIODataRead;
  size = 4;
  type = repeated;
  access = read;

  //[0:31] RXPIORead;
  requires Window == 1 && Busy==false && RxQUsed>4*count;
  ensures RxQUsed==old(RxQUsed)-(4*count); 
  // test_input Window=1, Busy=false, RxQUsed=20, count=2;
}

port  0x00 {
  name = TXPIODataWrite;
  size = 4;
  type=repeated;
  access = write;

  //[0:31] TXPIOWrite;
  requires Window == 1 && Busy==false && TxQFree>4*count;
  ensures TxQFree==old(TxQFree)-(4*count);
  // test_input Window=1, Busy=false, RxQUsed=20, count=2;
}

port  0x0A {
  name = FreeRecBytes;
  size = 2;
  access = read;
  [0:14] RXFreebytes;
  requires Window == 3 && Busy==false; 
  // RxFree doesnt help, we need Rx used
  test_input Window=3, Busy=false;
}

port  0x0C {
  name = FreeTransBytes;
  size = 2;
  access = read;
  [0:14] TXFreebytes;
  requires (Window==1 || Window==3) && Busy==false;
  ensures TxQFree == TXFreebytes;
  test_input Window=1, Busy=false;
}

port  0x0A {
  name = Timer;
  size = 1;
  access = read;
  //[0:7] timer;
  requires Window == 1 && Busy==false;
  test_input Window=1, Busy=false;
}

// Statistics Registers
port  0x0C {
  name = TXByteSuccess;
  size = 2;
  requires      Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x0A {
  name = RXByteSuccess;
  size = 2;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x08 {
  name = TransDef;
  size = 1;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x07 {
  name = RXFrameSuccess;
  size = 1;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x06 {
  name = TXFrameSuccess;
  size = 1;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x05 {
  name = RXFrameDiscard;
  size = 1;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x04 {
  name = TXLateCollisions;
  size = 1;
  requires     Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x03 {
  name = TXFramesCollision;
  size = 1;
  [0:4] relevant;
  requires      Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x02 {
  name = TXFramesCollisions;
  size = 1;
  [0:4] relevant;
  requires      Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x01 {
  name = TXFramesNoHB;
  size = 1;
  [0:3] relevant;
  requires      Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

port  0x00 {
  name = CarrierLost;
  size = 1;
  [0:3] relevant;
  requires      Window == 6 && Busy==false && StatsEnabled==false;
  test_input Window=6, Busy=false, StatsEnabled=false;
}

// Diagnostic Registers
port  0x0A {
  name = MediaTypeAndStatus;
  size = 2;

  [15]   TPE;
  [14]   CE;
  [13]   IN;
  [12]   SQ;
  [11]   LB;
  [10]   PL;
  [9]    J;
  [8]    US;
  [7]    LK;
  [6]    JE;
  [5]    CS;
  [4]    CO;
  [3]    SQE;
  [2]    CSD;
  requires      Window == 6 && Busy==false;
  test_input Window=6, Busy=false;
}

port  0x06 {
  name = NetDiag;
  size = 2;
  [15]   EL;
  [14]   ENL;
  [13]   ECL;
  [12]   FL;
  [11]   TXE;
  [10]   RXE;
  [9]    TXT;
  [8]    TXR;
  [7]    SE;
  [5:1]  ASIC;
  [0]    TLD;
  requires     Window == 4 && Busy==false;
  test_input Window=4, Busy=false;
}

port  0x04 {
  name = FIFODiag;
  size = 2;
  [15]   RXR;
  [14]   reserved;
  [13]   RXU;
  [12]   RSO;
  [11]   RXO;
  [10]   TXO;
  [7:0]  RSD;
  requires     Window == 4 && Busy==false;
  test_input Window=4, Busy=false;
}

port  0x08 {
  name = EthernetContStatus;
  size = 2;
  [15]   TXD;
  [14]   TXR;
  [13]   TXU;
  [12]   TXM;
  [11]   TXLate;
  [10]   TXS;
  [9]    TXLCAR;
  [8]    TXE;
  [7]    RXR;
  [6]    RXD;
  [5]    RXFrame;
  [4]    RXO;
  [3]    RXFCS;
  [2]    RXDagain;
  [1]    RXS;
  [0]    RXT;
  requires      Window == 4 && Busy==false;
  test_input Window=4, Busy=false;
}