The PCI example illustrates how zero-length durations can be used for counting only special kind of steps [MS03].

The PCI Local bus example

A model of the PCI local bus was analyzed by Campos et al. in [CCMM95], computing minimum and maximum delays with symbolic model checking techniques. This model is one of the standard NuSMV examples (we take pci4p.smv as a basis in the sequel). We refer to [CCMM95] for more explanations on this case study. The reader only needs to know that it is a large example where nuSMV can show that a complete transaction might take up to 244 steps, from the request of the bus to the end of the transaction.

The PCI example using TSMV

First of all, we assume duration 1 on all transitions. In that case, we are able to prove the aforementioned maximal time for a complete transaction, by adding the following lines to the main module of the PCI model:

	VAR  duration: 0..1;
	INIT  duration=0
	TRANS  next(duration)=1
	COMPUTE MAX[ req0, isa_bridge.end_transaction ]
	COMPUTE MAX[ req1, scsi_ctrl.end_transaction ]
	COMPUTE MAX[ req2, vga_ctrl.end_transaction ]
	COMPUTE MAX[ req4, processor.end_transaction ]

For the isa_bridge+ and scsi_ctrl components, the result is 244. It is 130 for the other two components (see explanations for this difference in [CCMM95]).

It is also possible to count specific kinds of events. For instance, we compute the number of transactions issued on the PCI bus between a request and a grant of each of the masters. This is achieved by the following lines:

	DEFINE start_tr := processor.start_transaction | 
			vga_ctrl.start_transaction | 
			scsi_ctrl.start_transaction |
			isa_bridge.start_transaction ;
	VAR  duration: 0..1;
	INIT  duration=0
	TRANS  
	  next(duration)=case
		start_tr: 1;
		1        : 0;
	  esac

	COMPUTE MAX[ req0, grant=0 ]
	COMPUTE MAX[ req1, grant=1 ]
	COMPUTE MAX[ req2, grant=2 ]
	COMPUTE MAX[ req4, grant=4 ]

TSMV answers that up to 5 transactions might start between request and grant for both the isa_bridge and the scsi_ctrl components, and 2 for the other two masters. These are the values given in [CCMM95], where they were obtained with a special condition counting algorithm.

We also counted the amount of data the processor can transfer between a request and its corresponding grant, with the following lines:

in module bus_master
	VAR transmitting: boolean;
	ASSIGN 
		init(transmitting) := FALSE;
		next(transmitting) := (count>next(count));
in module main
	VAR  duration: 0..1;
	INIT  duration=0
	TRANS  next(duration)=case
		processor.transmitting	: 1;
		1			: 0;
	esac

	COMPUTE MAX[ req0, grant=0 ]
	COMPUTE MAX[ req1, grant=1 ]
	COMPUTE MAX[ req2, grant=2 ]
	COMPUTE MAX[ req4, grant=4 ]

The result is 30 for the isa_bridge, the scsi_ctrl and the vga_ctrl, and 15 for the processor (the total amount of data that a master can transmit in one ``session'' is limited to 15 in this model). Last, we verify that, when a transaction is aborted, the component has to request for the bus before being able to transmit anew. We verify this property for the processor by counting only data transfers of the processor, and specifying that, after abortion, he can transmit at most one ``bit'' of data if he does not assert a new grant. This is achieved with the following additions to pci4p.smv:

in module bus_master
        VAR transmitting: boolean;
        ASSIGN
                init(transmitting) := FALSE;
                next(transmitting) := (count>next(count));
in module main
        VAR  duration: 0..1;
        INIT  duration=0
        TRANS  next(duration)=case
                processor.transmitting  : 1;
                1                       : 0;
        esac

	SPEC 
	  AG ((processor.transmitting & abort) -> !E [ (!req4) U>=2 TRUE ] )
	SPEC 
	  EF ((processor.transmitting & abort) ->  E [ (!req4) U= 1 TRUE ] )
	SPEC
	  EF ((processor.transmitting & abort) ->  E [ (!req4) U= 0 TRUE ] )

The table below summarizes the total time and memory consumption for these computations (with the -f flag):

Download model files

• the TSMV file for (E1)
• the TSMV file for (E2)
• the TSMV file for (E3)
• the TSMV file for (E4)
• the NuSMV pci4p model

Bibliography