source: vis_dev/vis-2.1/examples/crd/crd.mv @ 14

# 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