mesi_pro3.smv

-- Nusmv specification for MESI protocol with trasient state
-- Single cache line per processor with 1-bit data
-- Hyeonwoo 2/14/2023,2/22/2023
-- ******************************************************************
MODULE Cache(port_IO,bus_cmd,ack,done)
-- port_IO : 통로를 open,block 하는 param / bus_cmd: bus command snooping / ack 다른 cache state 확인 / 다른 cache 작업 확인 
VAR 
    state : {modified,exclusive, shared, invalid, -- 기존 state 
            modified_done,exclusive_done,shared_done,invalid_done, -- 완료된 것을 알려주는 state  
            i_pending,m_pending,s_pending}; -- transient state (pending state) 
    cpu_request : {cpu_wr,cpu_rd,none}; -- cpu가 -> cache로 보내는 요청
    task_status : {idle,rd_status,wr_status,wait,complete}; -- cpu 별 작업 상태 
    --/ idle 는 준비상태 , rd,wr,wait는 진행 상태 , complete는 state 가 변경되고 완료된 상태
    bus_req : {bus_rd,bus_rdx,invalidate,none}; -- task_status 가 wr_status 또는 rd_status 일때 버스로 보내지는 요청
DEFINE 
    -- CRAT := cpu_request = cpu_rd & ack = TRUE; CRAF := cpu_request = cpu_rd & ack = FALSE;
    -- CWAT := cpu_request = cpu_wr & ack = TRUE; CWAF := cpu_request = cpu_wr & ack = FALSE;
    -- STATE_DONE := state = modified_done | state = exclusive_done | state = shared_done | state = invalid_done;
    -- STATE_PENDING := state = i_pending | state = m_pending | state = s_pending;
