-- -- Model for the PCI Bus protocol -- -- Sergio Campos -- 02/95 -- -- -- Modified by N. Markey, 10/2003 -- ------------------------------------------------------------------------- -- -- Latency model for the PCI bus: -- -- REQ GNT FRAME TRDY -- |--------------|--------------------|-----------------|----------> -- <------------> <------------------> <---------------> -- Arbitration Bus acquisition Target latency -- latency latency -- ------------------------------------------------------------------------- ------------------------------------------------------------------------- -- -- Arbiter -- -- -- FP RR FP = Fixed Priority -- v v RR = Round Robin -- +---------+ -- SIOREQ ->|0 | -- REQ0 ->|1 Bank 0 |----+ -- +---------+ | -- | FP RR -- FP RR | v v -- v v | +----------+ -- +---------+ +--->|00 | -- REQ1 ->|0 | | | -- REQ2 ->|1 Bank 3 |-------->|01 Bank 2 |---> -- +---------+ | | -- +--->|10 | -- FP RR | +----------+ -- v v | -- +---------+ | -- CPUREQ ->|0 | | -- REQ3 ->|1 Bank 1 |----+ -- +---------+ -- MODULE arb_bank_2in(req0, req1, policy, grant, granted, change_now) -- see use of granted in assignment to last. VAR last: {0, 1}; DEFINE grant := case policy = FP: case req0: 0; req1: 1; 1: idle; esac; policy = RR: case last = 0: case req1: 1; req0: 0; 1: idle; esac; last = 1: case req0: 0; req1: 1; 1: idle; esac; esac; esac; ASSIGN init(last) := 0; next(last) := case !granted | !change_now: last; grant = 0: 0; grant = 1: 1; 1: last; esac; --SPEC AG(req1 -> A[req1 U (grant = 1 | req0)]) --SPEC AG(req0 -> A[req0 U grant = 0]) --SPEC AG((req1 & policy = RR) -> A[req1 U grant = 1]) MODULE arb_bank_3in(req0, req1, req2, policy, grant, change_now) VAR last: {0, 1, 2}; DEFINE grant := case policy = FP: case req0: 0; req1: 1; req2: 2; 1: idle; esac; policy = RR: case last = 0: case req1: 1; req2: 2; req0: 0; 1: idle; esac; last = 1: case req2: 2; req0: 0; req1: 1; 1: idle; esac; last = 2: case req0: 0; req1: 1; req2: 2; 1: idle; esac; esac; esac; ASSIGN init(last) := 0; next(last) := case !change_now: last; grant = 0: 0; grant = 1: 1; grant = 2: 2; 1: last; esac; --SPEC AG(req1 -> A[req1 U (grant = 1 | req0)]) --SPEC AG(req2 -> A[req2 U (grant = 2 | req0 | req1)]) MODULE arbiter(req0, req1, req2, req3, req4, req5, grant, b_frame_switch) VAR policy0: {FP, RR}; policy1: {FP, RR}; policy2: {FP, RR}; policy3: {FP, RR}; bank0: arb_bank_2in(req0, req1, policy0, grant0, (grant2 = 0), change_now); bank1: arb_bank_2in(req2, req3, policy1, grant1, (grant2 = 1), change_now); bank2: arb_bank_3in(reqbank0, reqbank1, reqbank3, policy2, grant2, change_now); bank3: arb_bank_2in(req4, req5, policy3, grant3, (grant2 = 2), change_now); grant: {0, 1, 2, 3, 4, 5, idle}; DEFINE reqbank0 := !(grant0 = idle); reqbank1 := !(grant1 = idle); reqbank3 := !(grant3 = idle); change_now := !(!b_frame_switch & !grant = idle); ASSIGN init(grant) := idle; next(grant) := case !b_frame_switch & !grant = idle: grant; -- only change grant when b_frame goes up. -- except when the bus is idle. grant2 = idle: idle; grant2 = 0: case grant0 = 0: 0; 1: 1; esac; grant2 = 1: case grant1 = 0: 2; 1: 3; esac; grant2 = 2: case grant3 = 0: 4; 1: 5; esac; esac; init(policy0) := RR; init(policy1) := RR; init(policy2) := RR; init(policy3) := RR; -- Policies can start in any configuration, but they don't change. next(policy0) := policy0; next(policy1) := policy1; next(policy2) := policy2; next(policy3) := policy3; ------------------------------------------------------------------------- -- -- Bus master is the access unit to the bus. It requests bus access, and -- upon being granted the bus, issues transactions. -- -- Bus signals are: -- -- frame: asserted at the beginning of the transaction (address phase), and -- deasserted when the transaction is finished. -- ad: address/data lines -- c_bd: bus command and byte enable - determines the transaction -- irdy: indicates that bus master is ready to complete the data phase. -- During write means data is ready; during read means ready to accept. -- trdy: indicates that bus target is ready to complete the data phase. -- The data phase is completed when (irdy & trdy). Wait cycles are -- inserted until then. -- -- req: request for bus access -- gnt: bus grant -- MODULE bus_master(-- in parameter: id, b_frame_switch, abort, abort_count, -- out parameters, values sent to the bus: ad, c_bd, frame, irdy, trdy, req, -- values received from the bus: b_gnt, b_c_bd, b_frame, b_irdy, b_trdy) VAR req: boolean; state: {idle, address, data}; count: 0..15; -- counts how many cache lines -- will be sent (or received). c_bd: {IDLE, MEM_READ, MEM_WRITE}; irdy: boolean; trdy: boolean; issue_next: boolean; -- true when a transaction will be requested in the -- next state (if not in progress already); DEFINE ad := 0; bus_idle := !b_frame & !b_irdy; -- transaction starts at -- the next clock cycle. start_transaction := b_gnt & bus_idle; -- transaction ends when -- all data has been sent. end_transaction := (state = data) & (count = 0); frame := (state = address) | ((state = data) & (count > 0)); ASSIGN init(req) := 0; next(req) := case frame & abort: 1; !req: case issue_next: 1; !issue_next: 0; esac; req: case b_gnt: 0; 1: 1; esac; esac; init(state) := idle; next(state) := case abort: idle; state = idle: case !start_transaction: idle; 1: address; -- just been granted the bus, -- start a new transaction. esac; state = address: data; state = data: case count = 0: idle; -- count to see if all data 1: data; -- has been sent. esac; esac; init(count) := 0; next(count) := case abort: 0; start_transaction: { 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15}; end_transaction: 0; !state = data: count; -- sends data only in data state !b_trdy: count; -- and only if target is ready count > 0: count - 1; 1: count; esac; init(c_bd) := IDLE; next(c_bd) := case abort: IDLE; start_transaction: {MEM_READ, MEM_WRITE}; -- Actual values are:{IO_READ, IO_WRITE, MEM_READ, -- MEM_WRITE, MEM_READ_MULT, MEM_READ_LINE, -- MEM_WRITE_INV}; end_transaction: IDLE; 1: c_bd; esac; init(irdy) := 0; next(irdy) := case abort: 0; state = address: 1; end_transaction: 0; 1: irdy; esac; init(trdy) := 0; next(trdy) := case abort: 0; !state = idle: 0; -- we don't assert trdy -- if we are the master. !trdy: case -- conditions for assertion b_c_bd = MEM_READ & b_irdy: 1; -- the condition above asserts -- one cycle after irdy, -- creating a turnaround cycle b_c_bd = MEM_WRITE & b_frame: 1; -- the condition above asserts -- at the same cycle at irdy, -- no turnaround cycle 1: 0; esac; trdy: case -- conditions for deassertion b_frame: 1; 1: 0; -- reset at end of trans. esac; esac; VAR transmitting: boolean; ASSIGN init(transmitting) := FALSE; next(transmitting) := (count>next(count)); -- -- Checks consistency of transactions -- -- -- Are [start,end]_transaction well defined ? -- --SPEC AG(start_transaction -> AX !start_transaction) --SPEC AG(start_transaction -> AX state = address) --SPEC AG(end_transaction -> AX !end_transaction) --SPEC AG(end_transaction -> AX state = idle) --SPEC AG(start_transaction -> AF end_transaction) --COMPUTE MIN[start_transaction, end_transaction] --COMPUTE MAX[start_transaction, end_transaction] --SPEC AG((!req & issue_next) -> AX req) -- spec below is false for low priority processes --SPEC AG((!req & issue_next & !b_gnt) -> AF b_gnt) ------------------------------------------------------------------------- -- -- Computes arbitration latency (see latency model) -- --COMPUTE MIN[req & !b_gnt, b_gnt & !frame] --COMPUTE MAX[req & !b_gnt, b_gnt & !frame] --COMPUTE MIN[!req & issue_next & !b_gnt, b_gnt] --COMPUTE MAX[!req & issue_next & !b_gnt, b_gnt] ------------------------------------------------------------------------- --SPEC AG(req & !b_gnt -> AF b_gnt) ------------------------------------------------------------------------- -- -- Computes bus acquisition latency (see latency model) -- --COMPUTE MIN[b_gnt & !frame, frame & b_frame_switch] --COMPUTE MAX[b_gnt & !frame, frame & b_frame_switch] --COMPUTE MIN[b_gnt & !frame, frame & b_frame_switch] --COMPUTE MAX[b_gnt & !frame, frame & b_frame_switch] ------------------------------------------------------------------------- --SPEC AG((b_gnt & !frame) -> AF frame) ------------------------------------------------------------------------- -- -- Computes target latency -- --COMPUTE MIN[frame & b_frame_switch, b_trdy] --COMPUTE MAX[frame & b_frame_switch, b_trdy] ------------------------------------------------------------------------- ------------------------------------------------------------------------- -- -- Computes maximum data transfer time. -- not very interesting, since it is the amount of data sent in a -- transaction, but stated for completeness. -- --DEFINE -- b_trdy_next := !b_trdy & b_c_bd = MEM_READ & b_irdy | -- !b_trdy & b_c_bd = MEM_WRITE & b_frame; --COMPUTE MIN[b_trdy_next & frame, end_transaction] --COMPUTE MAX[b_trdy_next & frame, end_transaction] --SPEC AG(b_trdy_next & frame -> AF end_transaction) --SPEC AG(b_trdy_next & !abort -> AX b_trdy) ------------------------------------------------------------------------- ------------------------------------------------------------------------- -- -- Computes maximum transaction time, even if abortion occurs -- --COMPUTE MIN[start_transaction, end_transaction] --COMPUTE MAX[start_transaction, end_transaction] ------------------------------------------------------------------------- --SPEC AG(start_transaction -> AF end_transaction) --SPEC AG(start_transaction & id = 0 -> ABG 18..18 !end_transaction) ------------------------------------------------------------------------- -- -- Bus master null implements an empty slot. basically sets req to 0. -- MODULE bus_master_null(-- in parameters: id, b_frame_switch, abort, abort_count, -- out parameters, values sent to the bus: ad, c_bd, frame, irdy, trdy, req, -- values received from the bus: b_gnt, b_c_bd, b_frame, b_irdy, b_trdy) DEFINE c_bd := 0; ad := 0; frame := 0; irdy := 0; trdy := 0; req := 0; ------------------------------------------------------------------------- MODULE main VAR arb: arbiter(req0, req1, req2, req3, req4, req5, grant, b_frame_switch); isa_bridge: bus_master(0, b_frame_switch, abort, abort_count, ad0, c_bd0, frame0, irdy0, trdy0, req0, (grant = 0), b_c_bd, b_frame, b_irdy, b_trdy); scsi_ctrl: bus_master(1, b_frame_switch, abort, abort_count, ad1, c_bd1, frame1, irdy1, trdy1, req1, (grant = 1), b_c_bd, b_frame, b_irdy, b_trdy); vga_ctrl: bus_master(2, b_frame_switch, abort, abort_count, ad2, c_bd2, frame2, irdy2, trdy2, req2, (grant = 2), b_c_bd, b_frame, b_irdy, b_trdy); slot0: bus_master_null(3, b_frame_switch, abort, abort_count, ad3, c_bd3, frame3, irdy3, trdy3, req3, (grant = 3), b_c_bd, b_frame, b_irdy, b_trdy); processor: bus_master(4, b_frame_switch, abort, abort_count, ad4, c_bd4, frame4, irdy4, trdy4, req4, (grant = 4), b_c_bd, b_frame, b_irdy, b_trdy); slot1: bus_master_null(5, b_frame_switch, abort, abort_count, ad5, c_bd5, frame5, irdy5, trdy5, req5, (grant = 5), b_c_bd, b_frame, b_irdy, b_trdy); -- -- Bus signals -- DEFINE b_frame := frame0 | frame1 | frame2 | frame3 | frame4 | frame5; b_irdy := irdy0 | irdy1 | irdy2 | irdy3 | irdy4 | irdy5; b_trdy := trdy0 | trdy1 | trdy2 | trdy3 | trdy4 | trdy5; b_c_bd := case frame0: c_bd0; frame1: c_bd1; frame2: c_bd2; frame3: c_bd3; frame4: c_bd4; 1: c_bd5; esac; bus_idle := !b_frame & !b_irdy; VAR b_frame_old: boolean; ASSIGN init(b_frame_old) := 0; next(b_frame_old) := b_frame; DEFINE b_frame_switch := b_frame & !b_frame_old; --SPEC AG(b_frame_switch -> AX !b_frame_switch) --SPEC AG(b_frame_switch -> b_frame) --SPEC AG(!b_frame -> !b_frame_switch) VAR abort_count: 0..3; abort_random: boolean; ASSIGN init(abort_count) := 0; next(abort_count) := case abort: case abort_count = 3: 3; 1: abort_count + 1; esac; 1: abort_count; esac; DEFINE abort := abort_random & b_frame; -- abort := 0; --TRANS (abort_count = 0) TRANS (abort_count = 0 | abort_count = 1) --TRANS (abort_count = 0 | abort_count = 1 | abort_count = 2) --SPEC AG !abort --SPEC EG abort_count = 0 --SPEC AG !abort_count = 3 ---------------------------------------------------------------------------- -- -- Check correctness of the arbiter -- --DEFINE -- all_FP := (arb.policy0 = FP) & (arb.policy1 = FP) & -- (arb.policy2 = FP) & (arb.policy3 = FP); -- all_RR := (arb.policy0 = RR) & (arb.policy1 = RR) & -- (arb.policy2 = RR) & (arb.policy3 = RR); -- -- If we do a complete RR scheduling, no starvation can occur -- --SPEC AG(req0 -> A[req0 U grant = 0]) -- 0 NEVER starves! --SPEC AG((req1 & all_RR) -> A[req1 U grant = 1]) --SPEC AG((req2 & all_RR) -> A[req2 U grant = 2]) --SPEC AG((req3 & all_RR) -> A[req3 U grant = 3]) --SPEC AG((req4 & all_RR) -> A[req4 U grant = 4]) --SPEC AG((req5 & all_RR) -> A[req5 U grant = 5]) -- -- We don't starve because of processors of lower priority -- --SPEC AG(req1 -> A[req1 U (grant = 1 | req0)]) --SPEC AG(req2 -> A[req2 U (grant = 2 | req0 | req1)]) --SPEC AG(req3 -> A[req3 U (grant = 3 | req0 | req1 | req2)]) --SPEC AG(req4 -> A[req4 U (grant = 4 | req0 | req1 | req2 | req3)]) --SPEC AG(req5 -> A[req5 U (grant = 5 | req0 | req1 | req2 | req3 | req5)]) -- -- What is the maximum time to get the bus (If we eventually get the bus) ? -- --COMPUTE MAX[req0, grant = 0] --COMPUTE MAX[req1 & all_RR, grant = 1] --COMPUTE MAX[req2 & all_RR, grant = 2] --COMPUTE MAX[req3 & all_RR, grant = 3] --COMPUTE MAX[req4 & all_RR, grant = 4] --COMPUTE MAX[req5 & all_RR, grant = 5] -- --------------------------------------------------------------------------- --SPEC AG((processor.start_transaction) -> AG !(scsi_ctrl.end_transaction)) --SPEC AG (isa_bridge.start_transaction -> -- !E[!isa_bridge.end_transaction BU 132..132 isa_bridge.end_transaction]) 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 ] )