-- Copyright (c) 2006 Gabor Madl -- All rights reserved. -- -- Redistribution and use in source and binary forms, with or without -- modification, are permitted provided that the following conditions -- are met: -- 1. Redistributions of source code must retain the above copyright -- notice, this list of conditions and the following disclaimer. -- 2. Redistributions in binary form must reproduce the above copyright -- notice, this list of conditions and the following disclaimer in the -- documentation and/or other materials provided with the distribution. -- 3. The name of the author may not be used to endorse or promote products -- derived from this software without specific prior written permission. -- THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR -- IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES -- OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. -- IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, -- INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT -- NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -- DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -- THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -- (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF -- THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. MODULE main() VAR -- AMBA bus signals captured in the model HTRANS : {IDLE, NONSEQ, BUSY}; BUSREQ1 : boolean; BUSREQ2 : boolean; BUSREQ3 : boolean; HGRANT1 : boolean; HGRANT2 : boolean; HGRANT3 : boolean; START1 : boolean; START2 : boolean; START3 : boolean; START4 : boolean; active : boolean; HMASTER : {master1, master2, master3, default}; MASTER1_STATE : {idle, write, x}; MASTER2_STATE : {idle, write, x}; MASTER3_STATE : {idle, write, x}; TIME : 0..170; -- HW components connected to the bus master1 : master_read_write (BUSREQ1, HGRANT1, MASTER1_STATE, 1, 1, 0, 1, START1, START2); master2 : master_read_write (BUSREQ2, HGRANT2, MASTER2_STATE, 25, 41, 1, 1, START2, START3); master3 : master_read_write (BUSREQ3, HGRANT3, MASTER3_STATE, 87, 95, 1, 1, START3, START4); arbiter : arbiter_round_robin (HTRANS, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, MASTER1_STATE, MASTER2_STATE, MASTER3_STATE); ASSIGN init (TIME) := 0; init (START1) := 1; init (START2) := 0; init (START3) := 0; init (START4) := 0; init (active) := 1; next (START1) := 0; next (active) := case START4 : 0; 1 : active; esac; next (TIME) := case active & TIME < 165 : TIME + 1; 1 : TIME; esac; HTRANS := case HMASTER = master1 : master1.HTRANS; HMASTER = master2 : master2.HTRANS; HMASTER = master3 : master3.HTRANS; HMASTER = default : IDLE; esac; SPEC AG (START4 -> TIME < 170) -- true MODULE master_read_write (BUSREQ, HGRANT, MASTER_STATE, BCET, WCET, READSIZE, WRITESIZE, START, FINISH) VAR state : {idle, busreq, haddr, read, write, busy, error}; io : {read, write}; ET : 0..95; HTRANS : {IDLE, NONSEQ, BUSY}; ASSIGN init (state) := idle; init (io) := read; next (state) := case state = idle & START & READSIZE = 0 : busy; state = idle & START : busreq; state = idle : idle; state = busreq & HGRANT : haddr; state = busreq & !HGRANT : state; state = haddr & HGRANT : read; state = read & HGRANT : write; state = write & HGRANT & io = read : busy; state = write & HGRANT & io = write : idle; state = busy & ET < BCET : busy; state = busy & ET = WCET : busreq; state = busy & BCET <= ET : {busy, busreq}; 1: error; esac; next (io) := case state = busy : write; state = idle : read; 1 : io; esac; next (ET) := case state = busy & ET < WCET : ET + 1; state = idle : 0; 1 : ET; esac; MASTER_STATE := case state = idle : idle; state = write : write; 1 : x; esac; HTRANS := case state = haddr : NONSEQ; state = read : NONSEQ; state = write : NONSEQ; state = busy : BUSY; 1 : IDLE; esac; BUSREQ := case state = busreq : 1; 1 : 0; esac; next (FINISH) := case state = write & HGRANT & io = write : 1; 1 : 0; esac; MODULE arbiter_round_robin (HTRANS, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, MASTER1_STATE, MASTER2_STATE, MASTER3_STATE) VAR preferred : {master1, master2, master3, default}; ASSIGN init (preferred) := default; next (preferred) := case -- Master starts the transmission !HGRANT1 & !HGRANT2 & !HGRANT3 & BUSREQ1 & BUSREQ2 & BUSREQ3 : {master1, master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & BUSREQ1 & BUSREQ2 : {master1, master2}; !HGRANT1 & !HGRANT2 & !HGRANT3 & BUSREQ2 & BUSREQ3 : {master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & BUSREQ1 & BUSREQ3 : {master1, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & BUSREQ1 & !BUSREQ2 & !BUSREQ3 : master1; !HGRANT1 & !HGRANT2 & !HGRANT3 & !BUSREQ1 & BUSREQ2 & !BUSREQ3 : master2; !HGRANT1 & !HGRANT2 & !HGRANT3 & !BUSREQ1 & !BUSREQ2 & BUSREQ3 : master3; -- Master finishes the transaction - round-robin HGRANT1 & MASTER1_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & MASTER2_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & MASTER3_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT1 & MASTER1_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ2 : master2; HGRANT1 & MASTER1_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = write & (HTRANS = IDLE | HTRANS = BUSY) & BUSREQ2 : master2; -- Master gives up its BUSREQ HGRANT1 & MASTER1_STATE = idle & HTRANS = IDLE & !BUSREQ1 & BUSREQ2 : master2; HGRANT1 & MASTER1_STATE = idle & HTRANS = IDLE & !BUSREQ1 & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = idle & HTRANS = IDLE & !BUSREQ2 & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = idle & HTRANS = IDLE & !BUSREQ2 & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = idle & HTRANS = IDLE & !BUSREQ3 & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = idle & HTRANS = IDLE & !BUSREQ3 & BUSREQ2 : master2; HGRANT1 & HTRANS = IDLE & HTRANS = IDLE & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & HTRANS = IDLE & HTRANS = IDLE & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & HTRANS = IDLE & HTRANS = IDLE & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; 1 : preferred; esac; HMASTER := case preferred = master1 : master1; preferred = master2 : master2; preferred = master3 : master3; preferred = default : default; esac; HGRANT1 := case preferred = master1 : 1; 1 : 0; esac; HGRANT2 := case preferred = master2 : 1; 1 : 0; esac; HGRANT3 := case preferred = master3 : 1; 1 : 0; esac;