ASSIGN
    -- 확인 
    init(task_status) := idle; -- 준비 상태 
    next(task_status) :=
    case
        state = modified_done | state = exclusive_done | state = shared_done | state = invalid_done : complete;
        task_status = complete : idle; --/ complete 다음은 항상 idle로 
        done = TRUE : complete;
        port_IO = TRUE : -- port 가 열렸을 때 
        case 
            task_status = idle : 
                case 
                    cpu_request = none : idle;
                    cpu_request = cpu_rd : rd_status;
                    cpu_request = cpu_wr : wr_status;
                esac;   
            state = i_pending | state = m_pending | state = s_pending : wait;
            TRUE : task_status; 
        esac; 
        port_IO = FALSE : -- bus 로 부터 받은 데이터 존재 
        case
            task_status = idle : 
                case 
                    bus_cmd = bus_rd : rd_status; 
                    bus_cmd = bus_rdx : wr_status;
                    TRUE : task_status;
                esac;
            TRUE: task_status;        
        esac;
        TRUE: task_status;
    esac;
    init(cpu_request) := none;    
    next(cpu_request):= 
        case 
            port_IO = TRUE : 
                case
                    cpu_request = none & task_status = idle : {cpu_wr,cpu_rd};
                    task_status = complete : none;
                    TRUE : cpu_request; -- (wr,rd,wait status)
                esac;
            port_IO = FALSE : none;  -- port_IO = FALSE 인 경우는 따로 
        esac;
    -- 확인 
    init(bus_req) := none;
    next(bus_req) :=
        case  
            port_IO = TRUE : -- open port 일때
                case
                    cpu_request = cpu_rd & task_status = wait : bus_rd;
                    cpu_request = cpu_wr & task_status = wait : bus_rdx;
                    state = modified & cpu_request = cpu_wr : bus_rdx;
                    state = shared & cpu_request = cpu_wr : bus_rdx;        
                    task_status = complete : none;
                    TRUE : bus_req;
                esac;
            port_IO = FALSE : 
                case
                    task_status = idle : bus_cmd;
                    task_status = complete : none;
                    TRUE : bus_req;
                esac;
            TRUE : bus_req;
        esac;
    init(state) := invalid;
    next(state) := 
    case
        state = exclusive_done : exclusive; state = modified_done : modified;
        state = shared_done : shared; state = invalid_done : invalid;
        port_IO = TRUE :-- cpu_로부터 
                case
                    -- 1.0 cpu_request = none 
                    cpu_request = none : state; 
                    -- 1.1 task_status = rd_status 일때 
                    task_status = rd_status:
                        case
                            state = invalid : i_pending;
                            state = shared : shared_done; -- 본인이 shared state 이면서 rd 권한 
                            state = exclusive : exclusive_done;
                            state = modified : modified_done;
                            TRUE : state;
                        esac;
                    -- 1.2 task_status = wr_status 일때 
                    task_status = wr_status:
                        case 
                            state = invalid : i_pending; 
                            state = shared : s_pending; -- pending 해서 다른 친구들 -> invalidate 하게 변경
                            state = exclusive : modified_done;
                            state = modified : m_pending;
                            TRUE : state;
                        esac;                    
                    -- 1.3 task_status = wait 일때 (다른 cache에서의 상황을 기다리는 중)
                    task_status = wait : --/ (state 가 pending 일때만 wait으로 넘어감)
                        case
                        -- 1.3.1 
                        state = i_pending & done = TRUE :
                            case
                                cpu_request = cpu_rd & ack = TRUE : shared_done; 
                                cpu_request = cpu_rd & ack = FALSE : exclusive_done; 
                                cpu_request = cpu_wr : modified_done;
                                -- cpu_request = cpu_wr & ack = TRUE : modified_done; 
                                -- cpu_request = cpu_wr & ack = FALSE : modified_done;
                            esac;
                        state = i_pending & done = FALSE : state;    
                        state = s_pending & done = TRUE :
                            case
                                cpu_request = cpu_rd & ack = TRUE : shared_done; 
                                cpu_request = cpu_rd & ack = FALSE : exclusive_done; 
                                cpu_request = cpu_wr & ack = TRUE : modified_done; 
                                cpu_request = cpu_wr & ack = FALSE : modified_done;
                            esac;
                        state = s_pending & done = FALSE : state; 
                        state = m_pending & done = TRUE :
                            case
                                cpu_request = cpu_rd & ack = TRUE : modified_done; 
                                cpu_request = cpu_rd & ack = FALSE : modified_done; 
                                cpu_request = cpu_wr & ack = TRUE : modified_done; 
                                cpu_request = cpu_wr & ack = FALSE : modified_done;
                            esac;
                        state = m_pending & done = FALSE : state; 
                        TRUE : state;
                        esac;
                    -- 1.5 i_pending state -> cpu_requset에 상관없이 그대로 유지
                    state = i_pending & ack = TRUE : shared_done;
                    state = i_pending & ack = FALSE : exclusive_done;
                    state = m_pending : 
                        case 
                            ack = TRUE : state;
                            ack = FALSE : modified_done;
                        esac;
                    state = s_pending:
                        case 
                            ack = TRUE : state;
                            ack = FALSE : shared_done;
                        esac;
                    TRUE : state;
                esac;
        port_IO = FALSE : 
                case
                    bus_cmd = invalidate : invalid_done;
                    task_status = idle :  state;
                    task_status = rd_status : 
                        case    
                            state = invalid : invalid_done;
                            -- state = modified : shared_done;
                            -- ack = TRUE : shared_done;
                            state = modified : shared_done;
                            state = exclusive : shared_done;
                            state = shared : shared_done;
                            TRUE : state;
                        esac;
                    task_status = wr_status | task_status = invalidate : invalid_done;
                    TRUE : state; 
                esac;
            TRUE : state;
        esac; 
-- END Cache
-- START main ******************************************************************
MODULE main
VAR
    BUS_CMD : {bus_rd,bus_rdx,invalidate,none};
    port_IO : array 0..3 of boolean; -- TRUE : open , FALSE : block
    ack : array 0..3 of boolean; -- 다른 cache의 상태(state) 를 확인하는 변수
    done : array 0..3 of boolean; -- 다른 cache에서 작업이 다 끝났는지를 확인하는 변수
    arbiter : {p0,p1,p2,p3,none,wait}; 
    c0 : Cache(port_IO[0],BUS_CMD,ack[0],done[0]);
    c1 : Cache(port_IO[1],BUS_CMD,ack[1],done[1]);
    c2 : Cache(port_IO[2],BUS_CMD,ack[2],done[2]);
    c3 : Cache(port_IO[3],BUS_CMD,ack[3],done[3]);  
DEFINE 
    ARBITER_ON := arbiter = p0 | arbiter = p1 | arbiter = p2 | arbiter = p3;
