The PCI example illustrates how zerolength 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 ]
 (E1) 
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 ]
 (E2) 
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 ]
 (E3) 
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 ] )
 (E4) 
The table below summarizes the total time and memory consumption for
these computations (with the f flag):
 NuSMV  TSMV 
 time  memory  time  memory 
(E1)  213.71 sec.  21192 KB  188.90 sec.  33328 KB 
(E2)    69.59 sec.  24340 KB 
(E3)    306.74 sec.  31780 KB 
(E4)    13.56 sec.  33900 KB 
Download model files
Bibliography
[CCMM95] 
Sergio Campos, Edmund Clarke, Wilfredo Marrero and Marius Minea.
Verifying the performance of the PCI local bus using symbolic techniques.
In Proc. of the 1995 International Conference on Computer Design (ICCD '95),
Austin, TX, USA, October 1995, IEEE Computer Society, 1995. 
[MS03] 
Nicolas Markey and Philippe Schnoebelen.
Symbolic
Model Checking of SimplyTimed Systems.
Research Report LSV0314, Lab. Specification and Verification, ENS de Cachan, Cachan, France, October
2003.

