# vl2mv tlc.v # version: 0.2 # date: 13:31:53 12/11/95 (PST) .model main # I/O ports .mv car_present 2 YES NO .mv farm_light 3 GREEN YELLOW RED .mv hwy_light 3 GREEN YELLOW RED # assign start_timer = farm_start_timer || hwy_start_timer # farm_start_timer || hwy_start_timer .names farm_start_timer hwy_start_timer _n1 .def 1 0 0 0 .names _n1 start_timer$raw_n0 - =_n1 .subckt timer timer start=start_timer short=short_timer long=long_timer .subckt sensor sensor car_present=car_present .subckt farm_control farm_control car_present=car_present enable_farm=enable_farm short_timer=short_timer long_timer=long_timer farm_light=farm_light farm_start_timer=farm_start_timer enable_hwy=enable_hwy .subckt hwy_control hwy_control car_present=car_present enable_hwy=enable_hwy short_timer=short_timer long_timer=long_timer hwy_light=hwy_light hwy_start_timer=hwy_start_timer enable_farm=enable_farm # conflict arbitrators .names start_timer$raw_n0 start_timer 0 0 1 1 # non-blocking assignments # latches # quasi-continuous assignment .end .model timer # I/O ports .outputs short .outputs long .inputs start .mv state 3 START SHORT LONG # state = 0 .mv state$raw_n2 3 START SHORT LONG .names state$raw_n2 START # non-blocking assignments for initial # assign rand_choice = $NDset ( 0,1 ) .names rand_choice 0 1 # assign short = ((state == SHORT ) || (state == LONG )) .mv _n7 3 START SHORT LONG .names _n7 SHORT # state == 1 .names state _n7 _n6 .def 0 - =state 1 .mv _n9 3 START SHORT LONG .names _n9 LONG # state == 2 .names state _n9 _n8 .def 0 - =state 1 # (state == 1) || (state == 2) .names _n6 _n8 _na .def 1 0 0 0 .names _na short$raw_n5 - =_na # assign long = (state == LONG ) .mv _nd 3 START SHORT LONG .names _nd LONG # state == 2 .names state _nd _nc .def 0 - =state 1 .names _nc long$raw_nb - =_nc .names start _ne - =start # state = 0 .mv state$start_nf$true 3 START SHORT LONG .names state$start_nf$true START .mv _n12 3 START SHORT LONG .names _n12 START .names state _n12 _n11 .def 0 - =state 1 .names _n11 _n10 1 1 0 0 .names _n14 1 # rand_choice == 1 .names rand_choice _n14 _n15 .def 0 0 1 1 1 0 1 .names _n15 _n13 0 1 1 0 .names _n13 _n17 - =_n13 # state = 1 .mv state$_n13_n18$true 3 START SHORT LONG .names state$_n13_n18$true SHORT # if/else (rand_choice == 1) .mv state$_n13$raw_n1b 3 START SHORT LONG .names state$_n13_n18$true state _n13 state$_n13$raw_n1b - - 0 =state - - 1 =state$_n13_n18$true .mv _n1e 3 START SHORT LONG .names _n1e SHORT .names state _n1e _n1d .def 0 - =state 1 .names _n1d _n1c 1 1 0 0 .names _n20 1 # rand_choice == 1 .names rand_choice _n20 _n21 .def 0 0 1 1 1 0 1 .names _n21 _n1f 0 1 1 0 .names _n1f _n23 - =_n1f # state = 2 .mv state$_n1f_n24$true 3 START SHORT LONG .names state$_n1f_n24$true LONG # if/else (rand_choice == 1) .mv state$_n1f$raw_n27 3 START SHORT LONG .names state$_n1f_n24$true state _n1f state$_n1f$raw_n27 - - 0 =state - - 1 =state$_n1f_n24$true # case (state ) .mv state$_n1c$raw_n2a 3 START SHORT LONG .names state$_n1f$raw_n27 state _n1c state$_n1c$raw_n2a - - 0 =state - - 1 =state$_n1f$raw_n27 .mv state$_n10$raw_n2b 3 START SHORT LONG .names state$_n13$raw_n1b state$_n1c$raw_n2a _n10 state$_n10$raw_n2b - - 0 =state$_n1c$raw_n2a - - 1 =state$_n13$raw_n1b # if/else (start ) .mv state$start$raw_n30 3 START SHORT LONG .names state$start_nf$true state$_n10$raw_n2b start state$start$raw_n30 - - 0 =state$_n10$raw_n2b - - 1 =state$start_nf$true # conflict arbitrators .names short$raw_n5 short 0 0 1 1 .names long$raw_nb long 0 0 1 1 .names _ne _n10 _n17 _n1c _n23 _n33 .def 0 1 - - - - 1 0 1 1 - - 1 0 0 - 1 1 1 .mv _n34 3 START SHORT LONG .names _n33 state$start$raw_n30 state _n34 1 - - =state$start$raw_n30 0 - - =state # non-blocking assignments # latches .r state$raw_n2 state - =state$raw_n2 .latch _n34 state # quasi-continuous assignment .end .model sensor # I/O ports .outputs car_present .mv car_present 2 YES NO # car_present = 1 .mv car_present$raw_n3a 2 YES NO .names car_present$raw_n3a NO # non-blocking assignments for initial # assign rand_choice = $NDset ( 0,1 ) .names rand_choice 0 1 .names _n3e 0 # rand_choice == 0 .names rand_choice _n3e _n3f .def 0 0 1 1 1 0 1 .names _n3f _n3d 0 1 1 0 .names _n3d _n41 - =_n3d # car_present = 1 .mv car_present$_n3d_n42$true 2 YES NO .names car_present$_n3d_n42$true NO # car_present = 0 .mv car_present$_n3d_n43$false 2 YES NO .names car_present$_n3d_n43$false YES # if/else (rand_choice == 0) .mv car_present$_n3d$raw_n45 2 YES NO .names car_present$_n3d_n42$true car_present$_n3d_n43$false _n3d car_present$_n3d$raw_n45 - - 0 =car_present$_n3d_n43$false - - 1 =car_present$_n3d_n42$true # conflict arbitrators .names _n41 _n48 .def 0 1 1 0 1 .mv _n49 2 YES NO .names _n48 car_present$_n3d$raw_n45 car_present _n49 1 - - =car_present$_n3d$raw_n45 0 - - =car_present # non-blocking assignments # latches .r car_present$raw_n3a car_present - =car_present$raw_n3a .latch _n49 car_present # quasi-continuous assignment .end .model farm_control # I/O ports .inputs car_present .outputs farm_light .inputs enable_farm .inputs long_timer .inputs short_timer .outputs farm_start_timer .outputs enable_hwy .mv car_present 2 YES NO .mv farm_light 3 GREEN YELLOW RED # farm_light = 2 .mv farm_light$raw_n4c 3 GREEN YELLOW RED .names farm_light$raw_n4c RED # non-blocking assignments for initial # assign farm_start_timer = (((farm_light == GREEN ) && ((car_present == NO ) || long_timer )) || (farm_light == RED ) && enable_farm ) .mv _n4f 3 GREEN YELLOW RED .names _n4f GREEN # farm_light == 0 .names farm_light _n4f _n4e .def 0 - =farm_light 1 .mv _n51 2 YES NO .names _n51 NO # car_present == 1 .names car_present _n51 _n50 .def 0 - =car_present 1 # (car_present == 1) || long_timer .names _n50 long_timer _n52 .def 1 0 0 0 # (farm_light == 0) && ((car_present == 1) || long_timer ) .names _n4e _n52 _n53 .def 0 1 1 1 .mv _n55 3 GREEN YELLOW RED .names _n55 RED # farm_light == 2 .names farm_light _n55 _n54 .def 0 - =farm_light 1 # (farm_light == 2) && enable_farm .names _n54 enable_farm _n56 .def 0 1 1 1 # ((farm_light == 0) && ((car_present == 1) || long_timer )) || (farm_light == 2) && enable_farm .names _n53 _n56 _n57 .def 1 0 0 0 .names _n57 farm_start_timer$raw_n4d - =_n57 # assign enable_hwy = ((farm_light == YELLOW ) && short_timer ) .mv _n5a 3 GREEN YELLOW RED .names _n5a YELLOW # farm_light == 1 .names farm_light _n5a _n59 .def 0 - =farm_light 1 # (farm_light == 1) && short_timer .names _n59 short_timer _n5b .def 0 1 1 1 .names _n5b enable_hwy$raw_n58 - =_n5b .mv _n5e 3 GREEN YELLOW RED .names _n5e GREEN .names farm_light _n5e _n5d .def 0 - =farm_light 1 .names _n5d _n5c 1 1 0 0 .mv _n60 2 YES NO .names _n60 NO # car_present == 1 .names car_present _n60 _n5f .def 0 - =car_present 1 # (car_present == 1) || long_timer .names _n5f long_timer _n61 .def 1 0 0 0 .names _n61 _n62 - =_n61 # farm_light = 1 .mv farm_light$_n61_n63$true 3 GREEN YELLOW RED .names farm_light$_n61_n63$true YELLOW # if/else ((car_present == 1) || long_timer ) .mv farm_light$_n61$raw_n66 3 GREEN YELLOW RED .names farm_light$_n61_n63$true farm_light _n61 farm_light$_n61$raw_n66 - - 0 =farm_light - - 1 =farm_light$_n61_n63$true .mv _n69 3 GREEN YELLOW RED .names _n69 YELLOW .names farm_light _n69 _n68 .def 0 - =farm_light 1 .names _n68 _n67 1 1 0 0 .names short_timer _n6a - =short_timer # farm_light = 2 .mv farm_light$short_timer_n6b$true 3 GREEN YELLOW RED .names farm_light$short_timer_n6b$true RED # if/else (short_timer ) .mv farm_light$short_timer$raw_n6e 3 GREEN YELLOW RED .names farm_light$short_timer_n6b$true farm_light short_timer farm_light$short_timer$raw_n6e - - 0 =farm_light - - 1 =farm_light$short_timer_n6b$true .mv _n71 3 GREEN YELLOW RED .names _n71 RED .names farm_light _n71 _n70 .def 0 - =farm_light 1 .names _n70 _n6f 1 1 0 0 .names enable_farm _n72 - =enable_farm # farm_light = 0 .mv farm_light$enable_farm_n73$true 3 GREEN YELLOW RED .names farm_light$enable_farm_n73$true GREEN # if/else (enable_farm ) .mv farm_light$enable_farm$raw_n76 3 GREEN YELLOW RED .names farm_light$enable_farm_n73$true farm_light enable_farm farm_light$enable_farm$raw_n76 - - 0 =farm_light - - 1 =farm_light$enable_farm_n73$true # case (farm_light ) .mv farm_light$_n6f$raw_n79 3 GREEN YELLOW RED .names farm_light$enable_farm$raw_n76 farm_light _n6f farm_light$_n6f$raw_n79 - - 0 =farm_light - - 1 =farm_light$enable_farm$raw_n76 .mv farm_light$_n67$raw_n7a 3 GREEN YELLOW RED .names farm_light$short_timer$raw_n6e farm_light$_n6f$raw_n79 _n67 farm_light$_n67$raw_n7a - - 0 =farm_light$_n6f$raw_n79 - - 1 =farm_light$short_timer$raw_n6e .mv farm_light$_n5c$raw_n7e 3 GREEN YELLOW RED .names farm_light$_n61$raw_n66 farm_light$_n67$raw_n7a _n5c farm_light$_n5c$raw_n7e - - 0 =farm_light$_n67$raw_n7a - - 1 =farm_light$_n61$raw_n66 # conflict arbitrators .names _n5c _n62 _n67 _n6a _n6f _n72 _n82 .def 0 1 1 - - - - 1 0 - 1 1 - - 1 0 - 0 - 1 1 1 .mv _n83 3 GREEN YELLOW RED .names _n82 farm_light$_n5c$raw_n7e farm_light _n83 1 - - =farm_light$_n5c$raw_n7e 0 - - =farm_light .names farm_start_timer$raw_n4d farm_start_timer 0 0 1 1 .names enable_hwy$raw_n58 enable_hwy 0 0 1 1 # non-blocking assignments # latches .r farm_light$raw_n4c farm_light - =farm_light$raw_n4c .latch _n83 farm_light # quasi-continuous assignment .end .model hwy_control # I/O ports .inputs car_present .outputs enable_farm .inputs long_timer .inputs short_timer .outputs hwy_light .outputs hwy_start_timer .inputs enable_hwy .mv car_present 2 YES NO .mv hwy_light 3 GREEN YELLOW RED # hwy_light = 0 .mv hwy_light$raw_n8b 3 GREEN YELLOW RED .names hwy_light$raw_n8b GREEN # non-blocking assignments for initial # assign hwy_start_timer = (((hwy_light == GREEN ) && ((car_present == YES ) && long_timer )) || (hwy_light == RED ) && enable_hwy ) .mv _n8e 3 GREEN YELLOW RED .names _n8e GREEN # hwy_light == 0 .names hwy_light _n8e _n8d .def 0 - =hwy_light 1 .mv _n90 2 YES NO .names _n90 YES # car_present == 0 .names car_present _n90 _n8f .def 0 - =car_present 1 # (car_present == 0) && long_timer .names _n8f long_timer _n91 .def 0 1 1 1 # (hwy_light == 0) && ((car_present == 0) && long_timer ) .names _n8d _n91 _n92 .def 0 1 1 1 .mv _n94 3 GREEN YELLOW RED .names _n94 RED # hwy_light == 2 .names hwy_light _n94 _n93 .def 0 - =hwy_light 1 # (hwy_light == 2) && enable_hwy .names _n93 enable_hwy _n95 .def 0 1 1 1 # ((hwy_light == 0) && ((car_present == 0) && long_timer )) || (hwy_light == 2) && enable_hwy .names _n92 _n95 _n96 .def 1 0 0 0 .names _n96 hwy_start_timer$raw_n8c - =_n96 # assign enable_farm = ((hwy_light == YELLOW ) && short_timer ) .mv _n99 3 GREEN YELLOW RED .names _n99 YELLOW # hwy_light == 1 .names hwy_light _n99 _n98 .def 0 - =hwy_light 1 # (hwy_light == 1) && short_timer .names _n98 short_timer _n9a .def 0 1 1 1 .names _n9a enable_farm$raw_n97 - =_n9a .mv _n9d 3 GREEN YELLOW RED .names _n9d GREEN .names hwy_light _n9d _n9c .def 0 - =hwy_light 1 .names _n9c _n9b 1 1 0 0 .mv _n9f 2 YES NO .names _n9f YES # car_present == 0 .names car_present _n9f _n9e .def 0 - =car_present 1 # (car_present == 0) && long_timer .names _n9e long_timer _na0 .def 0 1 1 1 .names _na0 _na1 - =_na0 # hwy_light = 1 .mv hwy_light$_na0_na2$true 3 GREEN YELLOW RED .names hwy_light$_na0_na2$true YELLOW # if/else ((car_present == 0) && long_timer ) .mv hwy_light$_na0$raw_na5 3 GREEN YELLOW RED .names hwy_light$_na0_na2$true hwy_light _na0 hwy_light$_na0$raw_na5 - - 0 =hwy_light - - 1 =hwy_light$_na0_na2$true .mv _na8 3 GREEN YELLOW RED .names _na8 YELLOW .names hwy_light _na8 _na7 .def 0 - =hwy_light 1 .names _na7 _na6 1 1 0 0 .names short_timer _na9 - =short_timer # hwy_light = 2 .mv hwy_light$short_timer_naa$true 3 GREEN YELLOW RED .names hwy_light$short_timer_naa$true RED # if/else (short_timer ) .mv hwy_light$short_timer$raw_nad 3 GREEN YELLOW RED .names hwy_light$short_timer_naa$true hwy_light short_timer hwy_light$short_timer$raw_nad - - 0 =hwy_light - - 1 =hwy_light$short_timer_naa$true .mv _nb0 3 GREEN YELLOW RED .names _nb0 RED .names hwy_light _nb0 _naf .def 0 - =hwy_light 1 .names _naf _nae 1 1 0 0 .names enable_hwy _nb1 - =enable_hwy # hwy_light = 0 .mv hwy_light$enable_hwy_nb2$true 3 GREEN YELLOW RED .names hwy_light$enable_hwy_nb2$true GREEN # if/else (enable_hwy ) .mv hwy_light$enable_hwy$raw_nb5 3 GREEN YELLOW RED .names hwy_light$enable_hwy_nb2$true hwy_light enable_hwy hwy_light$enable_hwy$raw_nb5 - - 0 =hwy_light - - 1 =hwy_light$enable_hwy_nb2$true # case (hwy_light ) .mv hwy_light$_nae$raw_nb8 3 GREEN YELLOW RED .names hwy_light$enable_hwy$raw_nb5 hwy_light _nae hwy_light$_nae$raw_nb8 - - 0 =hwy_light - - 1 =hwy_light$enable_hwy$raw_nb5 .mv hwy_light$_na6$raw_nb9 3 GREEN YELLOW RED .names hwy_light$short_timer$raw_nad hwy_light$_nae$raw_nb8 _na6 hwy_light$_na6$raw_nb9 - - 0 =hwy_light$_nae$raw_nb8 - - 1 =hwy_light$short_timer$raw_nad .mv hwy_light$_n9b$raw_nbd 3 GREEN YELLOW RED .names hwy_light$_na0$raw_na5 hwy_light$_na6$raw_nb9 _n9b hwy_light$_n9b$raw_nbd - - 0 =hwy_light$_na6$raw_nb9 - - 1 =hwy_light$_na0$raw_na5 # conflict arbitrators .names enable_farm$raw_n97 enable_farm 0 0 1 1 .names _n9b _na1 _na6 _na9 _nae _nb1 _nc1 .def 0 1 1 - - - - 1 0 - 1 1 - - 1 0 - 0 - 1 1 1 .mv _nc2 3 GREEN YELLOW RED .names _nc1 hwy_light$_n9b$raw_nbd hwy_light _nc2 1 - - =hwy_light$_n9b$raw_nbd 0 - - =hwy_light .names hwy_start_timer$raw_n8c hwy_start_timer 0 0 1 1 # non-blocking assignments # latches .r hwy_light$raw_n8b hwy_light - =hwy_light$raw_n8b .latch _nc2 hwy_light # quasi-continuous assignment .end