ASSIGN
    done[0] :=  case
            c1.task_status = complete & c2.task_status = complete & c3.task_status = complete : TRUE; TRUE : FALSE;
                esac;
    done[1] :=  case
            c0.task_status = complete & c2.task_status = complete & c3.task_status = complete : TRUE; TRUE : FALSE;
                esac;
    done[2] :=  case
            c1.task_status = complete & c0.task_status = complete & c3.task_status = complete : TRUE; TRUE : FALSE;
                esac;
    done[3] :=  case
            c1.task_status = complete & c2.task_status = complete & c0.task_status = complete : TRUE; TRUE : FALSE;
                esac;
    init(arbiter) := none;
    next(arbiter) := 
        case 
            arbiter = none : {p0,p1,p2,p3};
            ARBITER_ON : wait;
            -- arbiter = p0 | arbiter = p1 | arbiter = p2 | arbiter = p3 : wait;
            arbiter = wait :
                case
                    port_IO[0] = FALSE & port_IO[1] = FALSE & port_IO[2] = FALSE & port_IO[3] = FALSE : none;
                    TRUE : wait;
                esac;
        esac;    

    -- ///////// ack ////////// --
    -- ack 란 다른 cache 의 상태를 확인하는 변수 
    init(ack[0]) := FALSE;
    next(ack[0]) := case
                    c1.state = shared | c2.state = shared | c3.state = shared |
                    c1.state = shared_done | c2.state = shared_done | c3.state = shared_done : TRUE;
                    TRUE : FALSE;
                    -- c1.state = invalid | c2.state = invalid | c3.state = invalid 
                    -- | c1.state = invalid_done | c2.state = invalid_done | c3.state = invalid_done : FALSE;
                    -- TRUE : TRUE;
                esac;
    init(ack[1]):= FALSE;
    next(ack[1]):= case
                    c0.state = shared | c2.state = shared | c3.state = shared |
                    c0.state = shared_done | c2.state = shared_done | c3.state = shared_done : TRUE;
                    TRUE : FALSE;
                    -- c0.state = invalid | c2.state = invalid | c3.state = invalid 
                    -- | c0.state = invalid_done | c2.state = invalid_done | c3.state = invalid_done : FALSE;
                    -- TRUE : TRUE;
                esac;
    init(ack[2]) := FALSE;
    next(ack[2]) := case
                    c1.state = shared | c3.state = shared | c0.state = shared |
                    c1.state = shared_done | c3.state = shared_done | c0.state = shared_done : TRUE;
                    TRUE : FALSE;
                    -- c0.state = invalid | c1.state = invalid | c3.state = invalid 
                    -- | c0.state = invalid_done | c1.state = invalid_done | c3.state = invalid_done : FALSE;
                    -- TRUE : TRUE;
                esac;
    init(ack[3]):=FALSE;
    next(ack[3]):= case
                    c1.state = shared | c2.state = shared | c0.state = shared |
                    c1.state = shared_done | c2.state = shared_done | c0.state = shared_done : TRUE;
                    TRUE : FALSE; 
                    -- c0.state = invalid | c1.state = invalid | c2.state = invalid 
                    -- | c0.state = invalid_done | c1.state = invalid_done | c2.state = invalid_done : FALSE;
                    -- TRUE : TRUE;
                esac;
    -- ///////// port_IO ////////// --
    init(port_IO[0]) := FALSE;
    next(port_IO[0]) := 
            case
                c0.task_status = complete : FALSE; -- 종료 되었을 때  
                !(c0.task_status = complete) : 
                case
                    arbiter = none | arbiter = wait : port_IO[0]; 
                    arbiter = p0 : TRUE; TRUE : FALSE; 
                esac;
            esac;
    init(port_IO[1]) := FALSE;
    next(port_IO[1]) := 
            case
                c1.task_status = complete : FALSE;
                !(c1.task_status = complete):
                case
                    arbiter = none | arbiter = wait : port_IO[1]; 
                    arbiter = p1 : TRUE; TRUE : FALSE; 
                esac;
            esac;
    init(port_IO[2]) := FALSE;
    next(port_IO[2]) := 
            case 
                c2.task_status = complete : FALSE;
                !(c2.task_status = complete) : 
                case
                    arbiter = none | arbiter = wait : port_IO[2]; 
                    arbiter = p2 : TRUE; TRUE : FALSE; 
                esac;
            esac;
    init(port_IO[3]) := FALSE;
    next(port_IO[3]) := 
            case 
                c3.task_status = complete : FALSE;
                !(c3.task_status = complete) : 
                case
                    arbiter = none | arbiter = wait : port_IO[3]; 
                    arbiter = p3 : TRUE; TRUE : FALSE; 
                esac;
            esac;
    init(BUS_CMD) := none;
    next(BUS_CMD) := 
        case
            done[0] = TRUE | done[1] = TRUE | done[2] = TRUE | done[3] = TRUE : none;
            port_IO[0] = TRUE & c0.task_status = wait : c0.bus_req; 
            port_IO[1] = TRUE & c1.task_status = wait : c1.bus_req; 
            port_IO[2] = TRUE & c2.task_status = wait : c2.bus_req; 
            port_IO[3] = TRUE & c3.task_status = wait : c3.bus_req; 
            TRUE : none; 
        esac;
