# vl2mv coherence.v # version: 0.2 # date: 10:43:41 05/16/96 (PDT) .model COHERANCE # I/O ports .inputs any_value2 .inputs any_address2<0> .inputs any_value1 .inputs any_address1<0> .inputs inst2 .inputs inst1 .mv cache_req2 4 ok blk_rreq blk_excl noop .mv cache_req1 4 ok blk_rreq blk_excl noop .mv inst2 3 COMPUTE READ_WORD WRITE_WORD .mv inst1 3 COMPUTE READ_WORD WRITE_WORD .subckt PROC proc1 read_req=read_req1 write_req=write_req1 data=data1 address<0>=address1<0> acknowledge=acknowledge1 any_address<0>=any_address1<0> any_value=any_value1 inst=inst1 .subckt CACHE_CTRLER cc1 read_req=read_req1 write_req=write_req1 data=data1 address<0>=address1<0> acknowledge=acknowledge1 write_back_req=write_back_req1 inval=inval1 blocknum<0>=blocknum<0> blk_ok=blk_ok1 blk_data=blk_data back_data=back_data1 cache_req=cache_req1 blk_add<0>=blk_add1<0> .subckt PROC proc2 read_req=read_req2 write_req=write_req2 data=data2 address<0>=address2<0> acknowledge=acknowledge2 any_address<0>=any_address2<0> any_value=any_value2 inst=inst2 .subckt CACHE_CTRLER cc2 read_req=read_req2 write_req=write_req2 data=data2 address<0>=address2<0> acknowledge=acknowledge2 write_back_req=write_back_req2 inval=inval2 blocknum<0>=blocknum<0> blk_ok=blk_ok2 blk_data=blk_data back_data=back_data2 cache_req=cache_req2 blk_add<0>=blk_add2<0> .subckt DIRECTORY direc write_back_req1=write_back_req1 inval1=inval1 write_back_req2=write_back_req2 inval2=inval2 blocknum<0>=blocknum<0> blk_ok1=blk_ok1 blk_data=blk_data blk_ok2=blk_ok2 back_data1=back_data1 cache_req1=cache_req1 blk_add1<0>=blk_add1<0> back_data2=back_data2 cache_req2=cache_req2 blk_add2<0>=blk_add2<0> # conflict arbitrators # non-blocking assignments # latches # quasi-continuous assignment .end .model PROC # I/O ports .inputs inst .inputs any_value .outputs write_req .outputs read_req .inputs any_address<0> .outputs address<0> .outputs data .inputs acknowledge .mv proc_state 3 IDLE READING WRITING .mv inst 3 COMPUTE READ_WORD WRITE_WORD # proc_state = 0 .mv proc_state$raw_n0 3 IDLE READING WRITING .names proc_state$raw_n0 IDLE # non-blocking assignments for initial # assign read_req = ((proc_state == IDLE ) ? ((inst == READ_WORD ) ? 1 : 0) : ((proc_state == READING ) ? 1 : 0)) .mv _n3 3 IDLE READING WRITING .names _n3 IDLE # proc_state == 0 .names proc_state _n3 _n2 .def 0 - =proc_state 1 .mv _n5 3 COMPUTE READ_WORD WRITE_WORD .names _n5 READ_WORD # inst == 1 .names inst _n5 _n4 .def 0 - =inst 1 .names _n6 1 .names _n7 0 # (inst == 1) ? 1 : 0 .names _n6 _n7 _n4 _n8 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _nb 3 IDLE READING WRITING .names _nb READING # proc_state == 1 .names proc_state _nb _na .def 0 - =proc_state 1 .names _nc 1 .names _nd 0 # (proc_state == 1) ? 1 : 0 .names _nc _nd _na _ne 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # (proc_state == 0) ? ((inst == 1) ? 1 : 0) : ((proc_state == 1) ? 1 : 0) .names _n8 _ne _n2 _n10 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n10 read_req$raw_n1 - =_n10 # assign write_req = ((proc_state == IDLE ) ? ((inst == WRITE_WORD ) ? 1 : 0) : ((proc_state == WRITING ) ? 1 : 0)) .mv _n14 3 IDLE READING WRITING .names _n14 IDLE # proc_state == 0 .names proc_state _n14 _n13 .def 0 - =proc_state 1 .mv _n16 3 COMPUTE READ_WORD WRITE_WORD .names _n16 WRITE_WORD # inst == 2 .names inst _n16 _n15 .def 0 - =inst 1 .names _n17 1 .names _n18 0 # (inst == 2) ? 1 : 0 .names _n17 _n18 _n15 _n19 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n1c 3 IDLE READING WRITING .names _n1c WRITING # proc_state == 2 .names proc_state _n1c _n1b .def 0 - =proc_state 1 .names _n1d 1 .names _n1e 0 # (proc_state == 2) ? 1 : 0 .names _n1d _n1e _n1b _n1f 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # (proc_state == 0) ? ((inst == 2) ? 1 : 0) : ((proc_state == 2) ? 1 : 0) .names _n19 _n1f _n13 _n21 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n21 write_req$raw_n12 - =_n21 # assign data = any_value .names any_value data$raw_n23 - =any_value # assign address = any_address .names any_address<0> address$raw_n24<0> - =any_address<0> .mv _n27 3 IDLE READING WRITING .names _n27 IDLE .names proc_state _n27 _n26 .def 0 - =proc_state 1 .names _n26 _n25 1 1 0 0 .mv _n2a 3 COMPUTE READ_WORD WRITE_WORD .names _n2a COMPUTE .names inst _n2a _n29 .def 0 - =inst 1 .names _n29 _n28 1 1 0 0 # proc_state = 0 .mv proc_state$_n28_n2b$true 3 IDLE READING WRITING .names proc_state$_n28_n2b$true IDLE .mv _n2e 3 COMPUTE READ_WORD WRITE_WORD .names _n2e READ_WORD .names inst _n2e _n2d .def 0 - =inst 1 .names _n2d _n2c 1 1 0 0 # proc_state = 1 .mv proc_state$_n2c_n2f$true 3 IDLE READING WRITING .names proc_state$_n2c_n2f$true READING .mv _n32 3 COMPUTE READ_WORD WRITE_WORD .names _n32 WRITE_WORD .names inst _n32 _n31 .def 0 - =inst 1 .names _n31 _n30 1 1 0 0 # proc_state = 2 .mv proc_state$_n30_n33$true 3 IDLE READING WRITING .names proc_state$_n30_n33$true WRITING # proc_state = 0 .mv proc_state$raw_n34 3 IDLE READING WRITING .names proc_state$raw_n34 IDLE # case (inst ) .mv proc_state$_n30$raw_n36 3 IDLE READING WRITING .names proc_state$_n30_n33$true proc_state$raw_n34 _n30 proc_state$_n30$raw_n36 - - 0 =proc_state$raw_n34 - - 1 =proc_state$_n30_n33$true .mv proc_state$_n2c$raw_n3a 3 IDLE READING WRITING .names proc_state$_n2c_n2f$true proc_state$_n30$raw_n36 _n2c proc_state$_n2c$raw_n3a - - 0 =proc_state$_n30$raw_n36 - - 1 =proc_state$_n2c_n2f$true .mv proc_state$_n28$raw_n3e 3 IDLE READING WRITING .names proc_state$_n28_n2b$true proc_state$_n2c$raw_n3a _n28 proc_state$_n28$raw_n3e - - 0 =proc_state$_n2c$raw_n3a - - 1 =proc_state$_n28_n2b$true .mv _n43 3 IDLE READING WRITING .names _n43 READING .names proc_state _n43 _n42 .def 0 - =proc_state 1 .names _n42 _n41 1 1 0 0 .names acknowledge _n44 - =acknowledge # proc_state = 0 .mv proc_state$acknowledge_n45$true 3 IDLE READING WRITING .names proc_state$acknowledge_n45$true IDLE # if/else (acknowledge ) .mv proc_state$acknowledge$raw_n48 3 IDLE READING WRITING .names proc_state$acknowledge_n45$true proc_state acknowledge proc_state$acknowledge$raw_n48 - - 0 =proc_state - - 1 =proc_state$acknowledge_n45$true .mv _n4b 3 IDLE READING WRITING .names _n4b WRITING .names proc_state _n4b _n4a .def 0 - =proc_state 1 .names _n4a _n49 1 1 0 0 .names acknowledge _n4c - =acknowledge # proc_state = 0 .mv proc_state$acknowledge_n4d$true 3 IDLE READING WRITING .names proc_state$acknowledge_n4d$true IDLE # if/else (acknowledge ) .mv proc_state$acknowledge$raw_n50 3 IDLE READING WRITING .names proc_state$acknowledge_n4d$true proc_state acknowledge proc_state$acknowledge$raw_n50 - - 0 =proc_state - - 1 =proc_state$acknowledge_n4d$true # case (proc_state ) .mv proc_state$_n49$raw_n53 3 IDLE READING WRITING .names proc_state$acknowledge$raw_n50 proc_state _n49 proc_state$_n49$raw_n53 - - 0 =proc_state - - 1 =proc_state$acknowledge$raw_n50 .mv proc_state$_n41$raw_n54 3 IDLE READING WRITING .names proc_state$acknowledge$raw_n48 proc_state$_n49$raw_n53 _n41 proc_state$_n41$raw_n54 - - 0 =proc_state$_n49$raw_n53 - - 1 =proc_state$acknowledge$raw_n48 .mv proc_state$_n25$raw_n58 3 IDLE READING WRITING .names proc_state$_n28$raw_n3e proc_state$_n41$raw_n54 _n25 proc_state$_n25$raw_n58 - - 0 =proc_state$_n41$raw_n54 - - 1 =proc_state$_n28$raw_n3e # conflict arbitrators .names _n25 _n28 _n2c _n30 _n41 _n44 _n49 _n4c _n5c .def 0 1 1 - - - - - - 1 1 0 1 - - - - - 1 1 0 0 1 - - - - 1 1 0 0 0 - - - - 1 0 - - - 1 1 - - 1 0 - - - 0 - 1 1 1 .mv _n5d 3 IDLE READING WRITING .names _n5c proc_state$_n25$raw_n58 proc_state _n5d 1 - - =proc_state$_n25$raw_n58 0 - - =proc_state .names write_req$raw_n12 write_req 0 0 1 1 .names read_req$raw_n1 read_req 0 0 1 1 .names address$raw_n24<0> address<0> - =address$raw_n24<0> .names data$raw_n23 data 0 0 1 1 # non-blocking assignments # latches .r proc_state$raw_n0 proc_state - =proc_state$raw_n0 .latch _n5d proc_state # quasi-continuous assignment .end .model CACHE_CTRLER # I/O ports .outputs back_data .inputs write_req .outputs blk_add<0> .inputs inval .inputs blk_data .inputs read_req .inputs address<0> .inputs data .inputs blk_ok .inputs blocknum<0> .outputs cache_req .inputs write_back_req .outputs acknowledge .mv block_state 3 INVALID SHARED EXCLUSIVE .mv cache_state 5 Ready Rwait Wwait Rgrant Wgrant .mv cache_req 4 ok blk_rreq blk_excl noop # cache_state = 0 .mv cache_state$raw_n65 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$raw_n65 Ready # block_state = 0 .mv block_state$raw_n66 3 INVALID SHARED EXCLUSIVE .names block_state$raw_n66 INVALID # block_add = 0 .names block_add$raw_n67<0> 0 # block_val = 0 .names block_val$raw_n68 0 # blk_add = 0 .names blk_add$raw_n69<0> 0 # cache_req = 3 .mv cache_req$raw_n6a 4 ok blk_rreq blk_excl noop .names cache_req$raw_n6a noop # non-blocking assignments for initial # assign back_data = (cache_req == ok ) ? block_val : 0 .mv _n6d 4 ok blk_rreq blk_excl noop .names _n6d ok # cache_req == 0 .names cache_req _n6d _n6c .def 0 - =cache_req 1 .names _n6e 0 # (cache_req == 0) ? block_val : 0 .names block_val _n6e _n6c _n6f 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n6f back_data$raw_n6b - =_n6f # assign acknowledge = ((cache_state == Rgrant ) || (cache_state == Wgrant )) ? 1 : 0 .mv _n73 5 Ready Rwait Wwait Rgrant Wgrant .names _n73 Rgrant # cache_state == 3 .names cache_state _n73 _n72 .def 0 - =cache_state 1 .mv _n75 5 Ready Rwait Wwait Rgrant Wgrant .names _n75 Wgrant # cache_state == 4 .names cache_state _n75 _n74 .def 0 - =cache_state 1 # (cache_state == 3) || (cache_state == 4) .names _n72 _n74 _n76 .def 1 0 0 0 .names _n77 1 .names _n78 0 # ((cache_state == 3) || (cache_state == 4)) ? 1 : 0 .names _n77 _n78 _n76 _n79 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n79 acknowledge$raw_n71 - =_n79 .mv _n7d 5 Ready Rwait Wwait Rgrant Wgrant .names _n7d Ready .names cache_state _n7d _n7c .def 0 - =cache_state 1 .names _n7c _n7b 1 1 0 0 # block_add == blocknum .names block_add<0> blocknum<0> _n7f<0> .def 0 0 1 1 1 0 1 .names _n7f<0> _n80 .def 1 0 0 .names _n80 _n7e 0 1 1 0 # (inval ) && (block_add == blocknum ) .names inval _n7e _n81 .def 0 1 1 1 .names _n81 _n82 - =_n81 # block_state = 0 .mv block_state$_n81_n83$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n81_n83$true INVALID # cache_req = 0 .mv cache_req$_n81_n84$true 4 ok blk_rreq blk_excl noop .names cache_req$_n81_n84$true ok # cache_state = 0 .mv cache_state$_n81_n85$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n81_n85$true Ready .names write_back_req _n86 - =write_back_req # block_state = 1 .mv block_state$write_back_req_n87$true 3 INVALID SHARED EXCLUSIVE .names block_state$write_back_req_n87$true SHARED # cache_req = 0 .mv cache_req$write_back_req_n88$true 4 ok blk_rreq blk_excl noop .names cache_req$write_back_req_n88$true ok # cache_state = 0 .mv cache_state$write_back_req_n89$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n89$true Ready .names read_req _n8a - =read_req # block_add != address .names block_add<0> address<0> _n8c<0> .def 0 0 1 1 1 0 1 .names _n8c<0> _n8d .def 1 0 0 .names _n8d _n8b - =_n8d .mv _n8f 3 INVALID SHARED EXCLUSIVE .names _n8f INVALID # block_state == 0 .names block_state _n8f _n8e .def 0 - =block_state 1 # (block_add != address ) || (block_state == 0) .names _n8b _n8e _n90 .def 1 0 0 0 .names _n90 _n91 - =_n90 # cache_req = 1 .mv cache_req$_n90_n92$true 4 ok blk_rreq blk_excl noop .names cache_req$_n90_n92$true blk_rreq # blk_add = address .names address<0> blk_add$_n90_n93$true<0> - =address<0> # cache_state = 1 .mv cache_state$_n90_n94$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n90_n94$true Rwait # block_state = 0 .mv block_state$_n90_n95$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n90_n95$true INVALID # cache_state = 3 .mv cache_state$_n90_n96$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n90_n96$false Rgrant # cache_req = 3 .mv cache_req$_n90_n97$false 4 ok blk_rreq blk_excl noop .names cache_req$_n90_n97$false noop # if/else ((block_add != address ) || (block_state == 0)) .mv cache_state$_n90$raw_n9e 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n90_n94$true cache_state$_n90_n96$false _n90 cache_state$_n90$raw_n9e - - 0 =cache_state$_n90_n96$false - - 1 =cache_state$_n90_n94$true .mv cache_req$_n90$raw_n9f 4 ok blk_rreq blk_excl noop .names cache_req$_n90_n92$true cache_req$_n90_n97$false _n90 cache_req$_n90$raw_n9f - - 0 =cache_req$_n90_n97$false - - 1 =cache_req$_n90_n92$true .names blk_add$_n90_n93$true<0> blk_add<0> _n90 blk_add$_n90$raw_na0<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$_n90$raw_na2 3 INVALID SHARED EXCLUSIVE .names block_state$_n90_n95$true block_state _n90 block_state$_n90$raw_na2 - - 0 =block_state - - 1 =block_state$_n90_n95$true .names write_req _na7 - =write_req # block_add != address .names block_add<0> address<0> _na9<0> .def 0 0 1 1 1 0 1 .names _na9<0> _naa .def 1 0 0 .names _naa _na8 - =_naa .mv _nac 3 INVALID SHARED EXCLUSIVE .names _nac EXCLUSIVE # block_state != 2 .names block_state _nac _nab .def 1 - =block_state 0 # (block_add != address ) || (block_state != 2) .names _na8 _nab _nad .def 1 0 0 0 .names _nad _nae - =_nad # cache_req = 2 .mv cache_req$_nad_naf$true 4 ok blk_rreq blk_excl noop .names cache_req$_nad_naf$true blk_excl # blk_add = address .names address<0> blk_add$_nad_nb0$true<0> - =address<0> # cache_state = 2 .mv cache_state$_nad_nb1$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_nad_nb1$true Wwait # block_state = 0 .mv block_state$_nad_nb2$true 3 INVALID SHARED EXCLUSIVE .names block_state$_nad_nb2$true INVALID # cache_state = 4 .mv cache_state$_nad_nb3$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_nad_nb3$false Wgrant # cache_req = 3 .mv cache_req$_nad_nb4$false 4 ok blk_rreq blk_excl noop .names cache_req$_nad_nb4$false noop # if/else ((block_add != address ) || (block_state != 2)) .mv cache_state$_nad$raw_nbb 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_nad_nb1$true cache_state$_nad_nb3$false _nad cache_state$_nad$raw_nbb - - 0 =cache_state$_nad_nb3$false - - 1 =cache_state$_nad_nb1$true .mv cache_req$_nad$raw_nbc 4 ok blk_rreq blk_excl noop .names cache_req$_nad_naf$true cache_req$_nad_nb4$false _nad cache_req$_nad$raw_nbc - - 0 =cache_req$_nad_nb4$false - - 1 =cache_req$_nad_naf$true .names blk_add$_nad_nb0$true<0> blk_add<0> _nad blk_add$_nad$raw_nbd<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$_nad$raw_nbf 3 INVALID SHARED EXCLUSIVE .names block_state$_nad_nb2$true block_state _nad block_state$_nad$raw_nbf - - 0 =block_state - - 1 =block_state$_nad_nb2$true # cache_req = 3 .mv cache_req$write_req_nc4$false 4 ok blk_rreq blk_excl noop .names cache_req$write_req_nc4$false noop # blk_add = 0 .names blk_add$write_req_nc5$false<0> 0 # if/else (write_req ) .names blk_add$_nad$raw_nbd<0> blk_add$write_req_nc5$false<0> write_req blk_add$write_req$raw_nca<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$write_req$raw_nce 4 ok blk_rreq blk_excl noop .names cache_req$_nad$raw_nbc cache_req$write_req_nc4$false write_req cache_req$write_req$raw_nce - - 0 =cache_req$write_req_nc4$false - - 1 =cache_req$_nad$raw_nbc .mv block_state$write_req$raw_nd0 3 INVALID SHARED EXCLUSIVE .names block_state$_nad$raw_nbf block_state write_req block_state$write_req$raw_nd0 - - 0 =block_state - - 1 =block_state$_nad$raw_nbf .mv cache_state$write_req$raw_nd1 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_nad$raw_nbb cache_state write_req cache_state$write_req$raw_nd1 - - 0 =cache_state - - 1 =cache_state$_nad$raw_nbb # if/else (read_req ) .names blk_add$_n90$raw_na0<0> blk_add$write_req$raw_nca<0> read_req blk_add$read_req$raw_nd9<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$read_req$raw_ndb 3 INVALID SHARED EXCLUSIVE .names block_state$_n90$raw_na2 block_state$write_req$raw_nd0 read_req block_state$read_req$raw_ndb - - 0 =block_state$write_req$raw_nd0 - - 1 =block_state$_n90$raw_na2 .mv cache_state$read_req$raw_ndc 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n90$raw_n9e cache_state$write_req$raw_nd1 read_req cache_state$read_req$raw_ndc - - 0 =cache_state$write_req$raw_nd1 - - 1 =cache_state$_n90$raw_n9e .mv cache_req$read_req$raw_ndd 4 ok blk_rreq blk_excl noop .names cache_req$_n90$raw_n9f cache_req$write_req$raw_nce read_req cache_req$read_req$raw_ndd - - 0 =cache_req$write_req$raw_nce - - 1 =cache_req$_n90$raw_n9f # if/else (write_back_req ) .mv block_state$write_back_req$raw_ne9 3 INVALID SHARED EXCLUSIVE .names block_state$write_back_req_n87$true block_state$read_req$raw_ndb write_back_req block_state$write_back_req$raw_ne9 - - 0 =block_state$read_req$raw_ndb - - 1 =block_state$write_back_req_n87$true .mv cache_state$write_back_req$raw_nea 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n89$true cache_state$read_req$raw_ndc write_back_req cache_state$write_back_req$raw_nea - - 0 =cache_state$read_req$raw_ndc - - 1 =cache_state$write_back_req_n89$true .mv cache_req$write_back_req$raw_neb 4 ok blk_rreq blk_excl noop .names cache_req$write_back_req_n88$true cache_req$read_req$raw_ndd write_back_req cache_req$write_back_req$raw_neb - - 0 =cache_req$read_req$raw_ndd - - 1 =cache_req$write_back_req_n88$true .names blk_add<0> blk_add$read_req$raw_nd9<0> write_back_req blk_add$write_back_req$raw_nef<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # if/else ((inval ) && (block_add == blocknum )) .mv block_state$_n81$raw_nf7 3 INVALID SHARED EXCLUSIVE .names block_state$_n81_n83$true block_state$write_back_req$raw_ne9 _n81 block_state$_n81$raw_nf7 - - 0 =block_state$write_back_req$raw_ne9 - - 1 =block_state$_n81_n83$true .mv cache_state$_n81$raw_nf8 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n81_n85$true cache_state$write_back_req$raw_nea _n81 cache_state$_n81$raw_nf8 - - 0 =cache_state$write_back_req$raw_nea - - 1 =cache_state$_n81_n85$true .mv cache_req$_n81$raw_nf9 4 ok blk_rreq blk_excl noop .names cache_req$_n81_n84$true cache_req$write_back_req$raw_neb _n81 cache_req$_n81$raw_nf9 - - 0 =cache_req$write_back_req$raw_neb - - 1 =cache_req$_n81_n84$true .names blk_add<0> blk_add$write_back_req$raw_nef<0> _n81 blk_add$_n81$raw_nfd<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n104 5 Ready Rwait Wwait Rgrant Wgrant .names _n104 Rgrant .names cache_state _n104 _n103 .def 0 - =cache_state 1 .names _n103 _n102 1 1 0 0 # block_add == blocknum .names block_add<0> blocknum<0> _n106<0> .def 0 0 1 1 1 0 1 .names _n106<0> _n107 .def 1 0 0 .names _n107 _n105 0 1 1 0 # (inval ) && (block_add == blocknum ) .names inval _n105 _n108 .def 0 1 1 1 .names _n108 _n109 - =_n108 # block_state = 0 .mv block_state$_n108_n10a$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n108_n10a$true INVALID # cache_req = 0 .mv cache_req$_n108_n10b$true 4 ok blk_rreq blk_excl noop .names cache_req$_n108_n10b$true ok # cache_state = 0 .mv cache_state$_n108_n10c$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n108_n10c$true Ready # cache_state = 0 .mv cache_state$_n108_n10d$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n108_n10d$false Ready # if/else ((inval ) && (block_add == blocknum )) .mv cache_state$_n108$raw_n112 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n108_n10c$true cache_state$_n108_n10d$false _n108 cache_state$_n108$raw_n112 - - 0 =cache_state$_n108_n10d$false - - 1 =cache_state$_n108_n10c$true .mv block_state$_n108$raw_n114 3 INVALID SHARED EXCLUSIVE .names block_state$_n108_n10a$true block_state _n108 block_state$_n108$raw_n114 - - 0 =block_state - - 1 =block_state$_n108_n10a$true .mv cache_req$_n108$raw_n116 4 ok blk_rreq blk_excl noop .names cache_req$_n108_n10b$true cache_req _n108 cache_req$_n108$raw_n116 - - 0 =cache_req - - 1 =cache_req$_n108_n10b$true .mv _n11a 5 Ready Rwait Wwait Rgrant Wgrant .names _n11a Wgrant .names cache_state _n11a _n119 .def 0 - =cache_state 1 .names _n119 _n118 1 1 0 0 # block_add == blocknum .names block_add<0> blocknum<0> _n11c<0> .def 0 0 1 1 1 0 1 .names _n11c<0> _n11d .def 1 0 0 .names _n11d _n11b 0 1 1 0 # (inval ) && (block_add == blocknum ) .names inval _n11b _n11e .def 0 1 1 1 .names _n11e _n11f - =_n11e # block_state = 0 .mv block_state$_n11e_n120$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n11e_n120$true INVALID # cache_req = 0 .mv cache_req$_n11e_n121$true 4 ok blk_rreq blk_excl noop .names cache_req$_n11e_n121$true ok # cache_state = 0 .mv cache_state$_n11e_n122$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n11e_n122$true Ready # block_val = data .names data block_val$_n11e_n123$false - =data # cache_state = 0 .mv cache_state$_n11e_n124$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n11e_n124$false Ready # if/else ((inval ) && (block_add == blocknum )) .mv cache_state$_n11e$raw_n129 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n11e_n122$true cache_state$_n11e_n124$false _n11e cache_state$_n11e$raw_n129 - - 0 =cache_state$_n11e_n124$false - - 1 =cache_state$_n11e_n122$true .mv block_state$_n11e$raw_n12b 3 INVALID SHARED EXCLUSIVE .names block_state$_n11e_n120$true block_state _n11e block_state$_n11e$raw_n12b - - 0 =block_state - - 1 =block_state$_n11e_n120$true .mv cache_req$_n11e$raw_n12d 4 ok blk_rreq blk_excl noop .names cache_req$_n11e_n121$true cache_req _n11e cache_req$_n11e$raw_n12d - - 0 =cache_req - - 1 =cache_req$_n11e_n121$true .names block_val block_val$_n11e_n123$false _n11e block_val$_n11e$raw_n12f 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n133 5 Ready Rwait Wwait Rgrant Wgrant .names _n133 Rwait .names cache_state _n133 _n132 .def 0 - =cache_state 1 .names _n132 _n131 1 1 0 0 # block_add == blocknum .names block_add<0> blocknum<0> _n135<0> .def 0 0 1 1 1 0 1 .names _n135<0> _n136 .def 1 0 0 .names _n136 _n134 0 1 1 0 # (inval ) && (block_add == blocknum ) .names inval _n134 _n137 .def 0 1 1 1 .names _n137 _n138 - =_n137 # block_state = 0 .mv block_state$_n137_n139$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n137_n139$true INVALID # cache_req = 0 .mv cache_req$_n137_n13a$true 4 ok blk_rreq blk_excl noop .names cache_req$_n137_n13a$true ok # cache_state = 0 .mv cache_state$_n137_n13b$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n137_n13b$true Ready .names write_back_req _n13c - =write_back_req # cache_state = 0 .mv cache_state$write_back_req_n13d$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n13d$true Ready .names blk_ok _n13e - =blk_ok # block_val = blk_data .names blk_data block_val$blk_ok_n13f$true - =blk_data # block_add = blk_add .names blk_add<0> block_add$blk_ok_n140$true<0> - =blk_add<0> # block_state = 1 .mv block_state$blk_ok_n141$true 3 INVALID SHARED EXCLUSIVE .names block_state$blk_ok_n141$true SHARED # cache_req = 3 .mv cache_req$blk_ok_n142$true 4 ok blk_rreq blk_excl noop .names cache_req$blk_ok_n142$true noop # cache_state = 3 .mv cache_state$blk_ok_n143$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n143$true Rgrant # cache_state = 1 .mv cache_state$blk_ok_n144$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n144$false Rwait # if/else (blk_ok ) .mv cache_state$blk_ok$raw_n14c 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n143$true cache_state$blk_ok_n144$false blk_ok cache_state$blk_ok$raw_n14c - - 0 =cache_state$blk_ok_n144$false - - 1 =cache_state$blk_ok_n143$true .mv block_state$blk_ok$raw_n14f 3 INVALID SHARED EXCLUSIVE .names block_state$blk_ok_n141$true block_state blk_ok block_state$blk_ok$raw_n14f - - 0 =block_state - - 1 =block_state$blk_ok_n141$true .names block_add$blk_ok_n140$true<0> block_add<0> blk_ok block_add$blk_ok$raw_n150<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$blk_ok$raw_n153 4 ok blk_rreq blk_excl noop .names cache_req$blk_ok_n142$true cache_req blk_ok cache_req$blk_ok$raw_n153 - - 0 =cache_req - - 1 =cache_req$blk_ok_n142$true .names block_val$blk_ok_n13f$true block_val blk_ok block_val$blk_ok$raw_n154 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # if/else (write_back_req ) .mv cache_state$write_back_req$raw_n158 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n13d$true cache_state$blk_ok$raw_n14c write_back_req cache_state$write_back_req$raw_n158 - - 0 =cache_state$blk_ok$raw_n14c - - 1 =cache_state$write_back_req_n13d$true .mv block_state$write_back_req$raw_n15a 3 INVALID SHARED EXCLUSIVE .names block_state block_state$blk_ok$raw_n14f write_back_req block_state$write_back_req$raw_n15a - - 0 =block_state$blk_ok$raw_n14f - - 1 =block_state .names block_add<0> block_add$blk_ok$raw_n150<0> write_back_req block_add$write_back_req$raw_n15b<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$blk_ok$raw_n154 write_back_req block_val$write_back_req$raw_n15e 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$write_back_req$raw_n160 4 ok blk_rreq blk_excl noop .names cache_req cache_req$blk_ok$raw_n153 write_back_req cache_req$write_back_req$raw_n160 - - 0 =cache_req$blk_ok$raw_n153 - - 1 =cache_req # if/else ((inval ) && (block_add == blocknum )) .mv block_state$_n137$raw_n164 3 INVALID SHARED EXCLUSIVE .names block_state$_n137_n139$true block_state$write_back_req$raw_n15a _n137 block_state$_n137$raw_n164 - - 0 =block_state$write_back_req$raw_n15a - - 1 =block_state$_n137_n139$true .mv cache_state$_n137$raw_n165 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n137_n13b$true cache_state$write_back_req$raw_n158 _n137 cache_state$_n137$raw_n165 - - 0 =cache_state$write_back_req$raw_n158 - - 1 =cache_state$_n137_n13b$true .mv cache_req$_n137$raw_n166 4 ok blk_rreq blk_excl noop .names cache_req$_n137_n13a$true cache_req$write_back_req$raw_n160 _n137 cache_req$_n137$raw_n166 - - 0 =cache_req$write_back_req$raw_n160 - - 1 =cache_req$_n137_n13a$true .names block_add<0> block_add$write_back_req$raw_n15b<0> _n137 block_add$_n137$raw_n16b<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$write_back_req$raw_n15e _n137 block_val$_n137$raw_n16f 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n173 5 Ready Rwait Wwait Rgrant Wgrant .names _n173 Wwait .names cache_state _n173 _n172 .def 0 - =cache_state 1 .names _n172 _n171 1 1 0 0 # block_add == blocknum .names block_add<0> blocknum<0> _n175<0> .def 0 0 1 1 1 0 1 .names _n175<0> _n176 .def 1 0 0 .names _n176 _n174 0 1 1 0 # (inval ) && (block_add == blocknum ) .names inval _n174 _n177 .def 0 1 1 1 .names _n177 _n178 - =_n177 # block_state = 0 .mv block_state$_n177_n179$true 3 INVALID SHARED EXCLUSIVE .names block_state$_n177_n179$true INVALID # cache_req = 0 .mv cache_req$_n177_n17a$true 4 ok blk_rreq blk_excl noop .names cache_req$_n177_n17a$true ok # cache_state = 0 .mv cache_state$_n177_n17b$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n177_n17b$true Ready .names write_back_req _n17c - =write_back_req # cache_state = 0 .mv cache_state$write_back_req_n17d$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n17d$true Ready .names blk_ok _n17e - =blk_ok # block_val = blk_data .names blk_data block_val$blk_ok_n17f$true - =blk_data # block_add = blk_add .names blk_add<0> block_add$blk_ok_n180$true<0> - =blk_add<0> # block_state = 2 .mv block_state$blk_ok_n181$true 3 INVALID SHARED EXCLUSIVE .names block_state$blk_ok_n181$true EXCLUSIVE # cache_req = 3 .mv cache_req$blk_ok_n182$true 4 ok blk_rreq blk_excl noop .names cache_req$blk_ok_n182$true noop # cache_state = 4 .mv cache_state$blk_ok_n183$true 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n183$true Wgrant # cache_state = 2 .mv cache_state$blk_ok_n184$false 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n184$false Wwait # if/else (blk_ok ) .mv cache_state$blk_ok$raw_n18c 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$blk_ok_n183$true cache_state$blk_ok_n184$false blk_ok cache_state$blk_ok$raw_n18c - - 0 =cache_state$blk_ok_n184$false - - 1 =cache_state$blk_ok_n183$true .mv block_state$blk_ok$raw_n18f 3 INVALID SHARED EXCLUSIVE .names block_state$blk_ok_n181$true block_state blk_ok block_state$blk_ok$raw_n18f - - 0 =block_state - - 1 =block_state$blk_ok_n181$true .names block_add$blk_ok_n180$true<0> block_add<0> blk_ok block_add$blk_ok$raw_n190<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$blk_ok$raw_n193 4 ok blk_rreq blk_excl noop .names cache_req$blk_ok_n182$true cache_req blk_ok cache_req$blk_ok$raw_n193 - - 0 =cache_req - - 1 =cache_req$blk_ok_n182$true .names block_val$blk_ok_n17f$true block_val blk_ok block_val$blk_ok$raw_n194 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # if/else (write_back_req ) .mv cache_state$write_back_req$raw_n198 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$write_back_req_n17d$true cache_state$blk_ok$raw_n18c write_back_req cache_state$write_back_req$raw_n198 - - 0 =cache_state$blk_ok$raw_n18c - - 1 =cache_state$write_back_req_n17d$true .mv block_state$write_back_req$raw_n19a 3 INVALID SHARED EXCLUSIVE .names block_state block_state$blk_ok$raw_n18f write_back_req block_state$write_back_req$raw_n19a - - 0 =block_state$blk_ok$raw_n18f - - 1 =block_state .names block_add<0> block_add$blk_ok$raw_n190<0> write_back_req block_add$write_back_req$raw_n19b<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$blk_ok$raw_n194 write_back_req block_val$write_back_req$raw_n19e 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$write_back_req$raw_n1a0 4 ok blk_rreq blk_excl noop .names cache_req cache_req$blk_ok$raw_n193 write_back_req cache_req$write_back_req$raw_n1a0 - - 0 =cache_req$blk_ok$raw_n193 - - 1 =cache_req # if/else ((inval ) && (block_add == blocknum )) .mv block_state$_n177$raw_n1a4 3 INVALID SHARED EXCLUSIVE .names block_state$_n177_n179$true block_state$write_back_req$raw_n19a _n177 block_state$_n177$raw_n1a4 - - 0 =block_state$write_back_req$raw_n19a - - 1 =block_state$_n177_n179$true .mv cache_state$_n177$raw_n1a5 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n177_n17b$true cache_state$write_back_req$raw_n198 _n177 cache_state$_n177$raw_n1a5 - - 0 =cache_state$write_back_req$raw_n198 - - 1 =cache_state$_n177_n17b$true .mv cache_req$_n177$raw_n1a6 4 ok blk_rreq blk_excl noop .names cache_req$_n177_n17a$true cache_req$write_back_req$raw_n1a0 _n177 cache_req$_n177$raw_n1a6 - - 0 =cache_req$write_back_req$raw_n1a0 - - 1 =cache_req$_n177_n17a$true .names block_add<0> block_add$write_back_req$raw_n19b<0> _n177 block_add$_n177$raw_n1ab<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$write_back_req$raw_n19e _n177 block_val$_n177$raw_n1af 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # cache_req = 3 .mv cache_req$raw_n1b1 4 ok blk_rreq blk_excl noop .names cache_req$raw_n1b1 noop # case (cache_state ) .mv cache_req$_n171$raw_n1bb 4 ok blk_rreq blk_excl noop .names cache_req$_n177$raw_n1a6 cache_req$raw_n1b1 _n171 cache_req$_n171$raw_n1bb - - 0 =cache_req$raw_n1b1 - - 1 =cache_req$_n177$raw_n1a6 .mv block_state$_n171$raw_n1bc 3 INVALID SHARED EXCLUSIVE .names block_state$_n177$raw_n1a4 block_state _n171 block_state$_n171$raw_n1bc - - 0 =block_state - - 1 =block_state$_n177$raw_n1a4 .names block_add$_n177$raw_n1ab<0> block_add<0> _n171 block_add$_n171$raw_n1bd<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_state$_n171$raw_n1bf 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n177$raw_n1a5 cache_state _n171 cache_state$_n171$raw_n1bf - - 0 =cache_state - - 1 =cache_state$_n177$raw_n1a5 .names block_val$_n177$raw_n1af block_val _n171 block_val$_n171$raw_n1c0 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$_n131$raw_n1c9 3 INVALID SHARED EXCLUSIVE .names block_state$_n137$raw_n164 block_state$_n171$raw_n1bc _n131 block_state$_n131$raw_n1c9 - - 0 =block_state$_n171$raw_n1bc - - 1 =block_state$_n137$raw_n164 .names block_add$_n137$raw_n16b<0> block_add$_n171$raw_n1bd<0> _n131 block_add$_n131$raw_n1ca<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_state$_n131$raw_n1cc 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n137$raw_n165 cache_state$_n171$raw_n1bf _n131 cache_state$_n131$raw_n1cc - - 0 =cache_state$_n171$raw_n1bf - - 1 =cache_state$_n137$raw_n165 .names block_val$_n137$raw_n16f block_val$_n171$raw_n1c0 _n131 block_val$_n131$raw_n1cd 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$_n131$raw_n1cf 4 ok blk_rreq blk_excl noop .names cache_req$_n137$raw_n166 cache_req$_n171$raw_n1bb _n131 cache_req$_n131$raw_n1cf - - 0 =cache_req$_n171$raw_n1bb - - 1 =cache_req$_n137$raw_n166 .mv block_state$_n118$raw_n1de 3 INVALID SHARED EXCLUSIVE .names block_state$_n11e$raw_n12b block_state$_n131$raw_n1c9 _n118 block_state$_n118$raw_n1de - - 0 =block_state$_n131$raw_n1c9 - - 1 =block_state$_n11e$raw_n12b .mv cache_state$_n118$raw_n1df 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n11e$raw_n129 cache_state$_n131$raw_n1cc _n118 cache_state$_n118$raw_n1df - - 0 =cache_state$_n131$raw_n1cc - - 1 =cache_state$_n11e$raw_n129 .names block_val$_n11e$raw_n12f block_val$_n131$raw_n1cd _n118 block_val$_n118$raw_n1e0 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv cache_req$_n118$raw_n1e2 4 ok blk_rreq blk_excl noop .names cache_req$_n11e$raw_n12d cache_req$_n131$raw_n1cf _n118 cache_req$_n118$raw_n1e2 - - 0 =cache_req$_n131$raw_n1cf - - 1 =cache_req$_n11e$raw_n12d .names block_add<0> block_add$_n131$raw_n1ca<0> _n118 block_add$_n118$raw_n1e8<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$_n102$raw_n1f0 3 INVALID SHARED EXCLUSIVE .names block_state$_n108$raw_n114 block_state$_n118$raw_n1de _n102 block_state$_n102$raw_n1f0 - - 0 =block_state$_n118$raw_n1de - - 1 =block_state$_n108$raw_n114 .mv cache_state$_n102$raw_n1f1 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n108$raw_n112 cache_state$_n118$raw_n1df _n102 cache_state$_n102$raw_n1f1 - - 0 =cache_state$_n118$raw_n1df - - 1 =cache_state$_n108$raw_n112 .mv cache_req$_n102$raw_n1f2 4 ok blk_rreq blk_excl noop .names cache_req$_n108$raw_n116 cache_req$_n118$raw_n1e2 _n102 cache_req$_n102$raw_n1f2 - - 0 =cache_req$_n118$raw_n1e2 - - 1 =cache_req$_n108$raw_n116 .names block_add<0> block_add$_n118$raw_n1e8<0> _n102 block_add$_n102$raw_n1f7<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$_n118$raw_n1e0 _n102 block_val$_n102$raw_n1fb 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv block_state$_n7b$raw_n202 3 INVALID SHARED EXCLUSIVE .names block_state$_n81$raw_nf7 block_state$_n102$raw_n1f0 _n7b block_state$_n7b$raw_n202 - - 0 =block_state$_n102$raw_n1f0 - - 1 =block_state$_n81$raw_nf7 .mv cache_state$_n7b$raw_n203 5 Ready Rwait Wwait Rgrant Wgrant .names cache_state$_n81$raw_nf8 cache_state$_n102$raw_n1f1 _n7b cache_state$_n7b$raw_n203 - - 0 =cache_state$_n102$raw_n1f1 - - 1 =cache_state$_n81$raw_nf8 .mv cache_req$_n7b$raw_n204 4 ok blk_rreq blk_excl noop .names cache_req$_n81$raw_nf9 cache_req$_n102$raw_n1f2 _n7b cache_req$_n7b$raw_n204 - - 0 =cache_req$_n102$raw_n1f2 - - 1 =cache_req$_n81$raw_nf9 .names blk_add$_n81$raw_nfd<0> blk_add<0> _n7b blk_add$_n7b$raw_n205<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_add<0> block_add$_n102$raw_n1f7<0> _n7b block_add$_n7b$raw_n20b<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names block_val block_val$_n102$raw_n1fb _n7b block_val$_n7b$raw_n20e 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # conflict arbitrators .names back_data$raw_n6b back_data 0 0 1 1 .names _n7b _n82 _n86 _n8a _n91 _na7 _nae _n211 .def 0 1 0 0 1 1 - - 1 1 0 0 0 - 1 1 1 1 0 0 0 - 0 - 1 .names _n211 blk_add$_n7b$raw_n205<0> blk_add<0> -> _n212<0> 1 - - =blk_add$_n7b$raw_n205<0> 0 - - =blk_add<0> .names _n7b _n82 _n86 _n8a _n91 _na7 _nae _n102 _n109 _n118 _n11f _n131 _n138 _n13c _n13e _n171 _n178 _n17c _n17e _n213 .def 0 1 1 - - - - - - - - - - - - - - - - - 1 1 0 1 - - - - - - - - - - - - - - - - 1 1 0 0 1 1 - - - - - - - - - - - - - - 1 1 0 0 0 - 1 1 - - - - - - - - - - - - 1 0 - - - - - - 1 1 - - - - - - - - - - 1 0 - - - - - - 0 - 1 1 - - - - - - - - 1 0 - - - - - - 0 - 0 - 1 1 - - - - - - 1 0 - - - - - - 0 - 0 - 1 0 0 1 - - - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 1 - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 0 0 1 1 .mv _n214 3 INVALID SHARED EXCLUSIVE .names _n213 block_state$_n7b$raw_n202 block_state _n214 1 - - =block_state$_n7b$raw_n202 0 - - =block_state .names _n7b _n102 _n118 _n131 _n138 _n13c _n13e _n171 _n178 _n17c _n17e _n219 .def 0 0 0 0 1 0 0 1 - - - - 1 0 0 0 0 - - - 1 0 0 1 1 .names _n219 block_add$_n7b$raw_n20b<0> block_add<0> -> _n21a<0> 1 - - =block_add$_n7b$raw_n20b<0> 0 - - =block_add<0> .names _n7b _n82 _n86 _n8a _n91 _na7 _nae _n102 _n109 _n118 _n11f _n131 _n138 _n13c _n13e _n171 _n178 _n17c _n17e _n21b .def 0 1 1 - - - - - - - - - - - - - - - - - 1 1 0 1 - - - - - - - - - - - - - - - - 1 1 0 0 1 1 - - - - - - - - - - - - - - 1 1 0 0 1 0 - - - - - - - - - - - - - - 1 1 0 0 0 - 1 1 - - - - - - - - - - - - 1 1 0 0 0 - 1 0 - - - - - - - - - - - - 1 0 - - - - - - 1 1 - - - - - - - - - - 1 0 - - - - - - 1 0 - - - - - - - - - - 1 0 - - - - - - 0 - 1 1 - - - - - - - - 1 0 - - - - - - 0 - 1 0 - - - - - - - - 1 0 - - - - - - 0 - 0 - 1 1 - - - - - - 1 0 - - - - - - 0 - 0 - 1 0 1 - - - - - 1 0 - - - - - - 0 - 0 - 1 0 0 1 - - - - 1 0 - - - - - - 0 - 0 - 1 0 0 0 - - - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 1 - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 0 1 - 1 0 - - - - - - 0 - 0 - 0 - - - 1 0 0 1 1 0 - - - - - - 0 - 0 - 0 - - - 1 0 0 0 1 .mv _n21c 5 Ready Rwait Wwait Rgrant Wgrant .names _n21b cache_state$_n7b$raw_n203 cache_state _n21c 1 - - =cache_state$_n7b$raw_n203 0 - - =cache_state .names _n7b _n102 _n118 _n11f _n131 _n138 _n13c _n13e _n171 _n178 _n17c _n17e _n221 .def 0 0 0 1 0 - - - - - - - - 1 0 0 0 - 1 0 0 1 - - - - 1 0 0 0 - 0 - - - 1 0 0 1 1 .names _n221 block_val$_n7b$raw_n20e block_val _n222 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n7b _n82 _n86 _n8a _n91 _na7 _nae _n102 _n109 _n118 _n11f _n131 _n138 _n13c _n13e _n171 _n178 _n17c _n17e _n223 .def 0 1 1 - - - - - - - - - - - - - - - - - 1 1 0 1 - - - - - - - - - - - - - - - - 1 1 0 0 1 1 - - - - - - - - - - - - - - 1 1 0 0 1 0 - - - - - - - - - - - - - - 1 1 0 0 0 - 1 1 - - - - - - - - - - - - 1 1 0 0 0 - 1 0 - - - - - - - - - - - - 1 1 0 0 0 - 0 - - - - - - - - - - - - - 1 0 - - - - - - 1 1 - - - - - - - - - - 1 0 - - - - - - 0 - 1 1 - - - - - - - - 1 0 - - - - - - 0 - 0 - 1 1 - - - - - - 1 0 - - - - - - 0 - 0 - 1 0 0 1 - - - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 1 - - 1 0 - - - - - - 0 - 0 - 0 - - - 1 0 0 1 1 0 - - - - - - 0 - 0 - 0 - - - 0 - - - 1 .mv _n224 4 ok blk_rreq blk_excl noop .names _n223 cache_req$_n7b$raw_n204 cache_req _n224 1 - - =cache_req$_n7b$raw_n204 0 - - =cache_req .names acknowledge$raw_n71 acknowledge 0 0 1 1 # non-blocking assignments # latches .r blk_add$raw_n69<0> blk_add<0> .def 0 1 1 .latch _n212<0> blk_add<0> .r block_state$raw_n66 block_state - =block_state$raw_n66 .latch _n214 block_state .r block_add$raw_n67<0> block_add<0> .def 0 1 1 .latch _n21a<0> block_add<0> .r cache_state$raw_n65 cache_state - =cache_state$raw_n65 .latch _n21c cache_state .r cache_req$raw_n6a cache_req - =cache_req$raw_n6a .latch _n224 cache_req .r block_val$raw_n68 block_val 0 0 1 1 .latch _n222 block_val # quasi-continuous assignment .end .model DIRECTORY # I/O ports .outputs blk_ok2 .outputs write_back_req2 .outputs blk_ok1 .outputs write_back_req1 .inputs blk_add2<0> .outputs inval2 .inputs blk_add1<0> .outputs blk_data .outputs inval1 .inputs cache_req2 .inputs back_data2 .inputs cache_req1 .inputs back_data1 .outputs blocknum<0> .mv cache_req2 4 ok blk_rreq blk_excl noop .mv cache_req1 4 ok blk_rreq blk_excl noop .mv arbiter_state 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE # arbiter_state = 0 .mv arbiter_state$raw_n229 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$raw_n229 ONE # main_mem [0] = 0 .names _n22c<0> 0 .names _n22d<0> 0 .names _n22d<0> _n22c<0> _n22f<0> .def 0 0 1 1 1 0 1 .names _n22f<0> _n230 .def 1 0 0 .names _n230 _n22e 0 1 1 0 .names _n231 0 .names _n22b _n231 _n22e main_mem$raw_n22a<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n233<0> 1 .names _n233<0> _n22c<0> _n235<0> .def 0 0 1 1 1 0 1 .names _n235<0> _n236 .def 1 0 0 .names _n236 _n234 0 1 1 0 .names _n237 0 .names _n22b _n237 _n234 main_mem$raw_n22a<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n22b 0 # cache_Rlist1 [0] = 0 .names _n23b<0> 0 .names _n23c<0> 0 .names _n23c<0> _n23b<0> _n23e<0> .def 0 0 1 1 1 0 1 .names _n23e<0> _n23f .def 1 0 0 .names _n23f _n23d 0 1 1 0 .names _n240 0 .names _n23a _n240 _n23d cache_Rlist1$raw_n239<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n242<0> 1 .names _n242<0> _n23b<0> _n244<0> .def 0 0 1 1 1 0 1 .names _n244<0> _n245 .def 1 0 0 .names _n245 _n243 0 1 1 0 .names _n246 0 .names _n23a _n246 _n243 cache_Rlist1$raw_n239<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n23a 0 # cache_Rlist2 [0] = 0 .names _n24a<0> 0 .names _n24b<0> 0 .names _n24b<0> _n24a<0> _n24d<0> .def 0 0 1 1 1 0 1 .names _n24d<0> _n24e .def 1 0 0 .names _n24e _n24c 0 1 1 0 .names _n24f 0 .names _n249 _n24f _n24c cache_Rlist2$raw_n248<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n251<0> 1 .names _n251<0> _n24a<0> _n253<0> .def 0 0 1 1 1 0 1 .names _n253<0> _n254 .def 1 0 0 .names _n254 _n252 0 1 1 0 .names _n255 0 .names _n249 _n255 _n252 cache_Rlist2$raw_n248<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n249 0 # cache_Wlist1 [0] = 0 .names _n259<0> 0 .names _n25a<0> 0 .names _n25a<0> _n259<0> _n25c<0> .def 0 0 1 1 1 0 1 .names _n25c<0> _n25d .def 1 0 0 .names _n25d _n25b 0 1 1 0 .names _n25e 0 .names _n258 _n25e _n25b cache_Wlist1$raw_n257<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n260<0> 1 .names _n260<0> _n259<0> _n262<0> .def 0 0 1 1 1 0 1 .names _n262<0> _n263 .def 1 0 0 .names _n263 _n261 0 1 1 0 .names _n264 0 .names _n258 _n264 _n261 cache_Wlist1$raw_n257<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n258 0 # cache_Wlist2 [0] = 0 .names _n268<0> 0 .names _n269<0> 0 .names _n269<0> _n268<0> _n26b<0> .def 0 0 1 1 1 0 1 .names _n26b<0> _n26c .def 1 0 0 .names _n26c _n26a 0 1 1 0 .names _n26d 0 .names _n267 _n26d _n26a cache_Wlist2$raw_n266<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n26f<0> 1 .names _n26f<0> _n268<0> _n271<0> .def 0 0 1 1 1 0 1 .names _n271<0> _n272 .def 1 0 0 .names _n272 _n270 0 1 1 0 .names _n273 0 .names _n267 _n273 _n270 cache_Wlist2$raw_n266<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n267 0 # main_mem [1] = 0 .names _n277<0> 1 .names _n278<0> 0 .names _n278<0> _n277<0> _n27a<0> .def 0 0 1 1 1 0 1 .names _n27a<0> _n27b .def 1 0 0 .names _n27b _n279 0 1 1 0 .names _n276 main_mem$raw_n22a<*0*> _n279 main_mem$raw_n275<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n27d<0> 1 .names _n27d<0> _n277<0> _n27f<0> .def 0 0 1 1 1 0 1 .names _n27f<0> _n280 .def 1 0 0 .names _n280 _n27e 0 1 1 0 .names _n276 main_mem$raw_n22a<*1*> _n27e main_mem$raw_n275<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n276 0 # cache_Rlist1 [1] = 0 .names _n284<0> 1 .names _n285<0> 0 .names _n285<0> _n284<0> _n287<0> .def 0 0 1 1 1 0 1 .names _n287<0> _n288 .def 1 0 0 .names _n288 _n286 0 1 1 0 .names _n283 cache_Rlist1$raw_n239<*0*> _n286 cache_Rlist1$raw_n282<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n28a<0> 1 .names _n28a<0> _n284<0> _n28c<0> .def 0 0 1 1 1 0 1 .names _n28c<0> _n28d .def 1 0 0 .names _n28d _n28b 0 1 1 0 .names _n283 cache_Rlist1$raw_n239<*1*> _n28b cache_Rlist1$raw_n282<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n283 0 # cache_Rlist2 [1] = 0 .names _n291<0> 1 .names _n292<0> 0 .names _n292<0> _n291<0> _n294<0> .def 0 0 1 1 1 0 1 .names _n294<0> _n295 .def 1 0 0 .names _n295 _n293 0 1 1 0 .names _n290 cache_Rlist2$raw_n248<*0*> _n293 cache_Rlist2$raw_n28f<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n297<0> 1 .names _n297<0> _n291<0> _n299<0> .def 0 0 1 1 1 0 1 .names _n299<0> _n29a .def 1 0 0 .names _n29a _n298 0 1 1 0 .names _n290 cache_Rlist2$raw_n248<*1*> _n298 cache_Rlist2$raw_n28f<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n290 0 # cache_Wlist1 [1] = 0 .names _n29e<0> 1 .names _n29f<0> 0 .names _n29f<0> _n29e<0> _n2a1<0> .def 0 0 1 1 1 0 1 .names _n2a1<0> _n2a2 .def 1 0 0 .names _n2a2 _n2a0 0 1 1 0 .names _n29d cache_Wlist1$raw_n257<*0*> _n2a0 cache_Wlist1$raw_n29c<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2a4<0> 1 .names _n2a4<0> _n29e<0> _n2a6<0> .def 0 0 1 1 1 0 1 .names _n2a6<0> _n2a7 .def 1 0 0 .names _n2a7 _n2a5 0 1 1 0 .names _n29d cache_Wlist1$raw_n257<*1*> _n2a5 cache_Wlist1$raw_n29c<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n29d 0 # cache_Wlist2 [1] = 0 .names _n2ab<0> 1 .names _n2ac<0> 0 .names _n2ac<0> _n2ab<0> _n2ae<0> .def 0 0 1 1 1 0 1 .names _n2ae<0> _n2af .def 1 0 0 .names _n2af _n2ad 0 1 1 0 .names _n2aa cache_Wlist2$raw_n266<*0*> _n2ad cache_Wlist2$raw_n2a9<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2b1<0> 1 .names _n2b1<0> _n2ab<0> _n2b3<0> .def 0 0 1 1 1 0 1 .names _n2b3<0> _n2b4 .def 1 0 0 .names _n2b4 _n2b2 0 1 1 0 .names _n2aa cache_Wlist2$raw_n266<*1*> _n2b2 cache_Wlist2$raw_n2a9<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2aa 0 # non-blocking assignments for initial # assign inval1 = ((arbiter_state == TWO ) && (cache_req2 == blk_excl )) ? 1 : 0 .mv _n2b8 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2b8 TWO # arbiter_state == 2 .names arbiter_state _n2b8 _n2b7 .def 0 - =arbiter_state 1 .mv _n2ba 4 ok blk_rreq blk_excl noop .names _n2ba blk_excl # cache_req2 == 2 .names cache_req2 _n2ba _n2b9 .def 0 - =cache_req2 1 # (arbiter_state == 2) && (cache_req2 == 2) .names _n2b7 _n2b9 _n2bb .def 0 1 1 1 .names _n2bc 1 .names _n2bd 0 # ((arbiter_state == 2) && (cache_req2 == 2)) ? 1 : 0 .names _n2bc _n2bd _n2bb _n2be 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2be inval1$raw_n2b6 - =_n2be # assign inval2 = ((arbiter_state == ONE ) && (cache_req1 == blk_excl )) ? 1 : 0 .mv _n2c2 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2c2 ONE # arbiter_state == 0 .names arbiter_state _n2c2 _n2c1 .def 0 - =arbiter_state 1 .mv _n2c4 4 ok blk_rreq blk_excl noop .names _n2c4 blk_excl # cache_req1 == 2 .names cache_req1 _n2c4 _n2c3 .def 0 - =cache_req1 1 # (arbiter_state == 0) && (cache_req1 == 2) .names _n2c1 _n2c3 _n2c5 .def 0 1 1 1 .names _n2c6 1 .names _n2c7 0 # ((arbiter_state == 0) && (cache_req1 == 2)) ? 1 : 0 .names _n2c6 _n2c7 _n2c5 _n2c8 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2c8 inval2$raw_n2c0 - =_n2c8 # assign write_back_req1 = ((arbiter_state == TWOWAIT ) && (cache_req1 != ok )) ? 1 : 0 .mv _n2cc 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2cc TWOWAIT # arbiter_state == 3 .names arbiter_state _n2cc _n2cb .def 0 - =arbiter_state 1 .mv _n2ce 4 ok blk_rreq blk_excl noop .names _n2ce ok # cache_req1 != 0 .names cache_req1 _n2ce _n2cd .def 1 - =cache_req1 0 # (arbiter_state == 3) && (cache_req1 != 0) .names _n2cb _n2cd _n2cf .def 0 1 1 1 .names _n2d0 1 .names _n2d1 0 # ((arbiter_state == 3) && (cache_req1 != 0)) ? 1 : 0 .names _n2d0 _n2d1 _n2cf _n2d2 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2d2 write_back_req1$raw_n2ca - =_n2d2 # assign write_back_req2 = ((arbiter_state == ONEWAIT ) && (cache_req2 != ok )) ? 1 : 0 .mv _n2d6 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2d6 ONEWAIT # arbiter_state == 1 .names arbiter_state _n2d6 _n2d5 .def 0 - =arbiter_state 1 .mv _n2d8 4 ok blk_rreq blk_excl noop .names _n2d8 ok # cache_req2 != 0 .names cache_req2 _n2d8 _n2d7 .def 1 - =cache_req2 0 # (arbiter_state == 1) && (cache_req2 != 0) .names _n2d5 _n2d7 _n2d9 .def 0 1 1 1 .names _n2da 1 .names _n2db 0 # ((arbiter_state == 1) && (cache_req2 != 0)) ? 1 : 0 .names _n2da _n2db _n2d9 _n2dc 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2dc write_back_req2$raw_n2d4 - =_n2dc # assign blk_data = (arbiter_state == ONESERVE ) ? main_mem [blk_add1 ] : (arbiter_state == TWOSERVE ) ? main_mem [blk_add2 ] : 0 .mv _n2e0 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2e0 ONESERVE # arbiter_state == 4 .names arbiter_state _n2e0 _n2df .def 0 - =arbiter_state 1 .names main_mem<*0*> main_mem<*1*> blk_add1<0> _n2e1 0 - 0 0 1 - 0 1 - 0 1 0 - 1 1 1 .mv _n2e3 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2e3 TWOSERVE # arbiter_state == 5 .names arbiter_state _n2e3 _n2e2 .def 0 - =arbiter_state 1 .names main_mem<*0*> main_mem<*1*> blk_add2<0> _n2e4 0 - 0 0 1 - 0 1 - 0 1 0 - 1 1 1 .names _n2e5 0 # (arbiter_state == 5) ? main_mem [blk_add2 ] : 0 .names _n2e4 _n2e5 _n2e2 _n2e6 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # (arbiter_state == 4) ? main_mem [blk_add1 ] : (arbiter_state == 5) ? main_mem [blk_add2 ] : 0 .names _n2e1 _n2e6 _n2df _n2e8 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2e8 blk_data$raw_n2de - =_n2e8 # assign blk_ok1 = (arbiter_state == ONESERVE ) ? 1 : 0 .mv _n2ec 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2ec ONESERVE # arbiter_state == 4 .names arbiter_state _n2ec _n2eb .def 0 - =arbiter_state 1 .names _n2ed 1 .names _n2ee 0 # (arbiter_state == 4) ? 1 : 0 .names _n2ed _n2ee _n2eb _n2ef 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2ef blk_ok1$raw_n2ea - =_n2ef # assign blk_ok2 = (arbiter_state == TWOSERVE ) ? 1 : 0 .mv _n2f3 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2f3 TWOSERVE # arbiter_state == 5 .names arbiter_state _n2f3 _n2f2 .def 0 - =arbiter_state 1 .names _n2f4 1 .names _n2f5 0 # (arbiter_state == 5) ? 1 : 0 .names _n2f4 _n2f5 _n2f2 _n2f6 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n2f6 blk_ok2$raw_n2f1 - =_n2f6 # assign blocknum = ((arbiter_state == ONE ) && (cache_req1 == blk_excl )) ? blk_add1 : ((arbiter_state == TWO ) && (cache_req2 == blk_excl )) ? blk_add2 : 0 .mv _n2fa 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2fa ONE # arbiter_state == 0 .names arbiter_state _n2fa _n2f9 .def 0 - =arbiter_state 1 .mv _n2fc 4 ok blk_rreq blk_excl noop .names _n2fc blk_excl # cache_req1 == 2 .names cache_req1 _n2fc _n2fb .def 0 - =cache_req1 1 # (arbiter_state == 0) && (cache_req1 == 2) .names _n2f9 _n2fb _n2fd .def 0 1 1 1 .mv _n2ff 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n2ff TWO # arbiter_state == 2 .names arbiter_state _n2ff _n2fe .def 0 - =arbiter_state 1 .mv _n301 4 ok blk_rreq blk_excl noop .names _n301 blk_excl # cache_req2 == 2 .names cache_req2 _n301 _n300 .def 0 - =cache_req2 1 # (arbiter_state == 2) && (cache_req2 == 2) .names _n2fe _n300 _n302 .def 0 1 1 1 .names _n303<0> 0 # ((arbiter_state == 2) && (cache_req2 == 2)) ? blk_add2 : 0 .names blk_add2<0> _n303<0> _n302 _n304<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # ((arbiter_state == 0) && (cache_req1 == 2)) ? blk_add1 : ((arbiter_state == 2) && (cache_req2 == 2)) ? blk_add2 : 0 .names blk_add1<0> _n304<0> _n2fd _n306<0> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n306<0> blocknum$raw_n2f8<0> - =_n306<0> .mv _n30a 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n30a ONE .names arbiter_state _n30a _n309 .def 0 - =arbiter_state 1 .names _n309 _n308 1 1 0 0 .mv _n30c 4 ok blk_rreq blk_excl noop .names _n30c blk_rreq # cache_req1 == 1 .names cache_req1 _n30c _n30b .def 0 - =cache_req1 1 .names _n30b _n30d - =_n30b .names cache_Wlist2<*0*> cache_Wlist2<*1*> blk_add1<0> _n30f 0 - 0 0 1 - 0 1 - 0 1 0 - 1 1 1 .names _n310 1 # cache_Wlist2 [blk_add1 ] == 1 .names _n30f _n310 _n311 .def 0 0 1 1 1 0 1 .names _n311 _n30e 0 1 1 0 .names _n30e _n313 - =_n30e # cache_Rlist1 [blk_add1 ] = 1 .names _n316<0> 0 .names _n316<0> blk_add1<0> _n318<0> .def 0 0 1 1 1 0 1 .names _n318<0> _n319 .def 1 0 0 .names _n319 _n317 0 1 1 0 .names _n315 cache_Rlist1<*0*> _n317 cache_Rlist1$_n30e_n314$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n31b<0> 1 .names _n31b<0> blk_add1<0> _n31d<0> .def 0 0 1 1 1 0 1 .names _n31d<0> _n31e .def 1 0 0 .names _n31e _n31c 0 1 1 0 .names _n315 cache_Rlist1<*1*> _n31c cache_Rlist1$_n30e_n314$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n315 1 # cache_Wlist2 [blk_add1 ] = 0 .names _n322<0> 0 .names _n322<0> blk_add1<0> _n324<0> .def 0 0 1 1 1 0 1 .names _n324<0> _n325 .def 1 0 0 .names _n325 _n323 0 1 1 0 .names _n321 cache_Wlist2<*0*> _n323 cache_Wlist2$_n30e_n320$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n327<0> 1 .names _n327<0> blk_add1<0> _n329<0> .def 0 0 1 1 1 0 1 .names _n329<0> _n32a .def 1 0 0 .names _n32a _n328 0 1 1 0 .names _n321 cache_Wlist2<*1*> _n328 cache_Wlist2$_n30e_n320$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n321 0 # cache_Rlist2 [blk_add1 ] = 1 .names _n32e<0> 0 .names _n32e<0> blk_add1<0> _n330<0> .def 0 0 1 1 1 0 1 .names _n330<0> _n331 .def 1 0 0 .names _n331 _n32f 0 1 1 0 .names _n32d cache_Rlist2<*0*> _n32f cache_Rlist2$_n30e_n32c$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n333<0> 1 .names _n333<0> blk_add1<0> _n335<0> .def 0 0 1 1 1 0 1 .names _n335<0> _n336 .def 1 0 0 .names _n336 _n334 0 1 1 0 .names _n32d cache_Rlist2<*1*> _n334 cache_Rlist2$_n30e_n32c$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n32d 1 # arbiter_state = 1 .mv arbiter_state$_n30e_n338$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n30e_n338$true ONEWAIT # cache_Wlist1 [0] = 0 .names _n33b<0> 0 .names _n33c<0> 0 .names _n33c<0> _n33b<0> _n33e<0> .def 0 0 1 1 1 0 1 .names _n33e<0> _n33f .def 1 0 0 .names _n33f _n33d 0 1 1 0 .names _n33a cache_Wlist1<*0*> _n33d cache_Wlist1$_n30e_n339$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n341<0> 1 .names _n341<0> _n33b<0> _n343<0> .def 0 0 1 1 1 0 1 .names _n343<0> _n344 .def 1 0 0 .names _n344 _n342 0 1 1 0 .names _n33a cache_Wlist1<*1*> _n342 cache_Wlist1$_n30e_n339$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n33a 0 # cache_Wlist1 [1] = 0 .names _n348<0> 1 .names _n349<0> 0 .names _n349<0> _n348<0> _n34b<0> .def 0 0 1 1 1 0 1 .names _n34b<0> _n34c .def 1 0 0 .names _n34c _n34a 0 1 1 0 .names _n347 cache_Wlist1$_n30e_n339$false<*0*> _n34a cache_Wlist1$_n30e_n346$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n34e<0> 1 .names _n34e<0> _n348<0> _n350<0> .def 0 0 1 1 1 0 1 .names _n350<0> _n351 .def 1 0 0 .names _n351 _n34f 0 1 1 0 .names _n347 cache_Wlist1$_n30e_n339$false<*1*> _n34f cache_Wlist1$_n30e_n346$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n347 0 # cache_Rlist1 [blk_add1 ] = 1 .names _n355<0> 0 .names _n355<0> blk_add1<0> _n357<0> .def 0 0 1 1 1 0 1 .names _n357<0> _n358 .def 1 0 0 .names _n358 _n356 0 1 1 0 .names _n354 cache_Rlist1<*0*> _n356 cache_Rlist1$_n30e_n353$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n35a<0> 1 .names _n35a<0> blk_add1<0> _n35c<0> .def 0 0 1 1 1 0 1 .names _n35c<0> _n35d .def 1 0 0 .names _n35d _n35b 0 1 1 0 .names _n354 cache_Rlist1<*1*> _n35b cache_Rlist1$_n30e_n353$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n354 1 # arbiter_state = 4 .mv arbiter_state$_n30e_n35f$false 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n30e_n35f$false ONESERVE # if/else (cache_Wlist2 [blk_add1 ] == 1) .names cache_Rlist1$_n30e_n314$true<*0*> cache_Rlist1$_n30e_n353$false<*0*> _n30e cache_Rlist1$_n30e$raw_n366<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n30e_n314$true<*1*> cache_Rlist1$_n30e_n353$false<*1*> _n30e cache_Rlist1$_n30e$raw_n366<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n30e$raw_n369 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n30e_n338$true arbiter_state$_n30e_n35f$false _n30e arbiter_state$_n30e$raw_n369 - - 0 =arbiter_state$_n30e_n35f$false - - 1 =arbiter_state$_n30e_n338$true .names cache_Wlist2$_n30e_n320$true<*0*> cache_Wlist2<*0*> _n30e cache_Wlist2$_n30e$raw_n36a<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n30e_n320$true<*1*> cache_Wlist2<*1*> _n30e cache_Wlist2$_n30e$raw_n36a<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30e_n32c$true<*0*> cache_Rlist2<*0*> _n30e cache_Rlist2$_n30e$raw_n36d<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30e_n32c$true<*1*> cache_Rlist2<*1*> _n30e cache_Rlist2$_n30e$raw_n36d<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1<*0*> cache_Wlist1$_n30e_n346$false<*0*> _n30e cache_Wlist1$_n30e$raw_n372<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1<*1*> cache_Wlist1$_n30e_n346$false<*1*> _n30e cache_Wlist1$_n30e$raw_n372<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n378 4 ok blk_rreq blk_excl noop .names _n378 blk_excl # cache_req1 == 2 .names cache_req1 _n378 _n377 .def 0 - =cache_req1 1 .names _n377 _n379 - =_n377 # cache_Wlist1 [blk_add1 ] = 1 .names _n37c<0> 0 .names _n37c<0> blk_add1<0> _n37e<0> .def 0 0 1 1 1 0 1 .names _n37e<0> _n37f .def 1 0 0 .names _n37f _n37d 0 1 1 0 .names _n37b cache_Wlist1<*0*> _n37d cache_Wlist1$_n377_n37a$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n381<0> 1 .names _n381<0> blk_add1<0> _n383<0> .def 0 0 1 1 1 0 1 .names _n383<0> _n384 .def 1 0 0 .names _n384 _n382 0 1 1 0 .names _n37b cache_Wlist1<*1*> _n382 cache_Wlist1$_n377_n37a$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n37b 1 # cache_Rlist1 [blk_add1 ] = 0 .names _n388<0> 0 .names _n388<0> blk_add1<0> _n38a<0> .def 0 0 1 1 1 0 1 .names _n38a<0> _n38b .def 1 0 0 .names _n38b _n389 0 1 1 0 .names _n387 cache_Rlist1<*0*> _n389 cache_Rlist1$_n377_n386$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n38d<0> 1 .names _n38d<0> blk_add1<0> _n38f<0> .def 0 0 1 1 1 0 1 .names _n38f<0> _n390 .def 1 0 0 .names _n390 _n38e 0 1 1 0 .names _n387 cache_Rlist1<*1*> _n38e cache_Rlist1$_n377_n386$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n387 0 # cache_Rlist2 [blk_add1 ] = 0 .names _n394<0> 0 .names _n394<0> blk_add1<0> _n396<0> .def 0 0 1 1 1 0 1 .names _n396<0> _n397 .def 1 0 0 .names _n397 _n395 0 1 1 0 .names _n393 cache_Rlist2<*0*> _n395 cache_Rlist2$_n377_n392$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n399<0> 1 .names _n399<0> blk_add1<0> _n39b<0> .def 0 0 1 1 1 0 1 .names _n39b<0> _n39c .def 1 0 0 .names _n39c _n39a 0 1 1 0 .names _n393 cache_Rlist2<*1*> _n39a cache_Rlist2$_n377_n392$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n393 0 # cache_Wlist2 [blk_add1 ] = 0 .names _n3a0<0> 0 .names _n3a0<0> blk_add1<0> _n3a2<0> .def 0 0 1 1 1 0 1 .names _n3a2<0> _n3a3 .def 1 0 0 .names _n3a3 _n3a1 0 1 1 0 .names _n39f cache_Wlist2<*0*> _n3a1 cache_Wlist2$_n377_n39e$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n3a5<0> 1 .names _n3a5<0> blk_add1<0> _n3a7<0> .def 0 0 1 1 1 0 1 .names _n3a7<0> _n3a8 .def 1 0 0 .names _n3a8 _n3a6 0 1 1 0 .names _n39f cache_Wlist2<*1*> _n3a6 cache_Wlist2$_n377_n39e$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n39f 0 # arbiter_state = 4 .mv arbiter_state$_n377_n3aa$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n377_n3aa$true ONESERVE # arbiter_state = 2 .mv arbiter_state$_n377_n3ab$false 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n377_n3ab$false TWO # if/else (cache_req1 == 2) .mv arbiter_state$_n377$raw_n3b5 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n377_n3aa$true arbiter_state$_n377_n3ab$false _n377 arbiter_state$_n377$raw_n3b5 - - 0 =arbiter_state$_n377_n3ab$false - - 1 =arbiter_state$_n377_n3aa$true .names cache_Wlist1$_n377_n37a$true<*0*> cache_Wlist1<*0*> _n377 cache_Wlist1$_n377$raw_n3b6<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n377_n37a$true<*1*> cache_Wlist1<*1*> _n377 cache_Wlist1$_n377$raw_n3b6<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n377_n39e$true<*0*> cache_Wlist2<*0*> _n377 cache_Wlist2$_n377$raw_n3b9<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n377_n39e$true<*1*> cache_Wlist2<*1*> _n377 cache_Wlist2$_n377$raw_n3b9<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n377_n392$true<*0*> cache_Rlist2<*0*> _n377 cache_Rlist2$_n377$raw_n3bc<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n377_n392$true<*1*> cache_Rlist2<*1*> _n377 cache_Rlist2$_n377$raw_n3bc<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n377_n386$true<*0*> cache_Rlist1<*0*> _n377 cache_Rlist1$_n377$raw_n3bf<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n377_n386$true<*1*> cache_Rlist1<*1*> _n377 cache_Rlist1$_n377$raw_n3bf<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # if/else (cache_req1 == 1) .names cache_Wlist1$_n30e$raw_n372<*0*> cache_Wlist1$_n377$raw_n3b6<*0*> _n30b cache_Wlist1$_n30b$raw_n3c9<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n30e$raw_n372<*1*> cache_Wlist1$_n377$raw_n3b6<*1*> _n30b cache_Wlist1$_n30b$raw_n3c9<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n30e$raw_n36a<*0*> cache_Wlist2$_n377$raw_n3b9<*0*> _n30b cache_Wlist2$_n30b$raw_n3cc<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n30e$raw_n36a<*1*> cache_Wlist2$_n377$raw_n3b9<*1*> _n30b cache_Wlist2$_n30b$raw_n3cc<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30e$raw_n36d<*0*> cache_Rlist2$_n377$raw_n3bc<*0*> _n30b cache_Rlist2$_n30b$raw_n3cf<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30e$raw_n36d<*1*> cache_Rlist2$_n377$raw_n3bc<*1*> _n30b cache_Rlist2$_n30b$raw_n3cf<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n30e$raw_n366<*0*> cache_Rlist1$_n377$raw_n3bf<*0*> _n30b cache_Rlist1$_n30b$raw_n3d2<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n30e$raw_n366<*1*> cache_Rlist1$_n377$raw_n3bf<*1*> _n30b cache_Rlist1$_n30b$raw_n3d2<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n30b$raw_n3d5 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n30e$raw_n369 arbiter_state$_n377$raw_n3b5 _n30b arbiter_state$_n30b$raw_n3d5 - - 0 =arbiter_state$_n377$raw_n3b5 - - 1 =arbiter_state$_n30e$raw_n369 .mv _n3e2 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n3e2 ONESERVE .names arbiter_state _n3e2 _n3e1 .def 0 - =arbiter_state 1 .names _n3e1 _n3e0 1 1 0 0 # arbiter_state = 2 .mv arbiter_state$_n3e0_n3e3$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n3e0_n3e3$true TWO .mv _n3e6 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n3e6 ONEWAIT .names arbiter_state _n3e6 _n3e5 .def 0 - =arbiter_state 1 .names _n3e5 _n3e4 1 1 0 0 .mv _n3e8 4 ok blk_rreq blk_excl noop .names _n3e8 ok # cache_req2 == 0 .names cache_req2 _n3e8 _n3e7 .def 0 - =cache_req2 1 .names _n3e7 _n3e9 - =_n3e7 # main_mem [blk_add1 ] = back_data2 .names _n3ec<0> 0 .names _n3ec<0> blk_add1<0> _n3ee<0> .def 0 0 1 1 1 0 1 .names _n3ee<0> _n3ef .def 1 0 0 .names _n3ef _n3ed 0 1 1 0 .names _n3eb main_mem<*0*> _n3ed main_mem$_n3e7_n3ea$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n3f1<0> 1 .names _n3f1<0> blk_add1<0> _n3f3<0> .def 0 0 1 1 1 0 1 .names _n3f3<0> _n3f4 .def 1 0 0 .names _n3f4 _n3f2 0 1 1 0 .names _n3eb main_mem<*1*> _n3f2 main_mem$_n3e7_n3ea$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names back_data2 _n3eb - =back_data2 # arbiter_state = 4 .mv arbiter_state$_n3e7_n3f6$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n3e7_n3f6$true ONESERVE # if/else (cache_req2 == 0) .names main_mem$_n3e7_n3ea$true<*0*> main_mem<*0*> _n3e7 main_mem$_n3e7$raw_n3fb<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem$_n3e7_n3ea$true<*1*> main_mem<*1*> _n3e7 main_mem$_n3e7$raw_n3fb<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n3e7$raw_n3fe 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n3e7_n3f6$true arbiter_state _n3e7 arbiter_state$_n3e7$raw_n3fe - - 0 =arbiter_state - - 1 =arbiter_state$_n3e7_n3f6$true .mv _n401 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n401 TWO .names arbiter_state _n401 _n400 .def 0 - =arbiter_state 1 .names _n400 _n3ff 1 1 0 0 .mv _n403 4 ok blk_rreq blk_excl noop .names _n403 blk_rreq # cache_req2 == 1 .names cache_req2 _n403 _n402 .def 0 - =cache_req2 1 .names _n402 _n404 - =_n402 .names cache_Wlist1<*0*> cache_Wlist1<*1*> blk_add2<0> _n406 0 - 0 0 1 - 0 1 - 0 1 0 - 1 1 1 .names _n407 1 # cache_Wlist1 [blk_add2 ] == 1 .names _n406 _n407 _n408 .def 0 0 1 1 1 0 1 .names _n408 _n405 0 1 1 0 .names _n405 _n40a - =_n405 # cache_Rlist2 [blk_add2 ] = 1 .names _n40d<0> 0 .names _n40d<0> blk_add2<0> _n40f<0> .def 0 0 1 1 1 0 1 .names _n40f<0> _n410 .def 1 0 0 .names _n410 _n40e 0 1 1 0 .names _n40c cache_Rlist2<*0*> _n40e cache_Rlist2$_n405_n40b$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n412<0> 1 .names _n412<0> blk_add2<0> _n414<0> .def 0 0 1 1 1 0 1 .names _n414<0> _n415 .def 1 0 0 .names _n415 _n413 0 1 1 0 .names _n40c cache_Rlist2<*1*> _n413 cache_Rlist2$_n405_n40b$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n40c 1 # cache_Wlist1 [blk_add2 ] = 0 .names _n419<0> 0 .names _n419<0> blk_add2<0> _n41b<0> .def 0 0 1 1 1 0 1 .names _n41b<0> _n41c .def 1 0 0 .names _n41c _n41a 0 1 1 0 .names _n418 cache_Wlist1<*0*> _n41a cache_Wlist1$_n405_n417$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n41e<0> 1 .names _n41e<0> blk_add2<0> _n420<0> .def 0 0 1 1 1 0 1 .names _n420<0> _n421 .def 1 0 0 .names _n421 _n41f 0 1 1 0 .names _n418 cache_Wlist1<*1*> _n41f cache_Wlist1$_n405_n417$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n418 0 # cache_Rlist1 [blk_add2 ] = 1 .names _n425<0> 0 .names _n425<0> blk_add2<0> _n427<0> .def 0 0 1 1 1 0 1 .names _n427<0> _n428 .def 1 0 0 .names _n428 _n426 0 1 1 0 .names _n424 cache_Rlist1<*0*> _n426 cache_Rlist1$_n405_n423$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n42a<0> 1 .names _n42a<0> blk_add2<0> _n42c<0> .def 0 0 1 1 1 0 1 .names _n42c<0> _n42d .def 1 0 0 .names _n42d _n42b 0 1 1 0 .names _n424 cache_Rlist1<*1*> _n42b cache_Rlist1$_n405_n423$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n424 1 # arbiter_state = 3 .mv arbiter_state$_n405_n42f$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n405_n42f$true TWOWAIT # cache_Wlist2 [0] = 0 .names _n432<0> 0 .names _n433<0> 0 .names _n433<0> _n432<0> _n435<0> .def 0 0 1 1 1 0 1 .names _n435<0> _n436 .def 1 0 0 .names _n436 _n434 0 1 1 0 .names _n431 cache_Wlist2<*0*> _n434 cache_Wlist2$_n405_n430$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n438<0> 1 .names _n438<0> _n432<0> _n43a<0> .def 0 0 1 1 1 0 1 .names _n43a<0> _n43b .def 1 0 0 .names _n43b _n439 0 1 1 0 .names _n431 cache_Wlist2<*1*> _n439 cache_Wlist2$_n405_n430$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n431 0 # cache_Wlist2 [1] = 0 .names _n43f<0> 1 .names _n440<0> 0 .names _n440<0> _n43f<0> _n442<0> .def 0 0 1 1 1 0 1 .names _n442<0> _n443 .def 1 0 0 .names _n443 _n441 0 1 1 0 .names _n43e cache_Wlist2$_n405_n430$false<*0*> _n441 cache_Wlist2$_n405_n43d$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n445<0> 1 .names _n445<0> _n43f<0> _n447<0> .def 0 0 1 1 1 0 1 .names _n447<0> _n448 .def 1 0 0 .names _n448 _n446 0 1 1 0 .names _n43e cache_Wlist2$_n405_n430$false<*1*> _n446 cache_Wlist2$_n405_n43d$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n43e 0 # cache_Rlist2 [blk_add2 ] = 1 .names _n44c<0> 0 .names _n44c<0> blk_add2<0> _n44e<0> .def 0 0 1 1 1 0 1 .names _n44e<0> _n44f .def 1 0 0 .names _n44f _n44d 0 1 1 0 .names _n44b cache_Rlist2<*0*> _n44d cache_Rlist2$_n405_n44a$false<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n451<0> 1 .names _n451<0> blk_add2<0> _n453<0> .def 0 0 1 1 1 0 1 .names _n453<0> _n454 .def 1 0 0 .names _n454 _n452 0 1 1 0 .names _n44b cache_Rlist2<*1*> _n452 cache_Rlist2$_n405_n44a$false<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n44b 1 # arbiter_state = 5 .mv arbiter_state$_n405_n456$false 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n405_n456$false TWOSERVE # if/else (cache_Wlist1 [blk_add2 ] == 1) .names cache_Rlist2$_n405_n40b$true<*0*> cache_Rlist2$_n405_n44a$false<*0*> _n405 cache_Rlist2$_n405$raw_n45c<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n405_n40b$true<*1*> cache_Rlist2$_n405_n44a$false<*1*> _n405 cache_Rlist2$_n405$raw_n45c<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n405$raw_n460 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n405_n42f$true arbiter_state$_n405_n456$false _n405 arbiter_state$_n405$raw_n460 - - 0 =arbiter_state$_n405_n456$false - - 1 =arbiter_state$_n405_n42f$true .names cache_Wlist1$_n405_n417$true<*0*> cache_Wlist1<*0*> _n405 cache_Wlist1$_n405$raw_n461<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n405_n417$true<*1*> cache_Wlist1<*1*> _n405 cache_Wlist1$_n405$raw_n461<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n405_n423$true<*0*> cache_Rlist1<*0*> _n405 cache_Rlist1$_n405$raw_n465<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n405_n423$true<*1*> cache_Rlist1<*1*> _n405 cache_Rlist1$_n405$raw_n465<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*0*> cache_Wlist2$_n405_n43d$false<*0*> _n405 cache_Wlist2$_n405$raw_n469<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*1*> cache_Wlist2$_n405_n43d$false<*1*> _n405 cache_Wlist2$_n405$raw_n469<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv _n46f 4 ok blk_rreq blk_excl noop .names _n46f blk_excl # cache_req2 == 2 .names cache_req2 _n46f _n46e .def 0 - =cache_req2 1 .names _n46e _n470 - =_n46e # cache_Wlist1 [blk_add2 ] = 0 .names _n473<0> 0 .names _n473<0> blk_add2<0> _n475<0> .def 0 0 1 1 1 0 1 .names _n475<0> _n476 .def 1 0 0 .names _n476 _n474 0 1 1 0 .names _n472 cache_Wlist1<*0*> _n474 cache_Wlist1$_n46e_n471$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n478<0> 1 .names _n478<0> blk_add2<0> _n47a<0> .def 0 0 1 1 1 0 1 .names _n47a<0> _n47b .def 1 0 0 .names _n47b _n479 0 1 1 0 .names _n472 cache_Wlist1<*1*> _n479 cache_Wlist1$_n46e_n471$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n472 0 # cache_Rlist1 [blk_add2 ] = 0 .names _n47f<0> 0 .names _n47f<0> blk_add2<0> _n481<0> .def 0 0 1 1 1 0 1 .names _n481<0> _n482 .def 1 0 0 .names _n482 _n480 0 1 1 0 .names _n47e cache_Rlist1<*0*> _n480 cache_Rlist1$_n46e_n47d$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n484<0> 1 .names _n484<0> blk_add2<0> _n486<0> .def 0 0 1 1 1 0 1 .names _n486<0> _n487 .def 1 0 0 .names _n487 _n485 0 1 1 0 .names _n47e cache_Rlist1<*1*> _n485 cache_Rlist1$_n46e_n47d$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n47e 0 # cache_Rlist2 [blk_add2 ] = 0 .names _n48b<0> 0 .names _n48b<0> blk_add2<0> _n48d<0> .def 0 0 1 1 1 0 1 .names _n48d<0> _n48e .def 1 0 0 .names _n48e _n48c 0 1 1 0 .names _n48a cache_Rlist2<*0*> _n48c cache_Rlist2$_n46e_n489$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n490<0> 1 .names _n490<0> blk_add2<0> _n492<0> .def 0 0 1 1 1 0 1 .names _n492<0> _n493 .def 1 0 0 .names _n493 _n491 0 1 1 0 .names _n48a cache_Rlist2<*1*> _n491 cache_Rlist2$_n46e_n489$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n48a 0 # cache_Wlist2 [blk_add2 ] = 1 .names _n497<0> 0 .names _n497<0> blk_add2<0> _n499<0> .def 0 0 1 1 1 0 1 .names _n499<0> _n49a .def 1 0 0 .names _n49a _n498 0 1 1 0 .names _n496 cache_Wlist2<*0*> _n498 cache_Wlist2$_n46e_n495$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n49c<0> 1 .names _n49c<0> blk_add2<0> _n49e<0> .def 0 0 1 1 1 0 1 .names _n49e<0> _n49f .def 1 0 0 .names _n49f _n49d 0 1 1 0 .names _n496 cache_Wlist2<*1*> _n49d cache_Wlist2$_n46e_n495$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n496 1 # arbiter_state = 5 .mv arbiter_state$_n46e_n4a1$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n46e_n4a1$true TWOSERVE # arbiter_state = 0 .mv arbiter_state$_n46e_n4a2$false 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n46e_n4a2$false ONE # if/else (cache_req2 == 2) .mv arbiter_state$_n46e$raw_n4ac 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n46e_n4a1$true arbiter_state$_n46e_n4a2$false _n46e arbiter_state$_n46e$raw_n4ac - - 0 =arbiter_state$_n46e_n4a2$false - - 1 =arbiter_state$_n46e_n4a1$true .names cache_Wlist1$_n46e_n471$true<*0*> cache_Wlist1<*0*> _n46e cache_Wlist1$_n46e$raw_n4ad<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n46e_n471$true<*1*> cache_Wlist1<*1*> _n46e cache_Wlist1$_n46e$raw_n4ad<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n46e_n495$true<*0*> cache_Wlist2<*0*> _n46e cache_Wlist2$_n46e$raw_n4b0<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n46e_n495$true<*1*> cache_Wlist2<*1*> _n46e cache_Wlist2$_n46e$raw_n4b0<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n46e_n489$true<*0*> cache_Rlist2<*0*> _n46e cache_Rlist2$_n46e$raw_n4b3<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n46e_n489$true<*1*> cache_Rlist2<*1*> _n46e cache_Rlist2$_n46e$raw_n4b3<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n46e_n47d$true<*0*> cache_Rlist1<*0*> _n46e cache_Rlist1$_n46e$raw_n4b6<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n46e_n47d$true<*1*> cache_Rlist1<*1*> _n46e cache_Rlist1$_n46e$raw_n4b6<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # if/else (cache_req2 == 1) .names cache_Wlist1$_n405$raw_n461<*0*> cache_Wlist1$_n46e$raw_n4ad<*0*> _n402 cache_Wlist1$_n402$raw_n4c0<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n405$raw_n461<*1*> cache_Wlist1$_n46e$raw_n4ad<*1*> _n402 cache_Wlist1$_n402$raw_n4c0<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n405$raw_n469<*0*> cache_Wlist2$_n46e$raw_n4b0<*0*> _n402 cache_Wlist2$_n402$raw_n4c3<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n405$raw_n469<*1*> cache_Wlist2$_n46e$raw_n4b0<*1*> _n402 cache_Wlist2$_n402$raw_n4c3<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n405$raw_n45c<*0*> cache_Rlist2$_n46e$raw_n4b3<*0*> _n402 cache_Rlist2$_n402$raw_n4c6<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n405$raw_n45c<*1*> cache_Rlist2$_n46e$raw_n4b3<*1*> _n402 cache_Rlist2$_n402$raw_n4c6<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n405$raw_n465<*0*> cache_Rlist1$_n46e$raw_n4b6<*0*> _n402 cache_Rlist1$_n402$raw_n4c9<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n405$raw_n465<*1*> cache_Rlist1$_n46e$raw_n4b6<*1*> _n402 cache_Rlist1$_n402$raw_n4c9<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n402$raw_n4cc 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n405$raw_n460 arbiter_state$_n46e$raw_n4ac _n402 arbiter_state$_n402$raw_n4cc - - 0 =arbiter_state$_n46e$raw_n4ac - - 1 =arbiter_state$_n405$raw_n460 .mv _n4d9 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n4d9 TWOSERVE .names arbiter_state _n4d9 _n4d8 .def 0 - =arbiter_state 1 .names _n4d8 _n4d7 1 1 0 0 # arbiter_state = 0 .mv arbiter_state$_n4d7_n4da$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n4d7_n4da$true ONE .mv _n4dd 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n4dd TWOWAIT .names arbiter_state _n4dd _n4dc .def 0 - =arbiter_state 1 .names _n4dc _n4db 1 1 0 0 .mv _n4df 4 ok blk_rreq blk_excl noop .names _n4df ok # cache_req1 == 0 .names cache_req1 _n4df _n4de .def 0 - =cache_req1 1 .names _n4de _n4e0 - =_n4de # main_mem [blk_add2 ] = back_data1 .names _n4e3<0> 0 .names _n4e3<0> blk_add2<0> _n4e5<0> .def 0 0 1 1 1 0 1 .names _n4e5<0> _n4e6 .def 1 0 0 .names _n4e6 _n4e4 0 1 1 0 .names _n4e2 main_mem<*0*> _n4e4 main_mem$_n4de_n4e1$true<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names _n4e8<0> 1 .names _n4e8<0> blk_add2<0> _n4ea<0> .def 0 0 1 1 1 0 1 .names _n4ea<0> _n4eb .def 1 0 0 .names _n4eb _n4e9 0 1 1 0 .names _n4e2 main_mem<*1*> _n4e9 main_mem$_n4de_n4e1$true<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names back_data1 _n4e2 - =back_data1 # arbiter_state = 5 .mv arbiter_state$_n4de_n4ed$true 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n4de_n4ed$true TWOSERVE # if/else (cache_req1 == 0) .names main_mem$_n4de_n4e1$true<*0*> main_mem<*0*> _n4de main_mem$_n4de$raw_n4f2<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem$_n4de_n4e1$true<*1*> main_mem<*1*> _n4de main_mem$_n4de$raw_n4f2<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n4de$raw_n4f5 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n4de_n4ed$true arbiter_state _n4de arbiter_state$_n4de$raw_n4f5 - - 0 =arbiter_state - - 1 =arbiter_state$_n4de_n4ed$true # case (arbiter_state ) .names main_mem$_n4de$raw_n4f2<*0*> main_mem<*0*> _n4db main_mem$_n4db$raw_n4fa<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem$_n4de$raw_n4f2<*1*> main_mem<*1*> _n4db main_mem$_n4db$raw_n4fa<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n4db$raw_n4fd 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n4de$raw_n4f5 arbiter_state _n4db arbiter_state$_n4db$raw_n4fd - - 0 =arbiter_state - - 1 =arbiter_state$_n4de$raw_n4f5 .mv arbiter_state$_n4d7$raw_n4ff 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n4d7_n4da$true arbiter_state$_n4db$raw_n4fd _n4d7 arbiter_state$_n4d7$raw_n4ff - - 0 =arbiter_state$_n4db$raw_n4fd - - 1 =arbiter_state$_n4d7_n4da$true .names main_mem<*0*> main_mem$_n4db$raw_n4fa<*0*> _n4d7 main_mem$_n4d7$raw_n501<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem<*1*> main_mem$_n4db$raw_n4fa<*1*> _n4d7 main_mem$_n4d7$raw_n501<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n3ff$raw_n50e 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n402$raw_n4cc arbiter_state$_n4d7$raw_n4ff _n3ff arbiter_state$_n3ff$raw_n50e - - 0 =arbiter_state$_n4d7$raw_n4ff - - 1 =arbiter_state$_n402$raw_n4cc .names cache_Wlist1$_n402$raw_n4c0<*0*> cache_Wlist1<*0*> _n3ff cache_Wlist1$_n3ff$raw_n50f<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n402$raw_n4c0<*1*> cache_Wlist1<*1*> _n3ff cache_Wlist1$_n3ff$raw_n50f<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n402$raw_n4c3<*0*> cache_Wlist2<*0*> _n3ff cache_Wlist2$_n3ff$raw_n512<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n402$raw_n4c3<*1*> cache_Wlist2<*1*> _n3ff cache_Wlist2$_n3ff$raw_n512<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n402$raw_n4c6<*0*> cache_Rlist2<*0*> _n3ff cache_Rlist2$_n3ff$raw_n515<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n402$raw_n4c6<*1*> cache_Rlist2<*1*> _n3ff cache_Rlist2$_n3ff$raw_n515<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n402$raw_n4c9<*0*> cache_Rlist1<*0*> _n3ff cache_Rlist1$_n3ff$raw_n518<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n402$raw_n4c9<*1*> cache_Rlist1<*1*> _n3ff cache_Rlist1$_n3ff$raw_n518<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem<*0*> main_mem$_n4d7$raw_n501<*0*> _n3ff main_mem$_n3ff$raw_n51c<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem<*1*> main_mem$_n4d7$raw_n501<*1*> _n3ff main_mem$_n3ff$raw_n51c<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem$_n3e7$raw_n3fb<*0*> main_mem$_n3ff$raw_n51c<*0*> _n3e4 main_mem$_n3e4$raw_n522<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem$_n3e7$raw_n3fb<*1*> main_mem$_n3ff$raw_n51c<*1*> _n3e4 main_mem$_n3e4$raw_n522<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n3e4$raw_n525 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n3e7$raw_n3fe arbiter_state$_n3ff$raw_n50e _n3e4 arbiter_state$_n3e4$raw_n525 - - 0 =arbiter_state$_n3ff$raw_n50e - - 1 =arbiter_state$_n3e7$raw_n3fe .names cache_Wlist1<*0*> cache_Wlist1$_n3ff$raw_n50f<*0*> _n3e4 cache_Wlist1$_n3e4$raw_n529<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1<*1*> cache_Wlist1$_n3ff$raw_n50f<*1*> _n3e4 cache_Wlist1$_n3e4$raw_n529<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*0*> cache_Wlist2$_n3ff$raw_n512<*0*> _n3e4 cache_Wlist2$_n3e4$raw_n52c<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*1*> cache_Wlist2$_n3ff$raw_n512<*1*> _n3e4 cache_Wlist2$_n3e4$raw_n52c<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2<*0*> cache_Rlist2$_n3ff$raw_n515<*0*> _n3e4 cache_Rlist2$_n3e4$raw_n52f<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2<*1*> cache_Rlist2$_n3ff$raw_n515<*1*> _n3e4 cache_Rlist2$_n3e4$raw_n52f<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1<*0*> cache_Rlist1$_n3ff$raw_n518<*0*> _n3e4 cache_Rlist1$_n3e4$raw_n532<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1<*1*> cache_Rlist1$_n3ff$raw_n518<*1*> _n3e4 cache_Rlist1$_n3e4$raw_n532<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n3e0$raw_n537 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n3e0_n3e3$true arbiter_state$_n3e4$raw_n525 _n3e0 arbiter_state$_n3e0$raw_n537 - - 0 =arbiter_state$_n3e4$raw_n525 - - 1 =arbiter_state$_n3e0_n3e3$true .names main_mem<*0*> main_mem$_n3e4$raw_n522<*0*> _n3e0 main_mem$_n3e0$raw_n539<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem<*1*> main_mem$_n3e4$raw_n522<*1*> _n3e0 main_mem$_n3e0$raw_n539<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1<*0*> cache_Wlist1$_n3e4$raw_n529<*0*> _n3e0 cache_Wlist1$_n3e0$raw_n53c<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1<*1*> cache_Wlist1$_n3e4$raw_n529<*1*> _n3e0 cache_Wlist1$_n3e0$raw_n53c<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*0*> cache_Wlist2$_n3e4$raw_n52c<*0*> _n3e0 cache_Wlist2$_n3e0$raw_n53f<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2<*1*> cache_Wlist2$_n3e4$raw_n52c<*1*> _n3e0 cache_Wlist2$_n3e0$raw_n53f<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2<*0*> cache_Rlist2$_n3e4$raw_n52f<*0*> _n3e0 cache_Rlist2$_n3e0$raw_n542<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2<*1*> cache_Rlist2$_n3e4$raw_n52f<*1*> _n3e0 cache_Rlist2$_n3e0$raw_n542<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1<*0*> cache_Rlist1$_n3e4$raw_n532<*0*> _n3e0 cache_Rlist1$_n3e0$raw_n545<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1<*1*> cache_Rlist1$_n3e4$raw_n532<*1*> _n3e0 cache_Rlist1$_n3e0$raw_n545<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n30b$raw_n3c9<*0*> cache_Wlist1$_n3e0$raw_n53c<*0*> _n308 cache_Wlist1$_n308$raw_n54e<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist1$_n30b$raw_n3c9<*1*> cache_Wlist1$_n3e0$raw_n53c<*1*> _n308 cache_Wlist1$_n308$raw_n54e<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n30b$raw_n3cc<*0*> cache_Wlist2$_n3e0$raw_n53f<*0*> _n308 cache_Wlist2$_n308$raw_n551<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Wlist2$_n30b$raw_n3cc<*1*> cache_Wlist2$_n3e0$raw_n53f<*1*> _n308 cache_Wlist2$_n308$raw_n551<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30b$raw_n3cf<*0*> cache_Rlist2$_n3e0$raw_n542<*0*> _n308 cache_Rlist2$_n308$raw_n554<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist2$_n30b$raw_n3cf<*1*> cache_Rlist2$_n3e0$raw_n542<*1*> _n308 cache_Rlist2$_n308$raw_n554<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n30b$raw_n3d2<*0*> cache_Rlist1$_n3e0$raw_n545<*0*> _n308 cache_Rlist1$_n308$raw_n557<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names cache_Rlist1$_n30b$raw_n3d2<*1*> cache_Rlist1$_n3e0$raw_n545<*1*> _n308 cache_Rlist1$_n308$raw_n557<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .mv arbiter_state$_n308$raw_n55a 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names arbiter_state$_n30b$raw_n3d5 arbiter_state$_n3e0$raw_n537 _n308 arbiter_state$_n308$raw_n55a - - 0 =arbiter_state$_n3e0$raw_n537 - - 1 =arbiter_state$_n30b$raw_n3d5 .names main_mem<*0*> main_mem$_n3e0$raw_n539<*0*> _n308 main_mem$_n308$raw_n560<*0*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 .names main_mem<*1*> main_mem$_n3e0$raw_n539<*1*> _n308 main_mem$_n308$raw_n560<*1*> 0 - 1 0 1 - 1 1 - 0 0 0 - 1 0 1 # conflict arbitrators .names blk_ok2$raw_n2f1 blk_ok2 0 0 1 1 .names _n308 _n3e0 _n3e4 _n3e9 _n3ff _n4d7 _n4db _n4e0 _n568 .def 0 0 0 1 1 - - - - 1 0 0 0 - 0 0 1 1 1 .names _n568 main_mem$_n308$raw_n560<*0*> main_mem<*0*> _n569<*0*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n568 main_mem$_n308$raw_n560<*1*> main_mem<*1*> _n569<*1*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names write_back_req2$raw_n2d4 write_back_req2 0 0 1 1 .names blk_ok1$raw_n2ea blk_ok1 0 0 1 1 .names write_back_req1$raw_n2ca write_back_req1 0 0 1 1 .names inval2$raw_n2c0 inval2 0 0 1 1 .names blk_data$raw_n2de blk_data 0 0 1 1 .names inval1$raw_n2b6 inval1 0 0 1 1 .names _n308 _n30d _n313 _n379 _n3e0 _n3e4 _n3ff _n404 _n40a _n470 _n56a .def 0 1 1 0 - - - - - - - 1 1 1 0 - - - - - - - 1 1 0 - 1 - - - - - - 1 0 - - - 0 0 1 1 1 - 1 0 - - - 0 0 1 0 - 1 1 .names _n56a cache_Wlist1$_n308$raw_n54e<*0*> cache_Wlist1<*0*> _n56b<*0*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n56a cache_Wlist1$_n308$raw_n54e<*1*> cache_Wlist1<*1*> _n56b<*1*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n308 _n30d _n313 _n379 _n3e0 _n3e4 _n3ff _n404 _n40a _n470 _n56c .def 0 1 1 1 - - - - - - - 1 1 0 - 1 - - - - - - 1 0 - - - 0 0 1 1 0 - 1 0 - - - 0 0 1 1 0 - 1 0 - - - 0 0 1 0 - 1 1 .names _n56c cache_Wlist2$_n308$raw_n551<*0*> cache_Wlist2<*0*> _n56d<*0*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n56c cache_Wlist2$_n308$raw_n551<*1*> cache_Wlist2<*1*> _n56d<*1*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n308 _n30d _n313 _n379 _n3e0 _n3e4 _n3ff _n404 _n40a _n470 _n56e .def 0 1 1 1 - - - - - - - 1 1 0 - 1 - - - - - - 1 0 - - - 0 0 1 1 1 - 1 0 - - - 0 0 1 1 0 - 1 0 - - - 0 0 1 0 - 1 1 .names _n56e cache_Rlist2$_n308$raw_n554<*0*> cache_Rlist2<*0*> _n56f<*0*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n56e cache_Rlist2$_n308$raw_n554<*1*> cache_Rlist2<*1*> _n56f<*1*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names blocknum$raw_n2f8<0> blocknum<0> - =blocknum$raw_n2f8<0> .names _n308 _n30d _n313 _n379 _n3e0 _n3e4 _n3ff _n404 _n40a _n470 _n570 .def 0 1 1 1 - - - - - - - 1 1 1 0 - - - - - - - 1 1 0 - 1 - - - - - - 1 0 - - - 0 0 1 1 1 - 1 0 - - - 0 0 1 0 - 1 1 .names _n570 cache_Rlist1$_n308$raw_n557<*0*> cache_Rlist1<*0*> _n571<*0*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n570 cache_Rlist1$_n308$raw_n557<*1*> cache_Rlist1<*1*> _n571<*1*> 1 0 - 0 1 1 - 1 0 - 0 0 0 - 1 1 .names _n308 _n30d _n313 _n379 _n3e0 _n3e4 _n3e9 _n3ff _n404 _n40a _n470 _n4d7 _n4db _n4e0 _n572 .def 0 1 1 1 - - - - - - - - - - - 1 1 1 0 - - - - - - - - - - - 1 1 0 - 1 - - - - - - - - - - 1 1 0 - 0 - - - - - - - - - - 1 0 - - - 1 - - - - - - - - - 1 0 - - - 0 1 1 - - - - - - - 1 0 - - - 0 0 - 1 1 1 - - - - 1 0 - - - 0 0 - 1 1 0 - - - - 1 0 - - - 0 0 - 1 0 - 1 - - - 1 0 - - - 0 0 - 1 0 - 0 - - - 1 0 - - - 0 0 - 0 - - - 1 - - 1 0 - - - 0 0 - 0 - - - 0 1 1 1 .mv _n573 6 ONE ONEWAIT TWO TWOWAIT ONESERVE TWOSERVE .names _n572 arbiter_state$_n308$raw_n55a arbiter_state _n573 1 - - =arbiter_state$_n308$raw_n55a 0 - - =arbiter_state # non-blocking assignments # latches .r main_mem$raw_n275<*0*> main_mem<*0*> .def 0 1 1 .r main_mem$raw_n275<*1*> main_mem<*1*> .def 0 1 1 .latch _n569<*0*> main_mem<*0*> .latch _n569<*1*> main_mem<*1*> .r cache_Wlist1$raw_n29c<*0*> cache_Wlist1<*0*> .def 0 1 1 .r cache_Wlist1$raw_n29c<*1*> cache_Wlist1<*1*> .def 0 1 1 .latch _n56b<*0*> cache_Wlist1<*0*> .latch _n56b<*1*> cache_Wlist1<*1*> .r cache_Wlist2$raw_n2a9<*0*> cache_Wlist2<*0*> .def 0 1 1 .r cache_Wlist2$raw_n2a9<*1*> cache_Wlist2<*1*> .def 0 1 1 .latch _n56d<*0*> cache_Wlist2<*0*> .latch _n56d<*1*> cache_Wlist2<*1*> .r cache_Rlist2$raw_n28f<*0*> cache_Rlist2<*0*> .def 0 1 1 .r cache_Rlist2$raw_n28f<*1*> cache_Rlist2<*1*> .def 0 1 1 .latch _n56f<*0*> cache_Rlist2<*0*> .latch _n56f<*1*> cache_Rlist2<*1*> .r cache_Rlist1$raw_n282<*0*> cache_Rlist1<*0*> .def 0 1 1 .r cache_Rlist1$raw_n282<*1*> cache_Rlist1<*1*> .def 0 1 1 .latch _n571<*0*> cache_Rlist1<*0*> .latch _n571<*1*> cache_Rlist1<*1*> .r arbiter_state$raw_n229 arbiter_state - =arbiter_state$raw_n229 .latch _n573 arbiter_state # quasi-continuous assignment .end