source: cegar_dev/cegar/concrete_model/concret_main.mv @ 49

# vl2mv Concret_Main.v 
# version: 1.4
# date:    13:18:30 09/06/2010 (CEST)
.model main 
# I/O ports
.outputs o1
.outputs o2
.inputs i1
.outputs r_i1
.subckt machine_concret machine_concret1 i1=i1  o1=o1  o2=o2  r_i1=r_i1  
# conflict arbitrators
# non-blocking assignments 
# latches
# quasi-continuous assignment
.end


.model machine_concret 
# I/O ports
.outputs o1
.outputs o2
.inputs i1
.outputs r_i1
.mv m_state 4 S0 S1 S2 S3 
# m_state  = 0
.mv m_state$raw_n0 4 S0 S1 S2 S3 
.names m_state$raw_n0
S0
# o1  = 0
.names o1$raw_n1
0
# o2  = 0
.names o2$raw_n2
0
# r_i1  = i1 
.names i1 r_i1$raw_n3
- =i1
# non-blocking assignments for initial
# r_i1  = i1 
.names i1 r_i1$raw_n4
- =i1
.mv _n7 4 S0 S1 S2 S3 
.names _n7
S0
.names m_state _n7 _n6
.def 0
- =m_state 1
.names _n6  _n5
1 1
0 0
.names _n9
1
# i1  == 1
.names i1 _n9 _na
.def 0
0 1 1
1 0 1
.names _na _n8
0 1  
1 0  
.names _n8 _nc
- =_n8
# m_state  = 1
.mv m_state$_n8_nd$true 4 S0 S1 S2 S3 
.names m_state$_n8_nd$true
S1
# o1  = 1
.names o1$_n8_ne$true
1
# o2  = 0
.names o2$_n8_nf$true
0
# o1  = 0
.names o1$_n8_n10$false
0
# o2  = 0
.names o2$_n8_n11$false
0
# m_state  = 0
.mv m_state$_n8_n12$false 4 S0 S1 S2 S3 
.names m_state$_n8_n12$false
S0
# if/else (i1  == 1)
.names o1$_n8_ne$true o1$_n8_n10$false _n8 o1$_n8$raw_n17
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names o2$_n8_nf$true o2$_n8_n11$false _n8 o2$_n8$raw_n19
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.mv m_state$_n8$raw_n1b 4 S0 S1 S2 S3 
.names m_state$_n8_nd$true m_state$_n8_n12$false _n8 m_state$_n8$raw_n1b
- - 0 =m_state$_n8_n12$false
- - 1 =m_state$_n8_nd$true
.mv _n27 4 S0 S1 S2 S3 
.names _n27
S1
.names m_state _n27 _n26
.def 0
- =m_state 1
.names _n26  _n25
1 1
0 0
# m_state  = 2
.mv m_state$_n25_n28$true 4 S0 S1 S2 S3 
.names m_state$_n25_n28$true
S2
# o1  = 0
.names o1$_n25_n29$true
0
# o2  = 1
.names o2$_n25_n2a$true
1
.mv _n2d 4 S0 S1 S2 S3 
.names _n2d
S2
.names m_state _n2d _n2c
.def 0
- =m_state 1
.names _n2c  _n2b
1 1
0 0
# m_state  = 3
.mv m_state$_n2b_n2e$true 4 S0 S1 S2 S3 
.names m_state$_n2b_n2e$true
S3
# o1  = 1
.names o1$_n2b_n2f$true
1
# o2  = 1
.names o2$_n2b_n30$true
1
.mv _n33 4 S0 S1 S2 S3 
.names _n33
S3
.names m_state _n33 _n32
.def 0
- =m_state 1
.names _n32  _n31
1 1
0 0
# o1  = 1
.names o1$_n31_n34$true
1
# o2  = 1
.names o2$_n31_n35$true
1
# m_state  = 3
.mv m_state$_n31_n36$true 4 S0 S1 S2 S3 
.names m_state$_n31_n36$true
S3
# case (m_state )
.names o1$_n31_n34$true o1 _n31 o1$_n31$raw_n3f
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names o2$_n31_n35$true o2 _n31 o2$_n31$raw_n41
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.mv m_state$_n31$raw_n43 4 S0 S1 S2 S3 
.names m_state$_n31_n36$true m_state _n31 m_state$_n31$raw_n43
- - 0 =m_state
- - 1 =m_state$_n31_n36$true
.names o1$_n2b_n2f$true o1$_n31$raw_n3f _n2b o1$_n2b$raw_n46
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names o2$_n2b_n30$true o2$_n31$raw_n41 _n2b o2$_n2b$raw_n48
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.mv m_state$_n2b$raw_n4a 4 S0 S1 S2 S3 
.names m_state$_n2b_n2e$true m_state$_n31$raw_n43 _n2b m_state$_n2b$raw_n4a
- - 0 =m_state$_n31$raw_n43
- - 1 =m_state$_n2b_n2e$true
.names o1$_n25_n29$true o1$_n2b$raw_n46 _n25 o1$_n25$raw_n58
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names o2$_n25_n2a$true o2$_n2b$raw_n48 _n25 o2$_n25$raw_n5a
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.mv m_state$_n25$raw_n5c 4 S0 S1 S2 S3 
.names m_state$_n25_n28$true m_state$_n2b$raw_n4a _n25 m_state$_n25$raw_n5c
- - 0 =m_state$_n2b$raw_n4a
- - 1 =m_state$_n25_n28$true
.names o1$_n8$raw_n17 o1$_n25$raw_n58 _n5 o1$_n5$raw_n6a
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.names o2$_n8$raw_n19 o2$_n25$raw_n5a _n5 o2$_n5$raw_n6c
0 - 1 0
1 - 1 1
- 0 0 0
- 1 0 1
.mv m_state$_n5$raw_n6e 4 S0 S1 S2 S3 
.names m_state$_n8$raw_n1b m_state$_n25$raw_n5c _n5 m_state$_n5$raw_n6e
- - 0 =m_state$_n25$raw_n5c
- - 1 =m_state$_n8$raw_n1b
# conflict arbitrators
.names _n5 _nc _n25 _n2b _n31 _n7c
.def 0
 1 1 - - - 1
 1 0 - - - 1
 0 - 1 - - 1
 0 - 0 1 - 1
 0 - 0 0 1 1