-- END main ******************************************************************

-- CTL CHECK SPEC
-- COMPELTE

-- 두개 비교 
-- 1. 
-- SPEC AG!(c0.state = modified & c1.state = modified) 
-- 2. 
-- SPEC AG!(c1.state = modified & c2.state = shared)
-- 3. 
-- SPEC AG!(c2.state = exclusive & c3.state = exclusive)
-- 4. 
-- SPEC AG!(c3.state = exclusive & c0.state = shared)

-- 세개 이상 비교 
-- 1
-- SPEC AG!(c0.state = modified & c1.state = modified & c2.state = modified)
-- SPEC AG!(c0.state = modified & c1.state = modified & c2.state = exclusive)
-- SPEC AG!(c0.state = modified & c1.state = modified & c2.state = shared)
-- SPEC AG!(c0.state = modified & c1.state = modified & c2.state = invalid) 

-- 2
-- SPEC AG!(c1.state = modified & c2.state = shared & c3.state = modified)
-- SPEC AG!(c1.state = modified & c2.state = shared & c3.state = exclusive)
-- SPEC AG!(c1.state = modified & c2.state = shared & c3.state = shared)
-- SPEC AG!(c1.state = modified & c2.state = shared & c3.state = invalid)

-- 3
-- SPEC AG!(c2.state = exclusive & c3.state = exclusive & c0.state = modified)
-- SPEC AG!(c2.state = exclusive & c3.state = exclusive & c0.state = exclusive)
-- SPEC AG!(c2.state = exclusive & c3.state = exclusive & c0.state = shared)
-- SPEC AG!(c2.state = exclusive & c3.state = exclusive & c0.state = invalid)

-- 4
-- SPEC AG!(c3.state = exclusive & c0.state = shared & c1.state = modified)
-- SPEC AG!(c3.state = exclusive & c0.state = shared & c1.state = exclusive)
-- SPEC AG!(c3.state = exclusive & c0.state = shared & c1.state = shared)
-- SPEC AG!(c3.state = exclusive & c0.state = shared & c1.state = invalid)

-- 4개 비교
-- 1.1 
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = modified & c3.state = modified)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = modified & c3.state = exclusive)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = modified & c3.state = shared)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = modified & c3.state = invalid)

-- 1.2 
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = exclusive & c3.state = modified)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = exclusive & c3.state = exclusive)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = exclusive & c3.state = shared)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = exclusive & c3.state = invalid)

-- 1.3
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = shared & c3.state = modified)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = shared & c3.state = exclusive)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = shared & c3.state = shared)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = shared & c3.state = invalid)

-- 1.4 
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = invalid & c3.state = modified)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = invalid & c3.state = exclusive)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = invalid & c3.state = shared)
SPEC AG!(c0.state = modified & c1.state = modified & c2.state = invalid & c3.state = invalid)

-- 기타 
-- SPEC AG!(c0.state = modified & c1.state = invalid & c2.state = exclusive & c3.state = shared) 
-- SPEC AG!(c0.state = shared & c1.state = invalid & c2.state = invalid)

-- port 관련 spec
-- SPEC AG!(c0.port_IO = TRUE & c1.port_IO = TRUE & c2.port_IO = TRUE &  c3.port_IO = TRUE)
-- SPEC AG!(c0.port_IO = TRUE & c2.port_IO = TRUE & c3.port_IO = TRUE)
-- SPEC AG!(c0.port_IO = TRUE & c2.port_IO = TRUE)

-- uncomplete