--****************************************************-- --****************************************************-- -- VALMEM Project -- -- Sample latch circuit by Remy (ST-Microelectronics) -- Times by Patricia Renault (LIP6) -- Modeling by Etienne ANDRE (LSV) -- -- Last modified : 23/04/2008 --****************************************************-- --****************************************************-- var s, ckClock, ckD, ckNot1, ckNot2, ckXor, ckAnd, ckLatch : clock; tNot1Down1, tNot2Up1, tXorUp1, tXorDown1, tAndUp1, tAndDown1, tLatchUp1 : discrete; dClockHigh, dClockLow, dSetup, dHold, dNot1Down_l, dNot1Down_u, dNot1Up_l, dNot1Up_u, dNot2Down_l, dNot2Down_u, dNot2Up_l, dNot2Up_u, dXorDown1Up_l, dXorDown1Up_u, dXorUp2Up_l, dXorUp2Up_u, dAndUp1_l, dAndUp1_u, dAndUp2_l, dAndUp2_u, dAndDown1_l, dAndDown1_u, dAndDown2_l, dAndDown2_u, dLatchUp_l, dLatchUp_u, q : parameter; --****************************************************-- --****************************************************-- -- AUTOMATA --****************************************************-- --****************************************************-- --****************************************************-- automaton clock1 --****************************************************-- synclabs: clockUp1; initially ClockLow1; loc ClockLow1: while ckClock <= dClockLow & ckClock >= 0 wait {} when ckClock >= dClockLow sync clockUp1 do {ckClock' = 0} goto ClockHigh1; loc ClockHigh1: while ckClock <= dClockHigh & ckClock >= 0 wait {} when True do {} goto ClockHigh1; end -- clock1 --****************************************************-- automaton d1 --****************************************************-- synclabs: clockUp1, dUp1, dDown1; initially DLow1; loc DLow1: while ckD<=dClockLow-dSetup & ckD >= 0 wait {} when ckD=dClockLow-dSetup sync dUp1 do {ckD' = 0} goto DHigh1; loc DHigh1: while ckD<=dSetup & ckD >= 0 wait {} when ckD=dSetup sync clockUp1 do {ckD' = 0} goto DHigh2; loc DHigh2: while ckD<=dHold & ckD >= 0 wait {} when ckD=dHold sync dDown1 do {} goto DLow2; loc DLow2: while ckD >= 0 wait {} when True do {} goto DLow2; end -- d1 --****************************************************-- automaton not1 --****************************************************-- synclabs: clockUp1, not1Down1; initially Not1High1; loc Not1High1: while ckNot1 >= 0 wait {} when True sync clockUp1 do {ckNot1' = 0} goto Not1High1bis; loc Not1High1bis: while ckNot1 <= dNot1Down_u & ckNot1 >= 0 wait {} when ckNot1 >= dNot1Down_l sync not1Down1 do {tNot1Down1' = s} goto Not1Low1; loc Not1Low1: while ckNot1 >= 0 wait {} when True do {} goto Not1Low1; end -- not1 --****************************************************-- automaton not2 --****************************************************-- synclabs: not1Down1, not2Up1; initially Not2Low1; loc Not2Low1: while ckNot2 >= 0 wait {} when True sync not1Down1 do {ckNot2' = 0} goto Not2Low1bis; loc Not2Low1bis: while ckNot2 <= dNot2Up_u & ckNot2 >= 0 wait {} when ckNot2 >= dNot2Up_l sync not2Up1 do {tNot2Up1' = s} goto Not2High1; loc Not2High1: while ckNot2 >= 0 wait {} when True do {} goto Not2High1; end -- not2 --****************************************************-- automaton xor1 --****************************************************-- synclabs: clockUp1, not2Up1, xorUp1, xorDown1; initially XorLow1; loc XorLow1: while ckXor >= 0 wait {} when True sync clockUp1 do {ckXor' = 0} goto XorLow1bis; loc XorLow1bis: while ckXor <= dXorUp2Up_u & ckXor >= 0 wait {} when ckXor >= dXorUp2Up_l sync xorUp1 do {tXorUp1' = s} goto XorHigh1; loc XorHigh1: while ckXor >= 0 wait {} when True sync not2Up1 do {ckXor' = 0} goto XorHigh1bis; loc XorHigh1bis: while ckXor <= dXorDown1Up_u & ckXor >= 0 wait {} when ckXor >= dXorDown1Up_l sync xorDown1 do {tXorDown1' = s} goto XorLow2; loc XorLow2: while ckXor >= 0 wait {} when True do {} goto XorLow2; end -- xor1 --****************************************************-- automaton and1 --****************************************************-- synclabs: clockUp1, xorDown1, andUp1, andDown1; initially AndLow1; loc AndLow1: while ckAnd >= 0 wait {} when True sync clockUp1 do {ckAnd' = 0} goto AndLow1bis; loc AndLow1bis: while ckAnd <= dAndUp2_u & ckAnd >= 0 wait {} when ckAnd >= dAndUp2_l sync andUp1 do {tAndUp1' = s} goto AndHigh1; loc AndHigh1: while ckAnd >= 0 wait {} when True sync xorDown1 do {ckAnd' = 0} goto AndHigh1bis; loc AndHigh1bis: while ckAnd <= dAndDown1_u & ckAnd >= 0 wait {} when ckAnd >= dAndDown1_l sync andDown1 do {tAndDown1' = s} goto AndLow2; loc AndLow2: while ckAnd >= 0 wait {} when True do {} goto AndLow2; end -- and1 --****************************************************-- automaton latch1 --****************************************************-- synclabs: dUp1, dDown1, andUp1, andDown1, latchUp1; initially LatchD0E0; loc LatchD0E0: while ckLatch >= 0 wait {} when True sync dUp1 do {} goto LatchD1E0; when True sync andUp1 do {ckLatch' = 0} goto LatchD0E1; loc LatchD0E1: while ckLatch >= 0 wait {} -- simplification : Q can not go down in our case when True sync dUp1 do {ckLatch' = 0} goto LatchD1E1; when True sync andDown1 do {} goto LatchD0E0; loc LatchD1E0: while ckLatch >= 0 wait {} when True sync andUp1 do {ckLatch' = 0} goto LatchD1E1; when True sync dDown1 do {} goto LatchD0E0; loc LatchD1E1: while ckLatch <= dLatchUp_u & ckLatch >= 0 wait {} when ckLatch >= dLatchUp_l sync latchUp1 do {tLatchUp1' = s, q'=1} goto LatchD1E1B; when True sync dDown1 do {} goto LatchD0E1; when True sync andDown1 do {} goto LatchD1E0; loc LatchD1E1B: while ckLatch >= 0 wait {} when True sync andDown1 do {} goto LatchD1E0; when True sync dDown1 do {} goto LatchD0E1; end -- latch1 --****************************************************-- --****************************************************-- -- ANALYSIS --****************************************************-- --****************************************************-- var init_reg, final_reg, post_reg, pre_reg, inter_reg : region; init_reg := ---------------------- -- Initial locations ---------------------- loc[clock1] = ClockLow1 & loc[d1] = DLow1 & loc[not1] = Not1High1 & loc[not2] = Not2Low1 & loc[xor1] = XorLow1 & loc[and1] = AndLow1 & loc[latch1] = LatchD0E0 ---------------------- -- Clocks ---------------------- & s = 0 & ckClock = 0 & ckD = 0 & ckNot1 = 0 & ckNot2 = 0 & ckXor = 0 & ckAnd = 0 & ckLatch = 0 & q=2 ---------------------- -- Parameters ---------------------- -- & dLatchUp_l>0 -- & dAndUp2_l >0 -- & dNot2Down_l>0 -- & dNot1Up_l>0 -- & dNot1Down_l>0 -- & dXorDown1Up_l>0 -- & dAndDown1_l>0 -- & dSetup>0 ---------------------- -- Instantiation of the parameters given by LIP6 (in ps) ---------------------- ---START PI0--- -- & dClockHigh = 1000 -- & dClockLow = 1000 -- & dNot1Down_l = 147 -- & dNot1Down_u = 147 -- & dNot1Up_l= 219 -- & dNot1Up_u = 219 -- & dNot2Down_l = 163 -- & dNot2Down_u = 163 -- & dNot2Up_l = 155 -- & dNot2Up_u = 155 -- & dXorUp2Up_l = 147 -- & dXorUp2Up_u = 147 -- & dXorDown1Up_l = 416 -- & dXorDown1Up_u = 416 -- & dAndUp2_l = 80 -- & dAndUp2_u = 80 -- & dAndDown1_l = 155 -- & dAndDown1_u = 155 -- & dLatchUp_l = 240 -- & dLatchUp_u = 240 -- & dHold = 350 -- & dSetup = 1 ---END PI0--- & dNot1Down_u = dNot1Down_l & dNot1Up_u = dNot1Up_l & dNot2Down_u = dNot2Down_l & dNot2Up_u = dNot2Up_l & dXorUp2Up_u = dXorUp2Up_l & dXorDown1Up_u = dXorDown1Up_l & dAndUp2_u = dAndUp2_l & dAndDown1_u = dAndDown1_l & dLatchUp_u = dLatchUp_l & dAndDown1_l>0 -- & dSetup = 140 -- valeur PATRICIA -- & dHold = -57 (!!!) -- valeur PATRICIA ---------------------- -- Resulting times and durations (in ps) ---------------------- -- & dSetup = 0 -- & dHold = 0 & tNot1Down1 = 0 & tNot2Up1 = 0 & tXorUp1 = 0 & tXorDown1 = 0 & tAndUp1 = 0 & tAndDown1 = 0 & tLatchUp1 = 0 ; --prints "--****************************************************--"; --prints " VALMEM Project : New circuit by Remi"; --prints "--****************************************************--"; --print init_reg; final_reg := True ---------------------- -- Final locations ---------------------- & loc[clock1] = ClockHigh1 & loc[d1] = DLow2 -- & loc[not1] = Not1High1 -- & loc[not2] = Not2Low1 -- & loc[xor1] = XorLow1 -- & loc[and1] = AndLow1 & loc[latch1] = LatchD0E0 ---------------------- -- Constraint to be fullfilled ---------------------- -- the latch did produce an output -- & tLatchUp1 > 0 & q=2 & s=dClockLow + dClockHigh & dLatchUp_l>0 & dAndUp2_l >0 & dNot2Down_l>0 & dNot1Up_l>0 & dNot1Down_l>0 & dXorDown1Up_l>0 & dAndDown1_l>0 & dSetup>0 & dHold>0 & dNot1Down_l = dNot1Down_u & dNot1Up_l = dNot1Up_u & dNot2Down_l = dNot2Down_u & dNot2Up_l = dNot2Up_u & dXorUp2Up_u = dXorUp2Up_l & dXorDown1Up_u = dXorDown1Up_l & dAndUp2_u = dAndUp2_l & dAndDown1_u = dAndDown1_l & dLatchUp_l = dLatchUp_u ; --prints "--****************************************************--"; --prints " Resulting states"; --prints "--****************************************************--"; post_reg := reach forward from init_reg endreach; prints "---START LOG---"; print(hide -- clocks s, ckClock, ckD, ckNot1, ckNot2, ckXor, ckAnd, ckLatch, -- given durations -- dClockLow, dClockHigh, -- dNot1Down_l, dNot1Up_l, dNot2Down_l, dNot2Up_l, dXorDown1Up_l, dXorUp2Up_l, dAndUp1_l, dAndUp2_l, dAndDown1_l, dAndDown2_l, dLatchUp_l, dNot1Down_u, dNot1Up_u, dNot2Down_u, dNot2Up_u, dXorDown1Up_u, dXorUp2Up_u, dAndUp1_u, dAndUp2_u, dAndDown1_u, dAndDown2_u, dLatchUp_u, -- unuseful results tNot1Down1, tNot2Up1, tXorUp1, tXorDown1, tAndUp1, tAndDown1, tLatchUp1, q in post_reg endhide); prints "---END LOG---"; --prints "--****************************************************--"; --prints " INTERSECTION WITH THE BAD STATE"; --prints "--****************************************************--"; --inter_reg := post_reg & final_reg; --print(hide -- -- clocks -- s, ckClock, ckD, ckNot1, ckNot2, ckXor, ckAnd, ckLatch, -- -- given durations -- dNot1Down_l, dNot1Up_l, -- dNot2Down_l, dNot2Up_l, -- dXorDown1Up_l, dXorUp2Up_l, -- dAndUp1_l, dAndUp2_l, dAndDown1_l, dAndDown2_l, -- dLatchUp_l, -- -- unuseful results -- tNot1Down1, -- tNot2Up1, -- tXorUp1, tXorDown1, -- tAndUp1, tAndDown1, -- tLatchUp1 --in -- inter_reg --endhide);