package Communication.FDDI.Binary; module timer(event ?reset, bool c0, c1, c2, c3, c4, c5, c6, c7) { bool s7, s6, s5, s4, s3, s2, s1, s0, cry8; loop { next(c7) = false; next(c6) = false; next(c5) = false; next(c4) = false; next(c3) = false; next(c2) = false; next(c1) = false; next(c0) = false; w1: pause; abort { loop { Add: Adder8(c7,c6,c5,c4,c3,c2,c1,c0, false,false,false,false,false,false,false,false, true, cry8,s7,s6,s5,s4,s3,s2,s1,s0); next(c7) = s7; next(c6) = s6; next(c5) = s5; next(c4) = s4; next(c3) = s3; next(c2) = s2; next(c1) = s1; next(c0) = s0; consume_time: pause; } }when(reset); } }satisfies { cf1 : assert A X w1; cf2 : assert A G (w1 -> A X consume_time); cf3 : assert A G (consume_time & !reset -> A X consume_time); cf4 : assert A G (consume_time & reset -> A X w1); df1 : assert !(c7 | c6 | c5 | c4 | c3 | c2 | c1 | c0); df20 : assert A X !(c7 | c6 | c5 | c4 | c3 | c2 | c1 | c0); df21 : assert A X A X (!(c7 | c6 | c5 | c4 | c3 | c2 | c1 ) & c0); reset0 : assert A G (c0 -> A X !c0); reset1 : assert A X A G (reset -> A X (!c7 & !c6 & !c5 & !c4 & !c3 & !c2 & !c1)); }