-- 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 HADDR : boolean; HTRANS : {IDLE, NONSEQ, SEQ, BUSY}; HWDATA : boolean; HRDATA : boolean; HREADY : boolean; HRESP : {OK, ERROR, RETRY, SPLIT}; BUSREQ1 : boolean; BUSREQ2 : boolean; BUSREQ3 : boolean; HGRANT1 : boolean; HGRANT2 : boolean; HGRANT3 : boolean; HMASTER : {master1, master2, master3, default}; HSPLIT : {0, master1, master2, master3}; -- HW components connected to the bus master1 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ1, HGRANT1); master2 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ2, HGRANT2); master3 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ3, HGRANT3); slave : slave (HADDR, HTRANS, HWDATA, HRDATA, HREADY, HRESP, HMASTER, HSPLIT); arbiter : arbiter_round_robin (HTRANS, HREADY, HRESP, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, HSPLIT); ASSIGN init (HRESP) := OK; HADDR := case HMASTER = master1 : master1.HADDR; HMASTER = master2 : master2.HADDR; HMASTER = master3 : master3.HADDR; HMASTER = default : 0; esac; HTRANS := case HMASTER = master1 : master1.HTRANS; HMASTER = master2 : master2.HTRANS; HMASTER = master3 : master3.HTRANS; HMASTER = default : IDLE; esac; HWDATA := case HMASTER = master1 : master1.HWDATA; HMASTER = master2 : master2.HWDATA; HMASTER = master3 : master3.HWDATA; HMASTER = default : 0; esac; JUSTICE HREADY JUSTICE HRESP = OK JUSTICE HSPLIT = master1 JUSTICE HSPLIT = master2 JUSTICE HSPLIT = master3 SPEC AG (master1.state != error) -- true SPEC AG (master2.state != error) -- true SPEC AG (master3.state != error) -- true SPEC AG (slave.state != error) -- true SPEC EF (arbiter.master1_state = mask & arbiter.master2_state = mask) -- true SPEC AG ((arbiter.master1_state = mask & arbiter.master2_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask)) -- true SPEC EF (arbiter.master1_state = mask & arbiter.master3_state = mask) -- true SPEC AG ((arbiter.master1_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master3_state != mask)) -- true SPEC EF (arbiter.master2_state = mask & arbiter.master3_state = mask) -- true SPEC AG ((arbiter.master2_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master2_state != mask | arbiter.master3_state != mask)) -- true SPEC EF (arbiter.master1_state = mask & arbiter.master2_state = mask & arbiter.master3_state = mask) -- true SPEC AG ((arbiter.master1_state = mask & arbiter.master2_state = mask & arbiter.master3_state = mask) -> AF (arbiter.master1_state != mask | arbiter.master2_state != mask | arbiter.master3_state != mask)) -- true SPEC AG (master1.state = busreq -> AF HGRANT1) -- true SPEC AG (master2.state = busreq -> AF HGRANT2) -- true SPEC AG (master3.state = busreq -> AF HGRANT3) -- true SPEC AG (master1.state = busreq -> AF master1.state = write) -- true SPEC AG (master2.state = busreq -> AF master2.state = write) -- true SPEC AG (master3.state = busreq -> AF master3.state = write) -- true MODULE master_read_write (HRDATA, HREADY, HRESP, BUSREQ, HGRANT) VAR state : {idle, busreq, haddr, read, write, error}; prev_state : {idle, busreq, haddr, read, write, error}; HADDR: boolean; HTRANS : {IDLE, NONSEQ, SEQ, BUSY}; HWDATA : boolean; ASSIGN init (state) := idle; init (prev_state) := state; next (prev_state) := state; next (state) := case HRESP = ERROR : error; HRESP = SPLIT & HGRANT : idle; !HREADY : state; HRESP = RETRY & HGRANT : prev_state; state = idle : {idle, busreq}; state = busreq & HGRANT & HRESP = OK : haddr; state = busreq & !HGRANT : state; state = haddr & HGRANT & HRESP = OK : read; state = read & HGRANT & HRDATA & HRESP = OK : write; state = write & HGRANT & HRESP = OK : idle; 1: error; esac; -- Set bus signals according to state HADDR := case state = haddr : 1; 1 : 0; esac; HTRANS := case state = haddr : NONSEQ; state = read : SEQ; state = write : SEQ; 1 : IDLE; esac; HWDATA := case state = write : 1; 1 : 0; esac; -- HRDATA written by slave -- HREADY written by slave -- HRESP written by slave BUSREQ := case state = busreq : 1; 1 : 0; esac; MODULE slave (HADDR, HTRANS, HWDATA, HRDATA, HREADY, HRESP, HMASTER, HSPLIT) VAR state : {idle, write, read, error}; prev_state : {idle, write, read, error}; MASK_MASTER1 : boolean; MASK_MASTER2 : boolean; MASK_MASTER3 : boolean; extended : boolean; ASSIGN init (state) := idle; init (MASK_MASTER1) := 0; init (MASK_MASTER2) := 0; init (MASK_MASTER3) := 0; init (prev_state) := state; init (extended) := 0; next (prev_state) := state; next (state) := case HRESP = SPLIT : idle; !HREADY : state; HRESP = RETRY : prev_state; state = idle & HTRANS = NONSEQ & HADDR : write; state = idle : state; state = write & HTRANS = SEQ : read; state = read & HTRANS = SEQ & HWDATA : idle; 1 : error; esac; HRDATA := case state = write : 1; 1 : 0; esac; HREADY := case HRESP = RETRY : 1; HRESP = SPLIT : 1; 1 : {1, 0}; esac; next (HRESP) := case HRESP = SPLIT & !extended : SPLIT; HRESP = RETRY & !extended : RETRY; HRESP = SPLIT & extended : OK; HRESP = RETRY & extended : OK; state = write & HREADY & HSPLIT = 0 : {OK, RETRY, SPLIT}; state = read & HREADY & HSPLIT = 0 : {OK, RETRY, SPLIT}; state = write & HREADY : {OK, SPLIT}; state = read & HREADY : {OK, SPLIT}; 1 : OK; esac; next (extended) := case HRESP = SPLIT & !extended : 1; HRESP = RETRY & !extended : 1; 1 : 0; esac; next (MASK_MASTER1) := case HMASTER = master1 & HRESP = SPLIT & !extended : 1; HSPLIT = master1 : 0; 1 : MASK_MASTER1; esac; next (MASK_MASTER2) := case HMASTER = master2 & HRESP = SPLIT & !extended : 1; HSPLIT = master2 : 0; 1 : MASK_MASTER2; esac; next (MASK_MASTER3) := case HMASTER = master3 & HRESP = SPLIT & !extended : 1; HSPLIT = master3 : 0; 1 : MASK_MASTER3; esac; HSPLIT := case MASK_MASTER1 & MASK_MASTER2 & MASK_MASTER3 : {master1, master2, master3}; MASK_MASTER2 & MASK_MASTER3 & HMASTER = master1 & HRESP != RETRY : {0, master2, master3}; MASK_MASTER1 & MASK_MASTER3 & HMASTER = master2 & HRESP != RETRY : {0, master1, master3}; MASK_MASTER1 & MASK_MASTER2 & HMASTER = master3 & HRESP != RETRY : {0, master1, master2}; MASK_MASTER1 & HMASTER = master2 & HRESP != RETRY : {0, master1}; MASK_MASTER1 & HMASTER = master3 & HRESP != RETRY : {0, master1}; MASK_MASTER2 & HMASTER = master3 & HRESP != RETRY : {0, master2}; MASK_MASTER2 & HMASTER = master1 & HRESP != RETRY : {0, master2}; MASK_MASTER3 & HMASTER = master1 & HRESP != RETRY : {0, master3}; MASK_MASTER3 & HMASTER = master2 & HRESP != RETRY : {0, master3}; 1 : 0; esac; MODULE arbiter_round_robin (HTRANS, HREADY, HRESP, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, HSPLIT) VAR master1_state : {idle, mask, grant, transmit}; master2_state : {idle, mask, grant, transmit}; master3_state : {idle, mask, grant, transmit}; master1_prev_state : {idle, mask, grant, transmit}; master2_prev_state : {idle, mask, grant, transmit}; master3_prev_state : {idle, mask, grant, transmit}; lasterror : boolean; preferred : {master1, master2, master3, default}; ASSIGN init (master1_state) := idle; init (master1_prev_state) := master1_state; init (master2_state) := idle; init (master2_prev_state) := master2_state; init (master3_state) := idle; init (master3_prev_state) := master2_state; init (lasterror) := 0; init (preferred) := default; next (master1_prev_state) := master1_state; next (master2_prev_state) := master2_state; next (master3_prev_state) := master3_state; next (preferred) := case -- Master starts the transmission !HGRANT1 & !HGRANT2 & !HGRANT3 & master1_state != mask & master2_state != mask & master3_state != mask & HREADY & HRESP = OK & BUSREQ1 & BUSREQ2 & BUSREQ3 : {master1, master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & master1_state != mask & master2_state != mask & HREADY & HRESP = OK & BUSREQ1 & BUSREQ2 : {master1, master2}; !HGRANT1 & !HGRANT2 & !HGRANT3 & master2_state != mask & master3_state != mask & HREADY & HRESP = OK & BUSREQ2 & BUSREQ3 : {master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & master1_state != mask & master3_state != mask & HREADY & HRESP = OK & BUSREQ1 & BUSREQ3 : {master1, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & master1_state != mask & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ2 & !BUSREQ3 : master1; !HGRANT1 & !HGRANT2 & !HGRANT3 & master2_state != mask & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ2 & !BUSREQ3 : master2; !HGRANT1 & !HGRANT2 & !HGRANT3 & master3_state != mask & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & BUSREQ3 : master3; -- Cross-splitting HGRANT1 & master1_state = transmit & master2_state = mask & HRESP = SPLIT & !BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : default; HGRANT1 & master1_state = transmit & master3_state = mask & HRESP = SPLIT & !BUSREQ2 & !BUSREQ3 & HSPLIT = master3 : default; HGRANT2 & master2_state = transmit & master3_state = mask & HRESP = SPLIT & !BUSREQ1 & !BUSREQ3 & HSPLIT = master3 : default; HGRANT2 & master2_state = transmit & master1_state = mask & HRESP = SPLIT & !BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : default; HGRANT3 & master3_state = transmit & master1_state = mask & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : default; HGRANT3 & master3_state = transmit & master2_state = mask & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & HSPLIT = master2 : default; HGRANT1 & master1_state = transmit & master2_state = mask & HRESP = SPLIT & BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : master2; HGRANT1 & master1_state = transmit & master3_state = mask & HRESP = SPLIT & !BUSREQ2 & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master2_state = transmit & master3_state = mask & HRESP = SPLIT & !BUSREQ1 & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master2_state = transmit & master1_state = mask & HRESP = SPLIT & BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : master1; HGRANT3 & master3_state = transmit & master1_state = mask & HRESP = SPLIT & BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : master1; HGRANT3 & master3_state = transmit & master2_state = mask & HRESP = SPLIT & !BUSREQ1 & BUSREQ2 & HSPLIT = master2 : master2; -- Split masters HGRANT1 & master2_state = mask & master3_state = mask & HRESP = SPLIT : default; HGRANT2 & master1_state = mask & master3_state = mask & HRESP = SPLIT : default; HGRANT3 & master1_state = mask & master2_state = mask & HRESP = SPLIT : default; HGRANT1 & master2_state != mask & HRESP = SPLIT & BUSREQ2 : master2; HGRANT1 & master3_state != mask & HRESP = SPLIT & BUSREQ3 : master3; HGRANT2 & master3_state != mask & HRESP = SPLIT & BUSREQ3 : master3; HGRANT2 & master1_state != mask & HRESP = SPLIT & BUSREQ1 : master1; HGRANT3 & master1_state != mask & HRESP = SPLIT & BUSREQ1 : master1; HGRANT3 & master2_state != mask & HRESP = SPLIT & BUSREQ2 : master2; HGRANT1 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; -- Master finishes the transaction - round-robin HGRANT1 & master1_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & master2_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & master3_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT1 & master1_state = transmit & master2_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 : master2; HGRANT1 & master1_state = transmit & master3_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 : master3; HGRANT2 & master2_state = transmit & master3_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 : master3; HGRANT2 & master2_state = transmit & master1_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 : master1; HGRANT3 & master3_state = transmit & master1_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 : master1; HGRANT3 & master3_state = transmit & master2_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 : master2; -- Master gives up its BUSREQ HGRANT1 & master1_state = idle & master2_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ2 : master2; HGRANT1 & master1_state = idle & master3_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ3 : master3; HGRANT2 & master2_state = idle & master3_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ2 & BUSREQ3 : master3; HGRANT2 & master2_state = idle & master1_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ2 & BUSREQ1 : master1; HGRANT3 & master3_state = idle & master1_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ3 & BUSREQ1 : master1; HGRANT3 & master3_state = idle & master2_state != mask & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ3 & BUSREQ2 : master2; HGRANT1 & master1_state = idle & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & master2_state = idle & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & master3_state = idle & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; -- Unmasking masters !HGRANT1 & !HGRANT2 & !HGRANT3 & master1_state = mask & HSPLIT = master1 : master1; !HGRANT1 & !HGRANT2 & !HGRANT3 & master2_state = mask & HSPLIT = master2 : master2; !HGRANT1 & !HGRANT2 & !HGRANT3 & master3_state = mask & HSPLIT = master3 : master3; HGRANT1 & master2_state = mask & HRESP = SPLIT & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & master3_state = mask & HRESP = SPLIT & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master3_state = mask & HRESP = SPLIT & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master1_state = mask & HRESP = SPLIT & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & master1_state = mask & HRESP = SPLIT & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & master2_state = mask & HRESP = SPLIT & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & master1_state = transmit & master2_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & master1_state = transmit & master3_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master2_state = transmit & master3_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & master2_state = transmit & master1_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & master3_state = transmit & master1_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & master3_state = transmit & master2_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & master1_state = idle & master2_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & !BUSREQ1 & HSPLIT = master2 : master2; HGRANT1 & master1_state = idle & master3_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & !BUSREQ1 & HSPLIT = master3 : master3; HGRANT2 & master2_state = idle & master3_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & !BUSREQ2 & HSPLIT = master3 : master3; HGRANT2 & master2_state = idle & master1_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : master1; HGRANT3 & master3_state = idle & master1_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : master1; HGRANT3 & master3_state = idle & master2_state = mask & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : master2; 1 : preferred; esac; next (master1_state) := case -- Roll back for retrys HRESP = RETRY & !lasterror : master1_prev_state; master1_state = idle & HREADY & HRESP = OK & HGRANT1 : grant; master1_state = grant & HTRANS != IDLE & HREADY & HRESP = OK & HGRANT1 : transmit; master1_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & HGRANT1 : idle; HREADY & HRESP = SPLIT & HGRANT1 & !lasterror : mask; master1_state = mask & HSPLIT = master1 : idle; lasterror : master1_state; !HREADY : master1_state; 1 : master1_state; esac; next (master2_state) := case -- Roll back for retrys HRESP = RETRY & !lasterror : master2_prev_state; master2_state = idle & HREADY & HRESP = OK & HGRANT2 : grant; master2_state = grant & HTRANS != IDLE & HREADY & HRESP = OK & HGRANT2 : transmit; master2_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & HGRANT2 : idle; HREADY & HRESP = SPLIT & HGRANT2 & !lasterror : mask; master2_state = mask & HSPLIT = master2 : idle; lasterror : master2_state; !HREADY : master2_state; 1 : master2_state; esac; next (master3_state) := case -- Roll back for retrys HRESP = RETRY & !lasterror : master3_prev_state; master3_state = idle & HREADY & HRESP = OK & HGRANT3 : grant; master3_state = grant & HTRANS != IDLE & HREADY & HRESP = OK & HGRANT3 : transmit; master3_state = transmit & HTRANS = IDLE & HREADY & HRESP = OK & HGRANT3 : idle; HREADY & HRESP = SPLIT & HGRANT3 & !lasterror : mask; master3_state = mask & HSPLIT = master3 : idle; lasterror : master3_state; !HREADY : master3_state; 1 : master3_state; esac; next (lasterror) := case HRESP = RETRY : 1; HRESP = SPLIT : 1; 1 : 0; 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;