-- 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; MASK_MASTER1 : boolean; MASK_MASTER2 : boolean; MASK_MASTER3 : boolean; HMASTER : {master1, master2, master3, default}; HSPLIT : {0, master1, master2, master3}; MASTER1_STATE : {idle, haddr, read, write}; MASTER2_STATE : {idle, haddr, read, write}; MASTER3_STATE : {idle, haddr, read, write}; SLAVE_STATE : {x, idle, write, read}; -- HW components connected to the bus master1 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ1, HGRANT1, MASK_MASTER1, MASTER1_STATE); master2 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ2, HGRANT2, MASK_MASTER2, MASTER2_STATE); master3 : master_read_write (HRDATA, HREADY, HRESP, BUSREQ3, HGRANT3, MASK_MASTER3, MASTER3_STATE); slave : slave (HADDR, HTRANS, HWDATA, HRDATA, HREADY, HRESP, HMASTER, HSPLIT, MASK_MASTER1, MASK_MASTER2, MASK_MASTER3, SLAVE_STATE); arbiter : arbiter_round_robin (HTRANS, HREADY, HRESP, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, HSPLIT, MASK_MASTER1, MASK_MASTER2, MASK_MASTER3, MASTER1_STATE, MASTER2_STATE, MASTER3_STATE, SLAVE_STATE); ASSIGN init (HRESP) := OK; init (MASK_MASTER1) := 0; init (MASK_MASTER2) := 0; init (MASK_MASTER3) := 0; 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 (MASK_MASTER1 & MASK_MASTER2) -- true SPEC AG ((MASK_MASTER1 & MASK_MASTER2) -> AF (!MASK_MASTER1 | !MASK_MASTER2)) -- true SPEC EF (MASK_MASTER1 & MASK_MASTER3) -- true SPEC AG ((MASK_MASTER1 & MASK_MASTER3) -> AF (!MASK_MASTER1 | !MASK_MASTER3)) -- true SPEC EF (MASK_MASTER2 & MASK_MASTER3) -- true SPEC AG ((MASK_MASTER2 & MASK_MASTER3) -> AF (!MASK_MASTER2 | !MASK_MASTER3)) -- true SPEC EF (MASK_MASTER1 & MASK_MASTER2 & MASK_MASTER3) -- true SPEC AG ((MASK_MASTER1 & MASK_MASTER2 & MASK_MASTER3) -> AF (!MASK_MASTER1 | !MASK_MASTER2 | !MASK_MASTER3)) -- 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, MASK_MASTER, MASTER_STATE) 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; MASK_MASTER & HGRANT : error; HRESP = SPLIT & HGRANT : state; !HREADY : state; MASK_MASTER : 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; MASTER_STATE := case state = idle : idle; state = busreq : idle; state = haddr : haddr; state = read : read; state = write : write; state = error : idle; esac; HADDR := case state = haddr : 1; 1 : 0; esac; HTRANS := case state = haddr : NONSEQ; state = read : NONSEQ; state = write : NONSEQ; 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, MASK_MASTER1, MASK_MASTER2, MASK_MASTER3, SLAVE_STATE) VAR state : {idle, write, read, error}; prev_state : {idle, write, read, error}; extended : boolean; ASSIGN init (state) := idle; init (prev_state) := state; init (extended) := 0; next (prev_state) := state; next (state) := case SLAVE_STATE != x : SLAVE_STATE; HRESP = SPLIT : idle; !HREADY : state; HTRANS = BUSY : state; HRESP = RETRY : prev_state; state = idle & HTRANS = NONSEQ & HADDR : write; state = idle : state; state = write & HTRANS = NONSEQ : read; state = read & HTRANS = NONSEQ & 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 : {OK, RETRY, SPLIT}; state = read & HREADY : {OK, RETRY, SPLIT}; 1 : OK; esac; next (extended) := case HRESP = SPLIT & !extended : 1; HRESP = RETRY & !extended : 1; 1 : 0; esac; HSPLIT := case MASK_MASTER1 & MASK_MASTER2 & MASK_MASTER3 : {master1, master2, master3}; MASK_MASTER2 & MASK_MASTER3 & HMASTER = master1 : {0, master2, master3}; MASK_MASTER1 & MASK_MASTER3 & HMASTER = master2 : {0, master1, master3}; MASK_MASTER1 & MASK_MASTER2 & HMASTER = master3 : {0, master1, master2}; MASK_MASTER1 & HMASTER = master2 : {0, master1}; MASK_MASTER1 & HMASTER = master3 : {0, master1}; MASK_MASTER2 & HMASTER = master3 : {0, master2}; MASK_MASTER2 & HMASTER = master1 : {0, master2}; MASK_MASTER3 & HMASTER = master1 : {0, master3}; MASK_MASTER3 & HMASTER = master2 : {0, master3}; 1 : 0; esac; MODULE arbiter_round_robin (HTRANS, HREADY, HRESP, BUSREQ1, BUSREQ2, BUSREQ3, HGRANT1, HGRANT2, HGRANT3, HMASTER, HSPLIT, MASK_MASTER1, MASK_MASTER2, MASK_MASTER3, MASTER1_STATE, MASTER2_STATE, MASTER3_STATE, SLAVE_STATE) VAR lasterror : boolean; preferred : {master1, master2, master3, default}; ASSIGN init (lasterror) := 0; init (preferred) := default; next (preferred) := case -- Master starts the transmission !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER1 & !MASK_MASTER2 & !MASK_MASTER3 & HREADY & HRESP = OK & BUSREQ1 & BUSREQ2 & BUSREQ3 : {master1, master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER1 & !MASK_MASTER2 & HREADY & HRESP = OK & BUSREQ1 & BUSREQ2 : {master1, master2}; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER2 & !MASK_MASTER3 & HREADY & HRESP = OK & BUSREQ2 & BUSREQ3 : {master2, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER1 & !MASK_MASTER3 & HREADY & HRESP = OK & BUSREQ1 & BUSREQ3 : {master1, master3}; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER1 & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ2 & !BUSREQ3 : master1; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER2 & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ2 & !BUSREQ3 : master2; !HGRANT1 & !HGRANT2 & !HGRANT3 & !MASK_MASTER3 & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & BUSREQ3 : master3; -- Cross-splitting HGRANT1 & MASTER1_STATE = write & MASK_MASTER2 & HRESP = SPLIT & !BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : default; HGRANT1 & MASTER1_STATE = write & MASK_MASTER3 & HRESP = SPLIT & !BUSREQ2 & !BUSREQ3 & HSPLIT = master3 : default; HGRANT2 & MASTER2_STATE = write & MASK_MASTER3 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ3 & HSPLIT = master3 : default; HGRANT2 & MASTER2_STATE = write & MASK_MASTER1 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : default; HGRANT3 & MASTER3_STATE = write & MASK_MASTER1 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : default; HGRANT3 & MASTER3_STATE = write & MASK_MASTER2 & HRESP = SPLIT & !BUSREQ1 & !BUSREQ2 & HSPLIT = master2 : default; HGRANT1 & MASTER1_STATE = write & MASK_MASTER2 & HRESP = SPLIT & BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : master2; HGRANT1 & MASTER1_STATE = write & MASK_MASTER3 & HRESP = SPLIT & !BUSREQ2 & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = write & MASK_MASTER3 & HRESP = SPLIT & !BUSREQ1 & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = write & MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = write & MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = write & MASK_MASTER2 & HRESP = SPLIT & !BUSREQ1 & BUSREQ2 & HSPLIT = master2 : master2; -- Split masters HGRANT1 & MASK_MASTER2 & MASK_MASTER3 & HRESP = SPLIT : default; HGRANT2 & MASK_MASTER1 & MASK_MASTER3 & HRESP = SPLIT : default; HGRANT3 & MASK_MASTER1 & MASK_MASTER2 & HRESP = SPLIT : default; HGRANT1 & !MASK_MASTER2 & HRESP = SPLIT & BUSREQ2 : master2; HGRANT1 & !MASK_MASTER3 & HRESP = SPLIT & BUSREQ3 : master3; HGRANT2 & !MASK_MASTER3 & HRESP = SPLIT & BUSREQ3 : master3; HGRANT2 & !MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 : master1; HGRANT3 & !MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 : master1; HGRANT3 & !MASK_MASTER2 & 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 = write & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & MASTER2_STATE = write & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & MASTER3_STATE = write & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT1 & MASTER1_STATE = write & !MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 : master2; HGRANT1 & MASTER1_STATE = write & !MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = write & !MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = write & !MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = write & !MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = write & !MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 : master2; -- Master gives up its BUSREQ HGRANT1 & MASTER1_STATE = idle & !MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ2 : master2; HGRANT1 & MASTER1_STATE = idle & !MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = idle & !MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ2 & BUSREQ3 : master3; HGRANT2 & MASTER2_STATE = idle & !MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ2 & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = idle & !MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ3 & BUSREQ1 : master1; HGRANT3 & MASTER3_STATE = idle & !MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ3 & BUSREQ2 : master2; HGRANT1 & HTRANS = IDLE & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT2 & HTRANS = IDLE & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; HGRANT3 & HTRANS = IDLE & HTRANS = IDLE & HREADY & HRESP = OK & !BUSREQ1 & !BUSREQ2 & !BUSREQ3 : default; -- Unmasking masters !HGRANT1 & !HGRANT2 & !HGRANT3 & MASK_MASTER1 & HSPLIT = master1 : master1; !HGRANT1 & !HGRANT2 & !HGRANT3 & MASK_MASTER2 & HSPLIT = master2 : master2; !HGRANT1 & !HGRANT2 & !HGRANT3 & MASK_MASTER3 & HSPLIT = master3 : master3; HGRANT1 & MASK_MASTER2 & HRESP = SPLIT & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & MASK_MASTER3 & HRESP = SPLIT & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASK_MASTER3 & HRESP = SPLIT & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & MASK_MASTER1 & HRESP = SPLIT & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & MASK_MASTER2 & HRESP = SPLIT & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & MASTER1_STATE = write & MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & MASTER1_STATE = write & MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = write & MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = write & MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = write & MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = write & MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & HSPLIT = master2 : master2; HGRANT1 & MASTER1_STATE = idle & MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & !BUSREQ1 & HSPLIT = master2 : master2; HGRANT1 & MASTER1_STATE = idle & MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & !BUSREQ1 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = idle & MASK_MASTER3 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ3 & !BUSREQ2 & HSPLIT = master3 : master3; HGRANT2 & MASTER2_STATE = idle & MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ2 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = idle & MASK_MASTER1 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ1 & !BUSREQ3 & HSPLIT = master1 : master1; HGRANT3 & MASTER3_STATE = idle & MASK_MASTER2 & HTRANS = IDLE & HREADY & HRESP = OK & BUSREQ2 & !BUSREQ3 & HSPLIT = master2 : master2; 1 : preferred; 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; next (MASK_MASTER1) := case HMASTER = master1 & HRESP = SPLIT & !lasterror : 1; HSPLIT = master1 : 0; 1 : MASK_MASTER1; esac; next (MASK_MASTER2) := case HMASTER = master2 & HRESP = SPLIT & !lasterror : 1; HSPLIT = master2 : 0; 1 : MASK_MASTER2; esac; next (MASK_MASTER3) := case HMASTER = master3 & HRESP = SPLIT & !lasterror : 1; HSPLIT = master3 : 0; 1 : MASK_MASTER3; esac; SLAVE_STATE := case HSPLIT = master1 & MASTER1_STATE = idle : idle; HSPLIT = master1 & MASTER1_STATE = haddr : idle; HSPLIT = master1 & MASTER1_STATE = read : write; HSPLIT = master1 & MASTER1_STATE = write : read; HSPLIT = master2 & MASTER2_STATE = idle : idle; HSPLIT = master2 & MASTER2_STATE = haddr : idle; HSPLIT = master2 & MASTER2_STATE = read : write; HSPLIT = master2 & MASTER2_STATE = write : read; HSPLIT = master3 & MASTER3_STATE = idle : idle; HSPLIT = master3 & MASTER3_STATE = haddr : idle; HSPLIT = master3 & MASTER3_STATE = read : write; HSPLIT = master3 & MASTER3_STATE = write : read; 1 : x; esac;