# vl2mv ctlp3.v # version: 0.2 # date: 11:13:08 12/11/95 (PST) .model diners # I/O ports .mv s0 4 THINKING HUNGRY EATING READING .mv s1 4 THINKING HUNGRY EATING READING .mv s2 4 THINKING HUNGRY EATING READING .mv _n0 4 THINKING HUNGRY EATING READING .names _n0 EATING .subckt philosopher ph0 out=s0 left=s1 right=s2 init=_n0 .mv _n1 4 THINKING HUNGRY EATING READING .names _n1 READING .subckt philosopher ph1 out=s1 left=s2 right=s0 init=_n1 .mv _n2 4 THINKING HUNGRY EATING READING .names _n2 HUNGRY .subckt philosopher ph2 out=s2 left=s0 right=s1 init=_n2 .subckt starvation str starv=s0 # conflict arbitrators # non-blocking assignments # latches # quasi-continuous assignment .end .model philosopher # I/O ports .inputs left .outputs out .inputs init .inputs right .mv left 4 THINKING HUNGRY EATING READING .mv out 4 THINKING HUNGRY EATING READING .mv r0_state 4 THINKING HUNGRY EATING READING .mv r1_state 4 THINKING HUNGRY EATING READING .mv state 4 THINKING HUNGRY EATING READING .mv init 4 THINKING HUNGRY EATING READING .mv right 4 THINKING HUNGRY EATING READING # state = init .mv state$raw_n3 4 THINKING HUNGRY EATING READING .names init state$raw_n3 - =init # non-blocking assignments for initial # assign r0_state = $NDset ( 0,1 ) .names r0_state THINKING HUNGRY # assign r1_state = $NDset ( 0,2 ) .names r1_state THINKING EATING # assign out = state .mv out$raw_n8 4 THINKING HUNGRY EATING READING .names state out$raw_n8 - =state .mv _nb 4 THINKING HUNGRY EATING READING .names _nb READING .names state _nb _na .def 0 - =state 1 .names _na _n9 1 1 0 0 .mv _nd 4 THINKING HUNGRY EATING READING .names _nd THINKING # left == 0 .names left _nd _nc .def 0 - =left 1 .names _nc _ne - =_nc # state = 0 .mv state$_nc_nf$true 4 THINKING HUNGRY EATING READING .names state$_nc_nf$true THINKING # if/else (left == 0) .mv state$_nc$raw_n12 4 THINKING HUNGRY EATING READING .names state$_nc_nf$true state _nc state$_nc$raw_n12 - - 0 =state - - 1 =state$_nc_nf$true .mv _n15 4 THINKING HUNGRY EATING READING .names _n15 THINKING .names state _n15 _n14 .def 0 - =state 1 .names _n14 _n13 1 1 0 0 .mv _n17 4 THINKING HUNGRY EATING READING .names _n17 READING # right == 3 .names right _n17 _n16 .def 0 - =right 1 .names _n16 _n18 - =_n16 # state = 3 .mv state$_n16_n19$true 4 THINKING HUNGRY EATING READING .names state$_n16_n19$true READING # state = r0_state .mv state$_n16_n1a$false 4 THINKING HUNGRY EATING READING .names r0_state state$_n16_n1a$false - =r0_state # if/else (right == 3) .mv state$_n16$raw_n1c 4 THINKING HUNGRY EATING READING .names state$_n16_n19$true state$_n16_n1a$false _n16 state$_n16$raw_n1c - - 0 =state$_n16_n1a$false - - 1 =state$_n16_n19$true .mv _n21 4 THINKING HUNGRY EATING READING .names _n21 EATING .names state _n21 _n20 .def 0 - =state 1 .names _n20 _n1f 1 1 0 0 # state = r1_state .mv state$_n1f_n22$true 4 THINKING HUNGRY EATING READING .names r1_state state$_n1f_n22$true - =r1_state .mv _n25 4 THINKING HUNGRY EATING READING .names _n25 HUNGRY .names state _n25 _n24 .def 0 - =state 1 .names _n24 _n23 1 1 0 0 .mv _n27 4 THINKING HUNGRY EATING READING .names _n27 EATING # left != 2 .names left _n27 _n26 .def 1 - =left 0 .mv _n29 4 THINKING HUNGRY EATING READING .names _n29 HUNGRY # right != 1 .names right _n29 _n28 .def 1 - =right 0 # left != 2 && right != 1 .names _n26 _n28 _n2a .def 0 1 1 1 .mv _n2c 4 THINKING HUNGRY EATING READING .names _n2c EATING # right != 2 .names right _n2c _n2b .def 1 - =right 0 # left != 2 && right != 1 && right != 2 .names _n2a _n2b _n2d .def 0 1 1 1 .names _n2d _n2e - =_n2d # state = 2 .mv state$_n2d_n2f$true 4 THINKING HUNGRY EATING READING .names state$_n2d_n2f$true EATING # if/else (left != 2 && right != 1 && right != 2) .mv state$_n2d$raw_n32 4 THINKING HUNGRY EATING READING .names state$_n2d_n2f$true state _n2d state$_n2d$raw_n32 - - 0 =state - - 1 =state$_n2d_n2f$true # case (state ) .mv state$_n23$raw_n35 4 THINKING HUNGRY EATING READING .names state$_n2d$raw_n32 state _n23 state$_n23$raw_n35 - - 0 =state - - 1 =state$_n2d$raw_n32 .mv state$_n1f$raw_n36 4 THINKING HUNGRY EATING READING .names state$_n1f_n22$true state$_n23$raw_n35 _n1f state$_n1f$raw_n36 - - 0 =state$_n23$raw_n35 - - 1 =state$_n1f_n22$true .mv state$_n13$raw_n3a 4 THINKING HUNGRY EATING READING .names state$_n16$raw_n1c state$_n1f$raw_n36 _n13 state$_n13$raw_n3a - - 0 =state$_n1f$raw_n36 - - 1 =state$_n16$raw_n1c .mv state$_n9$raw_n3e 4 THINKING HUNGRY EATING READING .names state$_nc$raw_n12 state$_n13$raw_n3a _n9 state$_n9$raw_n3e - - 0 =state$_n13$raw_n3a - - 1 =state$_nc$raw_n12 # conflict arbitrators .names out$raw_n8 out - =out$raw_n8 .names _n9 _ne _n13 _n18 _n1f _n23 _n2e _n42 .def 0 1 1 - - - - - 1 0 - 1 1 - - - 1 0 - 1 0 - - - 1 0 - 0 - 1 - - 1 0 - 0 - 0 1 1 1 .mv _n43 4 THINKING HUNGRY EATING READING .names _n42 state$_n9$raw_n3e state _n43 1 - - =state$_n9$raw_n3e 0 - - =state # non-blocking assignments # latches .r state$raw_n3 state - =state$raw_n3 .latch _n43 state # quasi-continuous assignment .end .model starvation # I/O ports .inputs starv .mv starv 4 THINKING HUNGRY EATING READING # state = 0 .names state$raw_n49 0 # non-blocking assignments for initial .names _n4c 0 .names state _n4c _n4d .def 0 0 1 1 1 0 1 .names _n4d _n4b 0 1 1 0 .names _n4b _n4a 1 1 0 0 .mv _n50 4 THINKING HUNGRY EATING READING .names _n50 HUNGRY # starv == 1 .names starv _n50 _n4f .def 0 - =starv 1 .names _n4f _n51 - =_n4f # state = 1 .names state$_n4f_n52$true 1 # if/else (starv == 1) .names state$_n4f_n52$true state _n4f state$_n4f$raw_n55 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n59 1 .names state _n59 _n5a .def 0 0 1 1 1 0 1 .names _n5a _n58 0 1 1 0 .names _n58 _n57 1 1 0 0 .mv _n5d 4 THINKING HUNGRY EATING READING .names _n5d THINKING # starv == 0 .names starv _n5d _n5c .def 0 - =starv 1 .names _n5c _n5e - =_n5c # state = 0 .names state$_n5c_n5f$true 0 # if/else (starv == 0) .names state$_n5c_n5f$true state _n5c state$_n5c$raw_n62 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # case (state ) .names state$_n5c$raw_n62 state _n57 state$_n57$raw_n66 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names state$_n4f$raw_n55 state$_n57$raw_n66 _n4a state$_n4a$raw_n68 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # conflict arbitrators .names _n4a _n51 _n57 _n5e _n6d .def 0 1 1 - - 1 0 - 1 1 1 .names _n6d state$_n4a$raw_n68 state _n6e 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 # non-blocking assignments # latches .r state$raw_n49 state 0 0 1 1 .latch _n6e state # quasi-continuous assignment .end