Studies/Formal Verification
MSI protocol - NuSMV 구현
쿠뱃봉
2023. 3. 10. 14:12
1. 관련 노트
2. 관련 코드
MODULE main
VAR
-- cpu_op1234: {rd1, wr1, rd2, wr2, none};
cpu_op1234: {rd1, wr1, rd2, wr2, rd3, wr3, none};
-- cpu_op1234: {rd1, wr1, rd2, wr2, rd3, wr3, rd4, wr4};
cache1 : {state_M, state_S, state_I, tr_S2M, tr_I2M, tr_I2S};
cache2 : {state_M, state_S, state_I, tr_S2M, tr_I2M, tr_I2S};
cache3 : {state_M, state_S, state_I, tr_S2M, tr_I2M, tr_I2S};
bus: {rd, rdx, upgrade, flush, none};
done1: boolean;
done2: boolean;
done3: boolean;
ASSIGN
init(cpu_op1234) := none;
next(cpu_op1234) := case
!(cpu_op1234 = none) : none;
done1 & done2 & done3 & (cpu_op1234 = none): {rd1, wr1, rd2, wr2, rd3, wr3};
TRUE: cpu_op1234;
esac;
init(cache1) := state_I;
-- init(cache1) := state_M; --/ cpu_wr 요청 작성 전까지 임의로 state_M으로 바꾸어 놓음
next(cache1) := case
--/ cpu rd 요청
cpu_op1234 = rd1 & cache1 = state_I : tr_I2S ;
cache1 = tr_I2S & bus = none : state_S ;
cache1 = tr_I2S & bus = flush : state_S ;
--/rd 요청에 따른 bus 받았을 때
cache1 = state_I & bus = rd : state_I ; --/ I에서 bus_rd를 받았을 때 I로 유지
cache1 = state_S & bus = rd : state_S ; --/ S에서 bus_rd를 받았을 때 S로 유지
cache1 = state_M & bus = flush & (cache2 = tr_I2S | cache3 = tr_I2S) : state_S ; --/ M이고 bus=flush 이면 S로 변화
--/cpu wr 요청
cpu_op1234 = wr1 & cache1 = state_I : tr_I2M ;
cache1 = tr_I2M & bus = none : state_M ;
cpu_op1234 = wr1 & cache1 = state_S : tr_S2M ;
cache1 = tr_S2M & bus = none : state_M ;--/
cpu_op1234 = wr1 & cache1 = state_M : state_M ;
--/wr 요청에 따른 bus 받았을 때
cache1 = state_I & bus = rdx & (done2 = FALSE | done3 = FALSE): state_I ;
cache1 = state_S & bus = rdx & (done2 = FALSE | done3 = FALSE): state_I ;
cache1 = state_M & bus = flush & (cache2 = tr_I2M | cache3 = tr_I2M) : state_I ;
TRUE : cache1 ;
esac;
init(cache2) := state_I;
-- init(cache2) := state_M; --/ cpu_wr 요청 작성 전까지 임의로 state_M으로 바꾸어 놓음
next(cache2) := case
--/ cpu rd 요청
cpu_op1234 = rd2 & cache2 = state_I : tr_I2S ;
cache2 = tr_I2S & bus = none : state_S ;
cache2 = tr_I2S & bus = flush : state_S ;--/
--/rd 요청에 따른 bus 받았을 때
cache2 = state_I & bus = rd : state_I ; --/ I에서 bus_rd를 받았을 때 I로 유지
cache2 = state_S & bus = rd : state_S ; --/ S에서 bus_rd를 받았을 때 S로 유지
cache2 = state_M & bus = flush & (cache1 = tr_I2S | cache3 = tr_I2S) : state_S ; --/ M이고 bus=flush 이면 S로 변화
--/cpu wr 요청
cpu_op1234 = wr2 & cache2 = state_I : tr_I2M ;
cache2 = tr_I2M & bus = none : state_M ;--/
cpu_op1234 = wr2 & cache2 = state_S : tr_S2M ;
cache2 = tr_S2M & bus = none : state_M ;--/
cpu_op1234 = wr2 & cache2 = state_M : state_M ;
--/wr 요청에 따른 bus 받았을 때
cache2 = state_I & bus = rdx & (done1 = FALSE| done3 = FALSE) : state_I ;
cache2 = state_S & bus = rdx & (done1 = FALSE| done3 = FALSE) : state_I ;
cache2 = state_M & bus = flush & (cache1 = tr_I2M | cache3 = tr_I2M): state_I ;
TRUE : cache2 ;
esac;
init(cache3) := state_I;
-- init(cache3) := state_M; --/임의로 설정
next(cache3) := case
--/ cpu rd 요청
cpu_op1234 = rd3 & cache3 = state_I : tr_I2S ;
cache3 = tr_I2S & bus = none : state_S ;
cache3 = tr_I2S & bus = flush : state_S ;
--/rd 요청에 따른 bus 받았을 때
cache3 = state_I & bus = rd : state_I ; --/ I에서 bus_rd를 받았을 때 I로 유지
cache3 = state_S & bus = rd : state_S ; --/ S에서 bus_rd를 받았을 때 S로 유지
cache3 = state_M & bus = flush & (cache1 = tr_I2S | cache2 = tr_I2S): state_S ; --/ M이고 bus=flush 이면 S로 변화
--/cpu wr 요청
cpu_op1234 = wr3 & cache3 = state_I : tr_I2M ;
cache3 = tr_I2M & bus = none : state_M ;--/
cpu_op1234 = wr3 & cache3 = state_S : tr_S2M ;
cache3 = tr_S2M & bus = none : state_M ;--/
cpu_op1234 = wr3 & cache3 = state_M : state_M ;
--/wr 요청에 따른 bus 받았을 때
cache3 = state_I & bus = rdx & (done1 = FALSE | done2 = FALSE): state_I ;
cache3 = state_S & bus = rdx & (done1 = FALSE | done2 = FALSE) : state_I ;
cache3 = state_M & bus = flush & (cache1 = tr_I2M | cache2 = tr_I2M): state_I ;
TRUE : cache3 ;
esac;
init(bus) := none;
next(bus) := case
--/rd
cpu_op1234 = rd1 & cache1 = state_I : rd ;
cpu_op1234 = rd2 & cache2 = state_I : rd ;
cpu_op1234 = rd3 & cache2 = state_I : rd ;
(cache1 = state_M | cache2 = state_M | cache3 = state_M) & bus = rd : flush ;
bus = flush : none ;
bus = rd : none ; --/ 두 줄 묶어서 bus != none : flush ; 로 처리해도 될 것 같기도?
--/wr
cpu_op1234 = wr1 & (cache1 = state_I | cache1 = state_S): rdx ;
cpu_op1234 = wr2 & (cache2 = state_I | cache2 = state_S): rdx ;
cpu_op1234 = wr3 & (cache3 = state_I | cache3 = state_S): rdx ;
cpu_op1234 = wr1 & cache1 = state_M : upgrade ;
cpu_op1234 = wr2 & cache2 = state_M : upgrade ;
(cache1 = state_M | cache2 = state_M) & bus= rdx : flush;
(cache1 = state_M | cache2 = state_M) & bus= flush : none;
bus = rdx : none ;
bus = upgrade : none ;
-- cache1 = state_I & bus = upgrade : none ; --/state_invalidate를 추가로 생성해줘야하지 않을까? state_I에서 bus_upgr를 받으면 state_invalidate로 변하는 용도
TRUE : bus ;
esac;
init(done1) := TRUE;
next(done1) := case
cpu_op1234 = rd1 : FALSE ;
done1 = FALSE & ((cache1 = state_I) | (cache1 = state_M) | (cache1 = state_S) ) & bus = none : TRUE;
cpu_op1234 = wr1 : FALSE ;
TRUE : done1 ;
esac;
init(done2) := TRUE;
next(done2) := case
cpu_op1234 = rd2 : FALSE ;
done2 = FALSE & ((cache2 = state_I) | (cache2 = state_M) | (cache2 = state_S) ) & bus = none : TRUE; --/transient 지나서 state 바뀌고 bus = none (bus처리완료) 일때 true
cpu_op1234 = wr2 : FALSE ;
TRUE : done2 ;
esac;
init(done3) := TRUE;
next(done3) := case
cpu_op1234 = rd3 : FALSE ;
done3 = FALSE & ((cache3 = state_I) | (cache3 = state_M) | (cache3 = state_S) ) & bus = none : TRUE; --/transient 지나서 state 바뀌고 bus = none (bus처리완료) 일때 true
cpu_op1234 = wr3 : FALSE ;
TRUE : done3 ;
esac;
SPEC AG ! (cache1 = state_M & cache2 = state_M);
SPEC AG ! (cache1 = state_M & cache3 = state_M);
SPEC AG ! (cache2 = state_M & cache3 = state_M);
SPEC AG ! (cache1 = state_M & cache2 = state_S);
SPEC AG ! (cache1 = state_M & cache3 = state_S);
SPEC AG ! (cache2 = state_M & cache3 = state_S);
SPEC AG ! (cache1 = state_S & cache2 = state_M);
SPEC AG ! (cache1 = state_S & cache3 = state_M);
SPEC AG ! (cache2 = state_S & cache3 = state_M);
SPEC AG (((cache1 = state_I | cache1 = state_S ) & (cpu_op1234 = rd1))-> AF cache1 = state_S); --/ M I 일때 M에 rd 요청이 오면 M I 그대로 유지
SPEC AG (((cache2 = state_I | cache2 = state_S ) & (cpu_op1234 = rd2))-> AF cache2 = state_S); --/ M I 일때 M에 rd 요청이 오면 M I 그대로 유지
SPEC AG (((cache3 = state_I | cache3 = state_S ) & (cpu_op1234 = rd3))-> AF cache3 = state_S); --/ M I 일때 M에 rd 요청이 오면 M I 그대로 유지
SPEC AG (((cache1 = state_I | cache1 = state_S |cache1 =state_M ) & (cpu_op1234 = wr1))-> AF cache1 = state_M);
SPEC AG (((cache2 = state_I | cache2 = state_S |cache2 =state_M ) & (cpu_op1234 = wr2))-> AF cache2 = state_M);
SPEC AG (((cache3 = state_I | cache3 = state_S |cache3 =state_M ) & (cpu_op1234 = wr3))-> AF cache3 = state_M);