.names _n7c o1$_n5$raw_n6a o1 _n7d 
1 0 - 0
1 1 - 1
0 - 0 0
0 - 1 1
.names _n5 _nc _n25 _n2b _n31 _n7e
.def 0
 1 1 - - - 1
 1 0 - - - 1
 0 - 1 - - 1
 0 - 0 1 - 1
 0 - 0 0 1 1
.names _n7e o2$_n5$raw_n6c o2 _n7f 
1 0 - 0
1 1 - 1
0 - 0 0
0 - 1 1
.names _n5 _nc _n25 _n2b _n31 _n80
.def 0
 1 1 - - - 1
 1 0 - - - 1
 0 - 1 - - 1
 0 - 0 1 - 1
 0 - 0 0 1 1
.mv _n81 4 S0 S1 S2 S3 
.names _n80 m_state$_n5$raw_n6e m_state _n81 
1 - - =m_state$_n5$raw_n6e
0 - - =m_state
.names _n82
.def 0
 1
.names _n82 r_i1$raw_n4 _n83 
.def 0
1 0 0
1 1 1
# non-blocking assignments 
# latches
.r o1$raw_n1 o1
0 0
1 1
.latch _n7d o1
.r o2$raw_n2 o2
0 0
1 1
.latch _n7f o2
.r m_state$raw_n0 m_state
- =m_state$raw_n0
.latch _n81 m_state
.r r_i1$raw_n3 r_i1
0 0
1 1
.latch _n83 r_i1
# quasi-continuous assignment
.end