• Lookup Processor -- the old idea

Lookup Processor -- the old idea

Author: Vojtech Rehak
"lup_with_SRAM.smv" models an idea of sharing SRAM and CAM by four lookup processors. The model is designed for and verified in the NuSMV model checker. More detailed information can be found at the following address: http://www.cesnet.cz/doc/techzpravy/2003/combo6-header-lookups/.

VHDL source list from CVS: liberouter/ver/models/lup_with_SRAM/ (date: 2004-04-27)

Preconditions

English description: Our model consists of five synchronous modules---four lookup processors and a "timer". The "timer" counts time slots (each is 10 ns long in reality) modulo 4 in variable "time". Lookup processors "lup0", "lup1", "lup2", and "lup3" simulate four lookup processors sharing CAM and SRAM. Each lookup processor can be in one of six states; a processor can change state only when the variable "time" is equal to its rank. Meaning and behavior of each state is as follows: The "sleep" state simulates behavior of a processor with empty input buffer. Subsequent state depends on whether any packet comes and whether CAM is not in use by another machine. If no packet comes then the lookup processor remains in "sleep" else lookup processor changes to "wait" or "load_data" state. The choice of "wait" or "load_data" depends on whether CAM is in use by another machine or not. The processor is in "wait" state if it wants to start processing of a packet but CAM is busy. Remaining in "wait" depends on availability of CAM. If CAM is free, the next state is "load_data". The "load_data" state represents the critical section of CAM sharing---loading data into CAM. The next state is "latency1". States "latency1" and "latency2" represent only waiting for result. In addition, "latency2" includes the finishing SRAM time slot. "Latency2" is followed by a sequence of "comp" states. The "comp" states simulate computation using SRAM. A "comp" state corresponds to performing one instruction; in the end of the processing SRAM is accessed. The number of instructions is not limited. It is obvious that the next states are "comp", "sleep", "wait", and "load_data". We abstract away from the emptiness of the input buffer and the number of instructions in computation using SRAM. It means that each decision based on that features is replaced by a non-deterministic choice. There are no restrictions on the choice. The described (and verified) model is therefore a bit more general than reality. It allows the input buffer to be empty forever or even to stay in "comp" states infinitely.

Formulas

Mutual exclusion of SRAM accesses

AG (!(lup0.SRAM_used & lup1.SRAM_used |
      lup0.SRAM_used & lup2.SRAM_used |
      lup0.SRAM_used & lup3.SRAM_used |
      lup1.SRAM_used & lup2.SRAM_used |
      lup1.SRAM_used & lup3.SRAM_used |
      lup2.SRAM_used & lup3.SRAM_used))
	

Assert globally that no pair of lups accesses SRAM at the same time.

Verified in 0.1 s.

Mutual exclusion of accesses to CAM

AG (!(lup0.state = load_data & lup1.state = load_data |
      lup0.state = load_data & lup2.state = load_data |
      lup0.state = load_data & lup3.state = load_data |
      lup1.state = load_data & lup2.state = load_data |
      lup1.state = load_data & lup3.state = load_data |
      lup2.state = load_data & lup3.state = load_data))
		      

Assert globally that no pair of lups accesses CAM at the same time.

Verified in 0.1 s.

Correctness of CAM_busy

AG (CAM_busy <-> ( lup0.state = load_data | lup1.state = load_data |
                   lup2.state = load_data | lup3.state = load_data  ) )
        

Correctness of CAM_busy.

Verified in 0.1 s.

Fairness of using CAM (no starving, no blocking)

G ((lup0.state = wait -> F lup0.state = load_data) &
   (lup1.state = wait -> F lup1.state = load_data) &
   (lup2.state = wait -> F lup2.state = load_data) &
   (lup3.state = wait -> F lup3.state = load_data))
        

Assert globally for each lup that if the machine is in wait state then it will reach load_data sometimes.

Verified in 0.1 s.

Maximal length of waiting

COMPUTE
  MAX [ lup0.state = wait , lup0.state = load_data ]
COMPUTE
  MAX [ lup1.state = wait , lup1.state = load_data ]
COMPUTE
  MAX [ lup2.state = wait , lup2.state = load_data ]
COMPUTE
  MAX [ lup3.state = wait , lup3.state = load_data ]
        

The maximal length of waiting for the CAM access.

The results of computations are equal to 12 for all cases.

Verified in 0.1 s.

The longest waiting for the CAM access

AG (!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait) |
    AX(!(lup0.state = wait)
    ))))))))))))
        

The verification generates the longest waiting for the CAM access as a counterexample.

Verified in 0.1 s.