# vl2mv crd.v # version: 0.2 # date: 11:12:45 12/11/95 (PST) .model environment # I/O ports .outputs test .outputs status_A .mv status_B 3 no_cars car_waiting cars_passing .mv signal_B 3 stop go slow .mv status_A 3 no_cars car_waiting cars_passing .mv signal_A 3 stop go slow .mv signal 3 go_slow go_A go_B .subckt POLICEMAN police status_A=status_A status_B=status_B signal=signal # assign signal_A = (signal == go_A ) ? 1 : (signal == go_slow ) ? 2 : 0 .mv signal_A$raw_n0 3 stop go slow .mv _n2 3 go_slow go_A go_B .names _n2 go_A # signal == 1 .names signal _n2 _n1 .def 0 - =signal 1 .mv _n4 3 go_slow go_A go_B .names _n4 go_slow # signal == 0 .names signal _n4 _n3 .def 0 - =signal 1 .mv _n5 3 stop go slow .names _n5 slow .mv _n6 3 stop go slow .names _n6 stop # (signal == 0) ? 2 : 0 .mv _n7 3 stop go slow .names _n5 _n6 _n3 _n7 - - 0 =_n6 - - 1 =_n5 .mv _n8 3 stop go slow .names _n8 go # (signal == 1) ? 1 : (signal == 0) ? 2 : 0 .mv _n9 3 stop go slow .names _n8 _n7 _n1 _n9 - - 0 =_n7 - - 1 =_n8 .names _n9 signal_A$raw_n0 - =_n9 # assign signal_B = (signal == go_B ) ? 1 : (signal == go_slow ) ? 2 : 0 .mv signal_B$raw_na 3 stop go slow .mv _nc 3 go_slow go_A go_B .names _nc go_B # signal == 2 .names signal _nc _nb .def 0 - =signal 1 .mv _ne 3 go_slow go_A go_B .names _ne go_slow # signal == 0 .names signal _ne _nd .def 0 - =signal 1 .mv _nf 3 stop go slow .names _nf slow .mv _n10 3 stop go slow .names _n10 stop # (signal == 0) ? 2 : 0 .mv _n11 3 stop go slow .names _nf _n10 _nd _n11 - - 0 =_n10 - - 1 =_nf .mv _n12 3 stop go slow .names _n12 go # (signal == 2) ? 1 : (signal == 0) ? 2 : 0 .mv _n13 3 stop go slow .names _n12 _n11 _nb _n13 - - 0 =_n11 - - 1 =_n12 .names _n13 signal_B$raw_na - =_n13 .subckt ROAD road_A signal=signal_A status=status_A .subckt ROAD road_B signal=signal_B status=status_B # assign test = ((status_A == cars_passing ) && (status_B == cars_passing )) ? 0 : 1 .mv _n16 3 no_cars car_waiting cars_passing .names _n16 cars_passing # status_A == 2 .names status_A _n16 _n15 .def 0 - =status_A 1 .mv _n18 3 no_cars car_waiting cars_passing .names _n18 cars_passing # status_B == 2 .names status_B _n18 _n17 .def 0 - =status_B 1 # (status_A == 2) && (status_B == 2) .names _n15 _n17 _n19 .def 0 1 1 1 .names _n1a 0 .names _n1b 1 # ((status_A == 2) && (status_B == 2)) ? 0 : 1 .names _n1a _n1b _n19 _n1c 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n1c test$raw_n14 - =_n1c .subckt collision col status_A=status_A status_B=status_B .subckt starvation starv stat=status_A # conflict arbitrators .names test$raw_n14 test 0 0 1 1 .names signal_B$raw_na signal_B - =signal_B$raw_na .names signal_A$raw_n0 signal_A - =signal_A$raw_n0 # non-blocking assignments # latches # quasi-continuous assignment .end .model POLICEMAN # I/O ports .inputs status_B .inputs status_A .outputs signal .mv status_B 3 no_cars car_waiting cars_passing .mv status_A 3 no_cars car_waiting cars_passing .mv signal 3 go_slow go_A go_B .mv state 4 go_A_init go_A_state go_B_init go_B_state # assign ri_state = $NDset ( 0,1 ) .names ri_state 0 1 .names _n22 0 .names ri_state _n22 _n23 .def 0 0 1 1 1 0 1 .names _n23 _n21 0 1 1 0 .names _n21 _n20 1 1 0 0 # state = 0 .mv state$_n20_n25$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n20_n25$true go_A_init .names _n28 1 .names ri_state _n28 _n29 .def 0 0 1 1 1 0 1 .names _n29 _n27 0 1 1 0 .names _n27 _n26 1 1 0 0 # state = 2 .mv state$_n26_n2b$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n26_n2b$true go_B_init # case (ri_state ) .mv state$_n26$raw_n2e 4 go_A_init go_A_state go_B_init go_B_state .names state$_n26_n2b$true state$_n26_n2b$true _n26 state$_n26$raw_n2e - - 0 =state$_n26_n2b$true - - 1 =state$_n26_n2b$true .mv state$_n20$raw_n2f 4 go_A_init go_A_state go_B_init go_B_state .names state$_n20_n25$true state$_n26$raw_n2e _n20 state$_n20$raw_n2f - - 0 =state$_n26$raw_n2e - - 1 =state$_n20_n25$true # non-blocking assignments for initial # assign signal = ((state == go_A_init ) || (state == go_B_init )) ? 0 : (state == go_A_state ) ? 1 : 2 .mv signal$raw_n33 3 go_slow go_A go_B .mv _n35 4 go_A_init go_A_state go_B_init go_B_state .names _n35 go_A_init # state == 0 .names state _n35 _n34 .def 0 - =state 1 .mv _n37 4 go_A_init go_A_state go_B_init go_B_state .names _n37 go_B_init # state == 2 .names state _n37 _n36 .def 0 - =state 1 # (state == 0) || (state == 2) .names _n34 _n36 _n38 .def 1 0 0 0 .mv _n3a 4 go_A_init go_A_state go_B_init go_B_state .names _n3a go_A_state # state == 1 .names state _n3a _n39 .def 0 - =state 1 .mv _n3b 3 go_slow go_A go_B .names _n3b go_A .mv _n3c 3 go_slow go_A go_B .names _n3c go_B # (state == 1) ? 1 : 2 .mv _n3d 3 go_slow go_A go_B .names _n3b _n3c _n39 _n3d - - 0 =_n3c - - 1 =_n3b .mv _n3e 3 go_slow go_A go_B .names _n3e go_slow # ((state == 0) || (state == 2)) ? 0 : (state == 1) ? 1 : 2 .mv _n3f 3 go_slow go_A go_B .names _n3e _n3d _n38 _n3f - - 0 =_n3d - - 1 =_n3e .names _n3f signal$raw_n33 - =_n3f # assign r_state = $NDset ( 0,1 ) .names r_state 0 1 .mv _n44 4 go_A_init go_A_state go_B_init go_B_state .names _n44 go_A_init .names state _n44 _n43 .def 0 - =state 1 .names _n43 _n42 1 1 0 0 .names _n47 0 .names r_state _n47 _n48 .def 0 0 1 1 1 0 1 .names _n48 _n46 0 1 1 0 .names _n46 _n45 1 1 0 0 # state = 0 .mv state$_n45_n4a$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n45_n4a$true go_A_init .names _n4d 1 .names r_state _n4d _n4e .def 0 0 1 1 1 0 1 .names _n4e _n4c 0 1 1 0 .names _n4c _n4b 1 1 0 0 # state = 1 .mv state$_n4b_n50$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n4b_n50$true go_A_state # case (r_state ) .mv state$_n4b$raw_n53 4 go_A_init go_A_state go_B_init go_B_state .names state$_n4b_n50$true state _n4b state$_n4b$raw_n53 - - 0 =state - - 1 =state$_n4b_n50$true .mv state$_n45$raw_n54 4 go_A_init go_A_state go_B_init go_B_state .names state$_n45_n4a$true state$_n4b$raw_n53 _n45 state$_n45$raw_n54 - - 0 =state$_n4b$raw_n53 - - 1 =state$_n45_n4a$true .mv _n5a 4 go_A_init go_A_state go_B_init go_B_state .names _n5a go_B_init .names state _n5a _n59 .def 0 - =state 1 .names _n59 _n58 1 1 0 0 .names _n5d 0 .names r_state _n5d _n5e .def 0 0 1 1 1 0 1 .names _n5e _n5c 0 1 1 0 .names _n5c _n5b 1 1 0 0 # state = 2 .mv state$_n5b_n60$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n5b_n60$true go_B_init .names _n63 1 .names r_state _n63 _n64 .def 0 0 1 1 1 0 1 .names _n64 _n62 0 1 1 0 .names _n62 _n61 1 1 0 0 # state = 3 .mv state$_n61_n66$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n61_n66$true go_B_state # case (r_state ) .mv state$_n61$raw_n69 4 go_A_init go_A_state go_B_init go_B_state .names state$_n61_n66$true state _n61 state$_n61$raw_n69 - - 0 =state - - 1 =state$_n61_n66$true .mv state$_n5b$raw_n6a 4 go_A_init go_A_state go_B_init go_B_state .names state$_n5b_n60$true state$_n61$raw_n69 _n5b state$_n5b$raw_n6a - - 0 =state$_n61$raw_n69 - - 1 =state$_n5b_n60$true .mv _n6f 3 go_slow go_A go_B .names _n6f go_A # signal == 1 .names signal _n6f _n6e .def 0 - =signal 1 .mv _n71 3 no_cars car_waiting cars_passing .names _n71 car_waiting # status_B == 1 .names status_B _n71 _n70 .def 0 - =status_B 1 # (signal == 1) && (status_B == 1) .names _n6e _n70 _n72 .def 0 1 1 1 .names _n72 _n73 - =_n72 # state = 2 .mv state$_n72_n74$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n72_n74$true go_B_init .mv _n76 3 go_slow go_A go_B .names _n76 go_B # signal == 2 .names signal _n76 _n75 .def 0 - =signal 1 .mv _n78 3 no_cars car_waiting cars_passing .names _n78 car_waiting # status_A == 1 .names status_A _n78 _n77 .def 0 - =status_A 1 # (signal == 2) && (status_A == 1) .names _n75 _n77 _n79 .def 0 1 1 1 .names _n79 _n7a - =_n79 # state = 0 .mv state$_n79_n7b$true 4 go_A_init go_A_state go_B_init go_B_state .names state$_n79_n7b$true go_A_init # if/else ((signal == 2) && (status_A == 1)) .mv state$_n79$raw_n7e 4 go_A_init go_A_state go_B_init go_B_state .names state$_n79_n7b$true state _n79 state$_n79$raw_n7e - - 0 =state - - 1 =state$_n79_n7b$true # if/else ((signal == 1) && (status_B == 1)) .mv state$_n72$raw_n80 4 go_A_init go_A_state go_B_init go_B_state .names state$_n72_n74$true state$_n79$raw_n7e _n72 state$_n72$raw_n80 - - 0 =state$_n79$raw_n7e - - 1 =state$_n72_n74$true # case (state ) .mv state$_n58$raw_n84 4 go_A_init go_A_state go_B_init go_B_state .names state$_n5b$raw_n6a state$_n72$raw_n80 _n58 state$_n58$raw_n84 - - 0 =state$_n72$raw_n80 - - 1 =state$_n5b$raw_n6a .mv state$_n42$raw_n88 4 go_A_init go_A_state go_B_init go_B_state .names state$_n45$raw_n54 state$_n58$raw_n84 _n42 state$_n42$raw_n88 - - 0 =state$_n58$raw_n84 - - 1 =state$_n45$raw_n54 # conflict arbitrators .names signal$raw_n33 signal - =signal$raw_n33 .names _n42 _n45 _n4b _n58 _n5b _n61 _n73 _n7a _n8b .def 0 1 1 - - - - - - 1 1 0 1 - - - - - 1 0 - - 1 1 - - - 1 0 - - 1 0 1 - - 1 0 - - 0 - - 1 - 1 0 - - 0 - - 0 1 1 .mv _n8c 4 go_A_init go_A_state go_B_init go_B_state .names _n8b state$_n42$raw_n88 state _n8c 1 - - =state$_n42$raw_n88 0 - - =state # non-blocking assignments # latches .r state$_n20$raw_n2f state - =state$_n20$raw_n2f .latch _n8c state # quasi-continuous assignment .end .model ROAD # I/O ports .outputs status .inputs signal .mv status 3 no_cars car_waiting cars_passing .mv signal 3 stop go slow .mv state 4 STOPPED_init STOPPED GO_init GO # state = 0 .mv state$raw_n93 4 STOPPED_init STOPPED GO_init GO .names state$raw_n93 STOPPED_init # non-blocking assignments for initial # assign status = (state == STOPPED_init ) ? 0 : (state == STOPPED ) ? 1 : (state == GO_init ) ? 2 : (state == GO ) ? 0 : 0 .mv status$raw_n94 3 no_cars car_waiting cars_passing .mv _n96 4 STOPPED_init STOPPED GO_init GO .names _n96 STOPPED_init # state == 0 .names state _n96 _n95 .def 0 - =state 1 .mv _n98 4 STOPPED_init STOPPED GO_init GO .names _n98 STOPPED # state == 1 .names state _n98 _n97 .def 0 - =state 1 .mv _n9a 4 STOPPED_init STOPPED GO_init GO .names _n9a GO_init # state == 2 .names state _n9a _n99 .def 0 - =state 1 .mv _n9c 4 STOPPED_init STOPPED GO_init GO .names _n9c GO # state == 3 .names state _n9c _n9b .def 0 - =state 1 .mv _n9d 3 no_cars car_waiting cars_passing .names _n9d no_cars .mv _n9e 3 no_cars car_waiting cars_passing .names _n9e no_cars # (state == 3) ? 0 : 0 .mv _n9f 3 no_cars car_waiting cars_passing .names _n9d _n9e _n9b _n9f - - 0 =_n9e - - 1 =_n9d .mv _na0 3 no_cars car_waiting cars_passing .names _na0 cars_passing # (state == 2) ? 2 : (state == 3) ? 0 : 0 .mv _na1 3 no_cars car_waiting cars_passing .names _na0 _n9f _n99 _na1 - - 0 =_n9f - - 1 =_na0 .mv _na2 3 no_cars car_waiting cars_passing .names _na2 car_waiting # (state == 1) ? 1 : (state == 2) ? 2 : (state == 3) ? 0 : 0 .mv _na3 3 no_cars car_waiting cars_passing .names _na2 _na1 _n97 _na3 - - 0 =_na1 - - 1 =_na2 .mv _na4 3 no_cars car_waiting cars_passing .names _na4 no_cars # (state == 0) ? 0 : (state == 1) ? 1 : (state == 2) ? 2 : (state == 3) ? 0 : 0 .mv _na5 3 no_cars car_waiting cars_passing .names _na4 _na3 _n95 _na5 - - 0 =_na3 - - 1 =_na4 .names _na5 status$raw_n94 - =_na5 # assign r_state = $NDset ( 0,1 ) .names r_state 0 1 .mv _naa 4 STOPPED_init STOPPED GO_init GO .names _naa STOPPED_init .names state _naa _na9 .def 0 - =state 1 .names _na9 _na8 1 1 0 0 .names _nad 0 .names r_state _nad _nae .def 0 0 1 1 1 0 1 .names _nae _nac 0 1 1 0 .names _nac _nab 1 1 0 0 # state = 0 .mv state$_nab_nb0$true 4 STOPPED_init STOPPED GO_init GO .names state$_nab_nb0$true STOPPED_init .names _nb3 1 .names r_state _nb3 _nb4 .def 0 0 1 1 1 0 1 .names _nb4 _nb2 0 1 1 0 .names _nb2 _nb1 1 1 0 0 # state = 1 .mv state$_nb1_nb6$true 4 STOPPED_init STOPPED GO_init GO .names state$_nb1_nb6$true STOPPED # case (r_state ) .mv state$_nb1$raw_nb9 4 STOPPED_init STOPPED GO_init GO .names state$_nb1_nb6$true state _nb1 state$_nb1$raw_nb9 - - 0 =state - - 1 =state$_nb1_nb6$true .mv state$_nab$raw_nba 4 STOPPED_init STOPPED GO_init GO .names state$_nab_nb0$true state$_nb1$raw_nb9 _nab state$_nab$raw_nba - - 0 =state$_nb1$raw_nb9 - - 1 =state$_nab_nb0$true .mv _nc0 4 STOPPED_init STOPPED GO_init GO .names _nc0 STOPPED .names state _nc0 _nbf .def 0 - =state 1 .names _nbf _nbe 1 1 0 0 .mv _nc2 3 stop go slow .names _nc2 go # signal == 1 .names signal _nc2 _nc1 .def 0 - =signal 1 .names _nc1 _nc3 - =_nc1 # state = 2 .mv state$_nc1_nc4$true 4 STOPPED_init STOPPED GO_init GO .names state$_nc1_nc4$true GO_init # if/else (signal == 1) .mv state$_nc1$raw_nc7 4 STOPPED_init STOPPED GO_init GO .names state$_nc1_nc4$true state _nc1 state$_nc1$raw_nc7 - - 0 =state - - 1 =state$_nc1_nc4$true .mv _nca 4 STOPPED_init STOPPED GO_init GO .names _nca GO_init .names state _nca _nc9 .def 0 - =state 1 .names _nc9 _nc8 1 1 0 0 .mv _ncc 3 stop go slow .names _ncc stop # signal == 0 .names signal _ncc _ncb .def 0 - =signal 1 .names _ncb _ncd - =_ncb # state = 0 .mv state$_ncb_nce$true 4 STOPPED_init STOPPED GO_init GO .names state$_ncb_nce$true STOPPED_init .names _nd1 0 .names r_state _nd1 _nd2 .def 0 0 1 1 1 0 1 .names _nd2 _nd0 0 1 1 0 .names _nd0 _ncf 1 1 0 0 # state = 2 .mv state$_ncf_nd4$true 4 STOPPED_init STOPPED GO_init GO .names state$_ncf_nd4$true GO_init .names _nd7 1 .names r_state _nd7 _nd8 .def 0 0 1 1 1 0 1 .names _nd8 _nd6 0 1 1 0 .names _nd6 _nd5 1 1 0 0 # state = 3 .mv state$_nd5_nda$true 4 STOPPED_init STOPPED GO_init GO .names state$_nd5_nda$true GO # case (r_state ) .mv state$_nd5$raw_ndd 4 STOPPED_init STOPPED GO_init GO .names state$_nd5_nda$true state _nd5 state$_nd5$raw_ndd - - 0 =state - - 1 =state$_nd5_nda$true .mv state$_ncf$raw_nde 4 STOPPED_init STOPPED GO_init GO .names state$_ncf_nd4$true state$_nd5$raw_ndd _ncf state$_ncf$raw_nde - - 0 =state$_nd5$raw_ndd - - 1 =state$_ncf_nd4$true # if/else (signal == 0) .mv state$_ncb$raw_ne3 4 STOPPED_init STOPPED GO_init GO .names state$_ncb_nce$true state$_ncf$raw_nde _ncb state$_ncb$raw_ne3 - - 0 =state$_ncf$raw_nde - - 1 =state$_ncb_nce$true .mv _ne8 4 STOPPED_init STOPPED GO_init GO .names _ne8 GO .names state _ne8 _ne7 .def 0 - =state 1 .names _ne7 _ne6 1 1 0 0 # state = 0 .mv state$_ne6_ne9$true 4 STOPPED_init STOPPED GO_init GO .names state$_ne6_ne9$true STOPPED_init # case (state ) .mv state$_ne6$raw_nec 4 STOPPED_init STOPPED GO_init GO .names state$_ne6_ne9$true state _ne6 state$_ne6$raw_nec - - 0 =state - - 1 =state$_ne6_ne9$true .mv state$_nc8$raw_nee 4 STOPPED_init STOPPED GO_init GO .names state$_ncb$raw_ne3 state$_ne6$raw_nec _nc8 state$_nc8$raw_nee - - 0 =state$_ne6$raw_nec - - 1 =state$_ncb$raw_ne3 .mv state$_nbe$raw_nf2 4 STOPPED_init STOPPED GO_init GO .names state$_nc1$raw_nc7 state$_nc8$raw_nee _nbe state$_nbe$raw_nf2 - - 0 =state$_nc8$raw_nee - - 1 =state$_nc1$raw_nc7 .mv state$_na8$raw_nf6 4 STOPPED_init STOPPED GO_init GO .names state$_nab$raw_nba state$_nbe$raw_nf2 _na8 state$_na8$raw_nf6 - - 0 =state$_nbe$raw_nf2 - - 1 =state$_nab$raw_nba # conflict arbitrators .names status$raw_n94 status - =status$raw_n94 .names _na8 _nab _nb1 _nbe _nc3 _nc8 _ncd _ncf _nd5 _ne6 _nf9 .def 0 1 1 - - - - - - - - 1 1 0 1 - - - - - - - 1 0 - - 1 1 - - - - - 1 0 - - 0 - 1 1 - - - 1 0 - - 0 - 1 0 1 - - 1 0 - - 0 - 1 0 0 1 - 1 0 - - 0 - 0 - - - 1 1 .mv _nfa 4 STOPPED_init STOPPED GO_init GO .names _nf9 state$_na8$raw_nf6 state _nfa 1 - - =state$_na8$raw_nf6 0 - - =state # non-blocking assignments # latches .r state$raw_n93 state - =state$raw_n93 .latch _nfa state # quasi-continuous assignment .end .model collision # I/O ports .inputs status_B .inputs status_A .mv status_B 3 no_cars car_waiting cars_passing .mv status_A 3 no_cars car_waiting cars_passing .mv state 2 GOOD BAD # state = 0 .mv state$raw_n100 2 GOOD BAD .names state$raw_n100 GOOD # non-blocking assignments for initial .mv _n103 2 GOOD BAD .names _n103 GOOD .names state _n103 _n102 .def 0 - =state 1 .names _n102 _n101 1 1 0 0 .mv _n105 3 no_cars car_waiting cars_passing .names _n105 cars_passing # status_A == 2 .names status_A _n105 _n104 .def 0 - =status_A 1 .mv _n107 3 no_cars car_waiting cars_passing .names _n107 cars_passing # status_B == 2 .names status_B _n107 _n106 .def 0 - =status_B 1 # (status_A == 2) && (status_B == 2) .names _n104 _n106 _n108 .def 0 1 1 1 .names _n108 _n109 - =_n108 # state = 1 .mv state$_n108_n10a$true 2 GOOD BAD .names state$_n108_n10a$true BAD # if/else ((status_A == 2) && (status_B == 2)) .mv state$_n108$raw_n10d 2 GOOD BAD .names state$_n108_n10a$true state _n108 state$_n108$raw_n10d - - 0 =state - - 1 =state$_n108_n10a$true # case (state ) .mv state$_n101$raw_n110 2 GOOD BAD .names state$_n108$raw_n10d state _n101 state$_n101$raw_n110 - - 0 =state - - 1 =state$_n108$raw_n10d # conflict arbitrators .names _n101 _n109 _n111 .def 0 1 1 1 .mv _n112 2 GOOD BAD .names _n111 state$_n101$raw_n110 state _n112 1 - - =state$_n101$raw_n110 0 - - =state # non-blocking assignments # latches .r state$raw_n100 state - =state$raw_n100 .latch _n112 state # quasi-continuous assignment .end .model starvation # I/O ports .inputs stat .mv state 2 OK NOT_OK .mv stat 3 no_cars car_waiting cars_passing # state = 0 .mv state$raw_n114 2 OK NOT_OK .names state$raw_n114 OK # non-blocking assignments for initial .mv _n117 2 OK NOT_OK .names _n117 OK .names state _n117 _n116 .def 0 - =state 1 .names _n116 _n115 1 1 0 0 .mv _n119 3 no_cars car_waiting cars_passing .names _n119 car_waiting # stat == 1 .names stat _n119 _n118 .def 0 - =stat 1 .names _n118 _n11a - =_n118 # state = 1 .mv state$_n118_n11b$true 2 OK NOT_OK .names state$_n118_n11b$true NOT_OK # if/else (stat == 1) .mv state$_n118$raw_n11e 2 OK NOT_OK .names state$_n118_n11b$true state _n118 state$_n118$raw_n11e - - 0 =state - - 1 =state$_n118_n11b$true .mv _n121 2 OK NOT_OK .names _n121 NOT_OK .names state _n121 _n120 .def 0 - =state 1 .names _n120 _n11f 1 1 0 0 .mv _n123 3 no_cars car_waiting cars_passing .names _n123 cars_passing # stat == 2 .names stat _n123 _n122 .def 0 - =stat 1 .names _n122 _n124 - =_n122 # state = 0 .mv state$_n122_n125$true 2 OK NOT_OK .names state$_n122_n125$true OK # if/else (stat == 2) .mv state$_n122$raw_n128 2 OK NOT_OK .names state$_n122_n125$true state _n122 state$_n122$raw_n128 - - 0 =state - - 1 =state$_n122_n125$true # case (state ) .mv state$_n11f$raw_n12b 2 OK NOT_OK .names state$_n122$raw_n128 state _n11f state$_n11f$raw_n12b - - 0 =state - - 1 =state$_n122$raw_n128 .mv state$_n115$raw_n12d 2 OK NOT_OK .names state$_n118$raw_n11e state$_n11f$raw_n12b _n115 state$_n115$raw_n12d - - 0 =state$_n11f$raw_n12b - - 1 =state$_n118$raw_n11e # conflict arbitrators .names _n115 _n11a _n11f _n124 _n130 .def 0 1 1 - - 1 0 - 1 1 1 .mv _n131 2 OK NOT_OK .names _n130 state$_n115$raw_n12d state _n131 1 - - =state$_n115$raw_n12d 0 - - =state # non-blocking assignments # latches .r state$raw_n114 state - =state$raw_n114 .latch _n131 state # quasi-continuous assignment .end