hub.com/YosysHQ/yosys</title>
<meta name='generator' content='cgit v1.2.3'/>
<meta name='robots' content='index, nofollow'/>
<link rel='stylesheet' type='text/css' href='/cgit.css'/>
<link rel='shortcut icon' href='/favicon.ico'/>
<link rel='alternate' title='Atom feed' href='http://git.panaceas.org/cgit/iCE40/yosys/atom/manual/APPNOTE_011_Design_Investigation.tex?h=master' type='application/atom+xml'/>
<link rel='vcs-git' href='git://git.panaceas.org/iCE40/yosys' title='iCE40/yosys Git repository'/>
<link rel='vcs-git' href='ssh://git@git.panaceas.org/git/iCE40/yosys' title='iCE40/yosys Git repository'/>
</head>
<body>
<div id='cgit'><table id='header'>
<tr>
<td class='logo' rowspan='2'><a href='/cgit/'><img src='/cgit.png' alt='cgit logo'/></a></td>
<td class='main'><a href='/cgit/'>index</a> : <a title='iCE40/yosys' href='/cgit/iCE40/yosys/'>iCE40/yosys</a></td><td class='form'><form method='get'>
<input type='hidden' name='id' value='85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'/><select name='h' onchange='this.form.submit();'>
<option value='master' selected='selected'>master</option>
</select> <input type='submit' value='switch'/></form></td></tr>
<tr><td class='sub'>clone of https://github.com/YosysHQ/yosys</td><td class='sub right'></td></tr></table>
<table class='tabs'><tr><td>
<a href='/cgit/iCE40/yosys/about/'>about</a><a href='/cgit/iCE40/yosys/'>summary</a><a href='/cgit/iCE40/yosys/refs/?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>refs</a><a href='/cgit/iCE40/yosys/log/manual/APPNOTE_011_Design_Investigation.tex'>log</a><a class='active' href='/cgit/iCE40/yosys/tree/manual/APPNOTE_011_Design_Investigation.tex?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>tree</a><a href='/cgit/iCE40/yosys/commit/manual/APPNOTE_011_Design_Investigation.tex?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>commit</a><a href='/cgit/iCE40/yosys/diff/manual/APPNOTE_011_Design_Investigation.tex?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>diff</a><a href='/cgit/iCE40/yosys/stats/manual/APPNOTE_011_Design_Investigation.tex'>stats</a></td><td class='form'><form class='right' method='get' action='/cgit/iCE40/yosys/log/manual/APPNOTE_011_Design_Investigation.tex'>
<input type='hidden' name='id' value='85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'/><select name='qt'>
<option value='grep'>log msg</option>
<option value='author'>author</option>
<option value='committer'>committer</option>
<option value='range'>range</option>
</select>
<input class='txt' type='search' size='10' name='q' value=''/>
<input type='submit' value='search'/>
</form>
</td></tr></table>
<div class='path'>path: <a href='/cgit/iCE40/yosys/tree/?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>root</a>/<a href='/cgit/iCE40/yosys/tree/manual?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>manual</a>/<a href='/cgit/iCE40/yosys/tree/manual/APPNOTE_011_Design_Investigation.tex?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>APPNOTE_011_Design_Investigation.tex</a></div><div class='content'>blob: 9780c78336cde92a2a3e91832d68157dd08fe8cc (<a href='/cgit/iCE40/yosys/plain/manual/APPNOTE_011_Design_Investigation.tex?id=85f1c2dcbe1ebd3fa609f2a9a558810dfcc8484c'>plain</a>)
<table summary='blob content' class='blob'>
<tr><td class='linenumbers'><pre><a id='n1' href='#n1'>1</a>
<a id='n2' href='#n2'>2</a>
<a id='n3' href='#n3'>3</a>
<a id='n4' href='#n4'>4</a>
<a id='n5' href='#n5'>5</a>
<a id='n6' href='#n6'>6</a>
<a id='n7' href='#n7'>7</a>
<a id='n8' href='#n8'>8</a>
<a id='n9' href='#n9'>9</a>
<a id='n10' href='#n10'>10</a>
<a id='n11' href='#n11'>11</a>
<a id='n12' href='#n12'>12</a>
<a id='n13' href='#n13'>13</a>
<a id='n14' href='#n14'>14</a>
<a id='n15' href='#n15'>15</a>
<a id='n16' href='#n16'>16</a>
<a id='n17' href='#n17'>17</a>
<a id='n18' href='#n18'>18</a>
<a id='n19' href='#n19'>19</a>
<a id='n20' href='#n20'>20</a>
<a id='n21' href='#n21'>21</a>
<a id='n22' href='#n22'>22</a>
<a id='n23' href='#n23'>23</a>
<a id='n24' href='#n24'>24</a>
<a id='n25' href='#n25'>25</a>
<a id='n26' href='#n26'>26</a>
<a id='n27' href='#n27'>27</a>
<a id='n28' href='#n28'>28</a>
<a id='n29' href='#n29'>29</a>
<a id='n30' href='#n30'>30</a>
<a id='n31' href='#n31'>31</a>
<a id='n32' href='#n32'>32</a>
<a id='n33' href='#n33'>33</a>
<a id='n34' href='#n34'>34</a>
<a id='n35' href='#n35'>35</a>
<a id='n36' href='#n36'>36</a>
<a id='n37' href='#n37'>37</a>
<a id='n38' href='#n38'>38</a>
<a id='n39' href='#n39'>39</a>
<a id='n40' href='#n40'>40</a>
<a id='n41' href='#n41'>41</a>
<a id='n42' href='#n42'>42</a>
<a id='n43' href='#n43'>43</a>
<a id='n44' href='#n44'>44</a>
<a id='n45' href='#n45'>45</a>
<a id='n46' href='#n46'>46</a>
<a id='n47' href='#n47'>47</a>
<a id='n48' href='#n48'>48</a>
<a id='n49' href='#n49'>49</a>
<a id='n50' href='#n50'>50</a>
<a id='n51' href='#n51'>51</a>
<a id='n52' href='#n52'>52</a>
<a id='n53' href='#n53'>53</a>
<a id='n54' href='#n54'>54</a>
<a id='n55' href='#n55'>55</a>
<a id='n56' href='#n56'>56</a>
<a id='n57' href='#n57'>57</a>
<a id='n58' href='#n58'>58</a>
<a id='n59' href='#n59'>59</a>
<a id='n60' href='#n60'>60</a>
<a id='n61' href='#n61'>61</a>
<a id='n62' href='#n62'>62</a>
<a id='n63' href='#n63'>63</a>
<a id='n64' href='#n64'>64</a>
<a id='n65' href='#n65'>65</a>
<a id='n66' href='#n66'>66</a>
<a id='n67' href='#n67'>67</a>
<a id='n68' href='#n68'>68</a>
<a id='n69' href='#n69'>69</a>
<a id='n70' href='#n70'>70</a>
<a id='n71' href='#n71'>71</a>
<a id='n72' href='#n72'>72</a>
<a id='n73' href='#n73'>73</a>
<a id='n74' href='#n74'>74</a>
<a id='n75' href='#n75'>75</a>
<a id='n76' href='#n76'>76</a>
<a id='n77' href='#n77'>77</a>
<a id='n78' href='#n78'>78</a>
<a id='n79' href='#n79'>79</a>
<a id='n80' href='#n80'>80</a>
<a id='n81' href='#n81'>81</a>
<a id='n82' href='#n82'>82</a>
<a id='n83' href='#n83'>83</a>
<a id='n84' href='#n84'>84</a>
<a id='n85' href='#n85'>85</a>
<a id='n86' href='#n86'>86</a>
<a id='n87' href='#n87'>87</a>
<a id='n88' href='#n88'>88</a>
<a id='n89' href='#n89'>89</a>
<a id='n90' href='#n90'>90</a>
<a id='n91' href='#n91'>91</a>
<a id='n92' href='#n92'>92</a>
<a id='n93' href='#n93'>93</a>
<a id='n94' href='#n94'>94</a>
<a id='n95' href='#n95'>95</a>
<a id='n96' href='#n96'>96</a>
<a id='n97' href='#n97'>97</a>
<a id='n98' href='#n98'>98</a>
<a id='n99' href='#n99'>99</a>
<a id='n100' href='#n100'>100</a>
<a id='n101' href='#n101'>101</a>
<a id='n102' href='#n102'>102</a>
<a id='n103' href='#n103'>103</a>
<a id='n104' href='#n104'>104</a>
<a id='n105' href='#n105'>105</a>
<a id='n106' href='#n106'>106</a>
<a id='n107' href='#n107'>107</a>
<a id='n108' href='#n108'>108</a>
<a id='n109' href='#n109'>109</a>
<a id='n110' href='#n110'>110</a>
<a id='n111' href='#n111'>111</a>
<a id='n112' href='#n112'>112</a>
<a id='n113' href='#n113'>113</a>
<a id='n114' href='#n114'>114</a>
<a id='n115' href='#n115'>115</a>
<a id='n116' href='#n116'>116</a>
<a id='n117' href='#n117'>117</a>
<a id='n118' href='#n118'>118</a>
<a id='n119' href='#n119'>119</a>
<a id='n120' href='#n120'>120</a>
<a id='n121' href='#n121'>121</a>
<a id='n122' href='#n122'>122</a>
<a id='n123' href='#n123'>123</a>
<a id='n124' href='#n124'>124</a>
<a id='n125' href='#n125'>125</a>
<a id='n126' href='#n126'>126</a>
<a id='n127' href='#n127'>127</a>
<a id='n128' href='#n128'>128</a>
<a id='n129' href='#n129'>129</a>
<a id='n130' href='#n130'>130</a>
<a id='n131' href='#n131'>131</a>
<a id='n132' href='#n132'>132</a>
<a id='n133' href='#n133'>133</a>
<a id='n134' href='#n134'>134</a>
<a id='n135' href='#n135'>135</a>
<a id='n136' href='#n136'>136</a>
<a id='n137' href='#n137'>137</a>
<a id='n138' href='#n138'>138</a>
<a id='n139' href='#n139'>139</a>
<a id='n140' href='#n140'>140</a>
<a id='n141' href='#n141'>141</a>
<a id='n142' href='#n142'>142</a>
<a id='n143' href='#n143'>143</a>
<a id='n144' href='#n144'>144</a>
<a id='n145' href='#n145'>145</a>
<a id='n146' href='#n146'>146</a>
<a id='n147' href='#n147'>147</a>
<a id='n148' href='#n148'>148</a>
<a id='n149' href='#n149'>149</a>
<a id='n150' href='#n150'>150</a>
<a id='n151' href='#n151'>151</a>
<a id='n152' href='#n152'>152</a>
<a id='n153' href='#n153'>153</a>
<a id='n154' href='#n154'>154</a>
<a id='n155' href='#n155'>155</a>
<a id='n156' href='#n156'>156</a>
<a id='n157' href='#n157'>157</a>
<a id='n158' href='#n158'>158</a>
<a id='n159' href='#n159'>159</a>
<a id='n160' href='#n160'>160</a>
<a id='n161' href='#n161'>161</a>
<a id='n162' href='#n162'>162</a>
<a id='n163' href='#n163'>163</a>
<a id='n164' href='#n164'>164</a>
<a id='n165' href='#n165'>165</a>
<a id='n166' href='#n166'>166</a>
<a id='n167' href='#n167'>167</a>
<a id='n168' href='#n168'>168</a>
<a id='n169' href='#n169'>169</a>
<a id='n170' href='#n170'>170</a>
<a id='n171' href='#n171'>171</a>
<a id='n172' href='#n172'>172</a>
<a id='n173' href='#n173'>173</a>
<a id='n174' href='#n174'>174</a>
<a id='n175' href='#n175'>175</a>
<a id='n176' href='#n176'>176</a>
<a id='n177' href='#n177'>177</a>
<a id='n178' href='#n178'>178</a>
<a id='n179' href='#n179'>179</a>
<a id='n180' href='#n180'>180</a>
<a id='n181' href='#n181'>181</a>
<a id='n182' href='#n182'>182</a>
<a id='n183' href='#n183'>183</a>
<a id='n184' href='#n184'>184</a>
<a id='n185' href='#n185'>185</a>
<a id='n186' href='#n186'>186</a>
<a id='n187' href='#n187'>187</a>
<a id='n188' href='#n188'>188</a>
<a id='n189' href='#n189'>189</a>
<a id='n190' href='#n190'>190</a>
<a id='n191' href='#n191'>191</a>
<a id='n192' href='#n192'>192</a>
<a id='n193' href='#n193'>193</a>
<a id='n194' href='#n194'>194</a>
<a id='n195' href='#n195'>195</a>
<a id='n196' href='#n196'>196</a>
<a id='n197' href='#n197'>197</a>
<a id='n198' href='#n198'>198</a>
<a id='n199' href='#n199'>199</a>
<a id='n200' href='#n200'>200</a>
<a id='n201' href='#n201'>201</a>
<a id='n202' href='#n202'>202</a>
<a id='n203' href='#n203'>203</a>
<a id='n204' href='#n204'>204</a>
<a id='n205' href='#n205'>205</a>
<a id='n206' href='#n206'>206</a>
<a id='n207' href='#n207'>207</a>
<a id='n208' href='#n208'>208</a>
<a id='n209' href='#n209'>209</a>
<a id='n210' href='#n210'>210</a>
<a id='n211' href='#n211'>211</a>
<a id='n212' href='#n212'>212</a>
<a id='n213' href='#n213'>213</a>
<a id='n214' href='#n214'>214</a>
<a id='n215' href='#n215'>215</a>
<a id='n216' href='#n216'>216</a>
<a id='n217' href='#n217'>217</a>
<a id='n218' href='#n218'>218</a>
<a id='n219' href='#n219'>219</a>
<a id='n220' href='#n220'>220</a>
<a id='n221' href='#n221'>221</a>
<a id='n222' href='#n222'>222</a>
<a id='n223' href='#n223'>223</a>
<a id='n224' href='#n224'>224</a>
<a id='n225' href='#n225'>225</a>
<a id='n226' href='#n226'>226</a>
<a id='n227' href='#n227'>227</a>
<a id='n228' href='#n228'>228</a>
<a id='n229' href='#n229'>229</a>
<a id='n230' href='#n230'>230</a>
<a id='n231' href='#n231'>231</a>
<a id='n232' href='#n232'>232</a>
<a id='n233' href='#n233'>233</a>
<a id='n234' href='#n234'>234</a>
<a id='n235' href='#n235'>235</a>
<a id='n236' href='#n236'>236</a>
<a id='n237' href='#n237'>237</a>
<a id='n238' href='#n238'>238</a>
<a id='n239' href='#n239'>239</a>
<a id='n240' href='#n240'>240</a>
<a id='n241' href='#n241'>241</a>
<a id='n242' href='#n242'>242</a>
<a id='n243' href='#n243'>243</a>
<a id='n244' href='#n244'>244</a>
<a id='n245' href='#n245'>245</a>
<a id='n246' href='#n246'>246</a>
<a id='n247' href='#n247'>247</a>
<a id='n248' href='#n248'>248</a>
<a id='n249' href='#n249'>249</a>
<a id='n250' href='#n250'>250</a>
<a id='n251' href='#n251'>251</a>
<a id='n252' href='#n252'>252</a>
<a id='n253' href='#n253'>253</a>
<a id='n254' href='#n254'>254</a>
<a id='n255' href='#n255'>255</a>
<a id='n256' href='#n256'>256</a>
<a id='n257' href='#n257'>257</a>
<a id='n258' href='#n258'>258</a>
<a id='n259' href='#n259'>259</a>
<a id='n260' href='#n260'>260</a>
<a id='n261' href='#n261'>261</a>
<a id='n262' href='#n262'>262</a>
<a id='n263' href='#n263'>263</a>
<a id='n264' href='#n264'>264</a>
<a id='n265' href='#n265'>265</a>
<a id='n266' href='#n266'>266</a>
<a id='n267' href='#n267'>267</a>
<a id='n268' href='#n268'>268</a>
<a id='n269' href='#n269'>269</a>
<a id='n270' href='#n270'>270</a>
<a id='n271' href='#n271'>271</a>
<a id='n272' href='#n272'>272</a>
<a id='n273' href='#n273'>273</a>
<a id='n274' href='#n274'>274</a>
<a id='n275' href='#n275'>275</a>
<a id='n276' href='#n276'>276</a>
<a id='n277' href='#n277'>277</a>
<a id='n278' href='#n278'>278</a>
<a id='n279' href='#n279'>279</a>
<a id='n280' href='#n280'>280</a>
<a id='n281' href='#n281'>281</a>
<a id='n282' href='#n282'>282</a>
<a id='n283' href='#n283'>283</a>
<a id='n284' href='#n284'>284</a>
<a id='n285' href='#n285'>285</a>
<a id='n286' href='#n286'>286</a>
<a id='n287' href='#n287'>287</a>
<a id='n288' href='#n288'>288</a>
<a id='n289' href='#n289'>289</a>
<a id='n290' href='#n290'>290</a>
<a id='n291' href='#n291'>291</a>
<a id='n292' href='#n292'>292</a>
<a id='n293' href='#n293'>293</a>
<a id='n294' href='#n294'>294</a>
<a id='n295' href='#n295'>295</a>
<a id='n296' href='#n296'>296</a>
<a id='n297' href='#n297'>297</a>
<a id='n298' href='#n298'>298</a>
<a id='n299' href='#n299'>299</a>
<a id='n300' href='#n300'>300</a>
<a id='n301' href='#n301'>301</a>
<a id='n302' href='#n302'>302</a>
<a id='n303' href='#n303'>303</a>
<a id='n304' href='#n304'>304</a>
<a id='n305' href='#n305'>305</a>
<a id='n306' href='#n306'>306</a>
<a id='n307' href='#n307'>307</a>
<a id='n308' href='#n308'>308</a>
<a id='n309' href='#n309'>309</a>
<a id='n310' href='#n310'>310</a>
<a id='n311' href='#n311'>311</a>
<a id='n312' href='#n312'>312</a>
<a id='n313' href='#n313'>313</a>
<a id='n314' href='#n314'>314</a>
<a id='n315' href='#n315'>315</a>
<a id='n316' href='#n316'>316</a>
<a id='n317' href='#n317'>317</a>
<a id='n318' href='#n318'>318</a>
<a id='n319' href='#n319'>319</a>
<a id='n320' href='#n320'>320</a>
<a id='n321' href='#n321'>321</a>
<a id='n322' href='#n322'>322</a>
<a id='n323' href='#n323'>323</a>
<a id='n324' href='#n324'>324</a>
<a id='n325' href='#n325'>325</a>
<a id='n326' href='#n326'>326</a>
<a id='n327' href='#n327'>327</a>
<a id='n328' href='#n328'>328</a>
<a id='n329' href='#n329'>329</a>
<a id='n330' href='#n330'>330</a>
<a id='n331' href='#n331'>331</a>
<a id='n332' href='#n332'>332</a>
<a id='n333' href='#n333'>333</a>
<a id='n334' href='#n334'>334</a>
<a id='n335' href='#n335'>335</a>
<a id='n336' href='#n336'>336</a>
<a id='n337' href='#n337'>337</a>
<a id='n338' href='#n338'>338</a>
<a id='n339' href='#n339'>339</a>
<a id='n340' href='#n340'>340</a>
<a id='n341' href='#n341'>341</a>
<a id='n342' href='#n342'>342</a>
<a id='n343' href='#n343'>343</a>
<a id='n344' href='#n344'>344</a>
<a id='n345' href='#n345'>345</a>
<a id='n346' href='#n346'>346</a>
<a id='n347' href='#n347'>347</a>
<a id='n348' href='#n348'>348</a>
<a id='n349' href='#n349'>349</a>
<a id='n350' href='#n350'>350</a>
<a id='n351' href='#n351'>351</a>
<a id='n352' href='#n352'>352</a>
<a id='n353' href='#n353'>353</a>
<a id='n354' href='#n354'>354</a>
<a id='n355' href='#n355'>355</a>
<a id='n356' href='#n356'>356</a>
<a id='n357' href='#n357'>357</a>
<a id='n358' href='#n358'>358</a>
<a id='n359' href='#n359'>359</a>
<a id='n360' href='#n360'>360</a>
<a id='n361' href='#n361'>361</a>
<a id='n362' href='#n362'>362</a>
<a id='n363' href='#n363'>363</a>
<a id='n364' href='#n364'>364</a>
<a id='n365' href='#n365'>365</a>
<a id='n366' href='#n366'>366</a>
<a id='n367' href='#n367'>367</a>
<a id='n368' href='#n368'>368</a>
<a id='n369' href='#n369'>369</a>
<a id='n370' href='#n370'>370</a>
<a id='n371' href='#n371'>371</a>
<a id='n372' href='#n372'>372</a>
<a id='n373' href='#n373'>373</a>
<a id='n374' href='#n374'>374</a>
<a id='n375' href='#n375'>375</a>
<a id='n376' href='#n376'>376</a>
<a id='n377' href='#n377'>377</a>
<a id='n378' href='#n378'>378</a>
<a id='n379' href='#n379'>379</a>
<a id='n380' href='#n380'>380</a>
<a id='n381' href='#n381'>381</a>
<a id='n382' href='#n382'>382</a>
<a id='n383' href='#n383'>383</a>
<a id='n384' href='#n384'>384</a>
<a id='n385' href='#n385'>385</a>
<a id='n386' href='#n386'>386</a>
<a id='n387' href='#n387'>387</a>
<a id='n388' href='#n388'>388</a>
<a id='n389' href='#n389'>389</a>
<a id='n390' href='#n390'>390</a>
<a id='n391' href='#n391'>391</a>
<a id='n392' href='#n392'>392</a>
<a id='n393' href='#n393'>393</a>
<a id='n394' href='#n394'>394</a>
<a id='n395' href='#n395'>395</a>
<a id='n396' href='#n396'>396</a>
<a id='n397' href='#n397'>397</a>
<a id='n398' href='#n398'>398</a>
<a id='n399' href='#n399'>399</a>
<a id='n400' href='#n400'>400</a>
<a id='n401' href='#n401'>401</a>
<a id='n402' href='#n402'>402</a>
<a id='n403' href='#n403'>403</a>
<a id='n404' href='#n404'>404</a>
<a id='n405' href='#n405'>405</a>
<a id='n406' href='#n406'>406</a>
<a id='n407' href='#n407'>407</a>
<a id='n408' href='#n408'>408</a>
<a id='n409' href='#n409'>409</a>
<a id='n410' href='#n410'>410</a>
<a id='n411' href='#n411'>411</a>
<a id='n412' href='#n412'>412</a>
<a id='n413' href='#n413'>413</a>
<a id='n414' href='#n414'>414</a>
<a id='n415' href='#n415'>415</a>
<a id='n416' href='#n416'>416</a>
<a id='n417' href='#n417'>417</a>
<a id='n418' href='#n418'>418</a>
<a id='n419' href='#n419'>419</a>
<a id='n420' href='#n420'>420</a>
<a id='n421' href='#n421'>421</a>
<a id='n422' href='#n422'>422</a>
<a id='n423' href='#n423'>423</a>
<a id='n424' href='#n424'>424</a>
<a id='n425' href='#n425'>425</a>
<a id='n426' href='#n426'>426</a>
<a id='n427' href='#n427'>427</a>
<a id='n428' href='#n428'>428</a>
<a id='n429' href='#n429'>429</a>
<a id='n430' href='#n430'>430</a>
<a id='n431' href='#n431'>431</a>
<a id='n432' href='#n432'>432</a>
<a id='n433' href='#n433'>433</a>
<a id='n434' href='#n434'>434</a>
<a id='n435' href='#n435'>435</a>
<a id='n436' href='#n436'>436</a>
<a id='n437' href='#n437'>437</a>
<a id='n438' href='#n438'>438</a>
<a id='n439' href='#n439'>439</a>
<a id='n440' href='#n440'>440</a>
<a id='n441' href='#n441'>441</a>
<a id='n442' href='#n442'>442</a>
<a id='n443' href='#n443'>443</a>
<a id='n444' href='#n444'>444</a>
<a id='n445' href='#n445'>445</a>
<a id='n446' href='#n446'>446</a>
<a id='n447' href='#n447'>447</a>
<a id='n448' href='#n448'>448</a>
<a id='n449' href='#n449'>449</a>
<a id='n450' href='#n450'>450</a>
<a id='n451' href='#n451'>451</a>
<a id='n452' href='#n452'>452</a>
<a id='n453' href='#n453'>453</a>
<a id='n454' href='#n454'>454</a>
<a id='n455' href='#n455'>455</a>
<a id='n456' href='#n456'>456</a>
<a id='n457' href='#n457'>457</a>
<a id='n458' href='#n458'>458</a>
<a id='n459' href='#n459'>459</a>
<a id='n460' href='#n460'>460</a>
<a id='n461' href='#n461'>461</a>
<a id='n462' href='#n462'>462</a>
<a id='n463' href='#n463'>463</a>
<a id='n464' href='#n464'>464</a>
<a id='n465' href='#n465'>465</a>
<a id='n466' href='#n466'>466</a>
<a id='n467' href='#n467'>467</a>
<a id='n468' href='#n468'>468</a>
<a id='n469' href='#n469'>469</a>
<a id='n470' href='#n470'>470</a>
<a id='n471' href='#n471'>471</a>
<a id='n472' href='#n472'>472</a>
<a id='n473' href='#n473'>473</a>
<a id='n474' href='#n474'>474</a>
<a id='n475' href='#n475'>475</a>
<a id='n476' href='#n476'>476</a>
<a id='n477' href='#n477'>477</a>
<a id='n478' href='#n478'>478</a>
<a id='n479' href='#n479'>479</a>
<a id='n480' href='#n480'>480</a>
<a id='n481' href='#n481'>481</a>
<a id='n482' href='#n482'>482</a>
<a id='n483' href='#n483'>483</a>
<a id='n484' href='#n484'>484</a>
<a id='n485' href='#n485'>485</a>
<a id='n486' href='#n486'>486</a>
<a id='n487' href='#n487'>487</a>
<a id='n488' href='#n488'>488</a>
<a id='n489' href='#n489'>489</a>
<a id='n490' href='#n490'>490</a>
<a id='n491' href='#n491'>491</a>
<a id='n492' href='#n492'>492</a>
<a id='n493' href='#n493'>493</a>
<a id='n494' href='#n494'>494</a>
<a id='n495' href='#n495'>495</a>
<a id='n496' href='#n496'>496</a>
<a id='n497' href='#n497'>497</a>
<a id='n498' href='#n498'>498</a>
<a id='n499' href='#n499'>499</a>
<a id='n500' href='#n500'>500</a>
<a id='n501' href='#n501'>501</a>
<a id='n502' href='#n502'>502</a>
<a id='n503' href='#n503'>503</a>
<a id='n504' href='#n504'>504</a>
<a id='n505' href='#n505'>505</a>
<a id='n506' href='#n506'>506</a>
<a id='n507' href='#n507'>507</a>
<a id='n508' href='#n508'>508</a>
<a id='n509' href='#n509'>509</a>
<a id='n510' href='#n510'>510</a>
<a id='n511' href='#n511'>511</a>
<a id='n512' href='#n512'>512</a>
<a id='n513' href='#n513'>513</a>
<a id='n514' href='#n514'>514</a>
<a id='n515' href='#n515'>515</a>
<a id='n516' href='#n516'>516</a>
<a id='n517' href='#n517'>517</a>
<a id='n518' href='#n518'>518</a>
<a id='n519' href='#n519'>519</a>
<a id='n520' href='#n520'>520</a>
<a id='n521' href='#n521'>521</a>
<a id='n522' href='#n522'>522</a>
<a id='n523' href='#n523'>523</a>
<a id='n524' href='#n524'>524</a>
<a id='n525' href='#n525'>525</a>
<a id='n526' href='#n526'>526</a>
<a id='n527' href='#n527'>527</a>
<a id='n528' href='#n528'>528</a>
<a id='n529' href='#n529'>529</a>
<a id='n530' href='#n530'>530</a>
<a id='n531' href='#n531'>531</a>
<a id='n532' href='#n532'>532</a>
<a id='n533' href='#n533'>533</a>
<a id='n534' href='#n534'>534</a>
<a id='n535' href='#n535'>535</a>
<a id='n536' href='#n536'>536</a>
<a id='n537' href='#n537'>537</a>
<a id='n538' href='#n538'>538</a>
<a id='n539' href='#n539'>539</a>
<a id='n540' href='#n540'>540</a>
<a id='n541' href='#n541'>541</a>
<a id='n542' href='#n542'>542</a>
<a id='n543' href='#n543'>543</a>
<a id='n544' href='#n544'>544</a>
<a id='n545' href='#n545'>545</a>
<a id='n546' href='#n546'>546</a>
<a id='n547' href='#n547'>547</a>
<a id='n548' href='#n548'>548</a>
<a id='n549' href='#n549'>549</a>
<a id='n550' href='#n550'>550</a>
<a id='n551' href='#n551'>551</a>
<a id='n552' href='#n552'>552</a>
<a id='n553' href='#n553'>553</a>
<a id='n554' href='#n554'>554</a>
<a id='n555' href='#n555'>555</a>
<a id='n556' href='#n556'>556</a>
<a id='n557' href='#n557'>557</a>
<a id='n558' href='#n558'>558</a>
<a id='n559' href='#n559'>559</a>
<a id='n560' href='#n560'>560</a>
<a id='n561' href='#n561'>561</a>
<a id='n562' href='#n562'>562</a>
<a id='n563' href='#n563'>563</a>
<a id='n564' href='#n564'>564</a>
<a id='n565' href='#n565'>565</a>
<a id='n566' href='#n566'>566</a>
<a id='n567' href='#n567'>567</a>
<a id='n568' href='#n568'>568</a>
<a id='n569' href='#n569'>569</a>
<a id='n570' href='#n570'>570</a>
<a id='n571' href='#n571'>571</a>
<a id='n572' href='#n572'>572</a>
<a id='n573' href='#n573'>573</a>
<a id='n574' href='#n574'>574</a>
<a id='n575' href='#n575'>575</a>
<a id='n576' href='#n576'>576</a>
<a id='n577' href='#n577'>577</a>
<a id='n578' href='#n578'>578</a>
<a id='n579' href='#n579'>579</a>
<a id='n580' href='#n580'>580</a>
<a id='n581' href='#n581'>581</a>
<a id='n582' href='#n582'>582</a>
<a id='n583' href='#n583'>583</a>
<a id='n584' href='#n584'>584</a>
<a id='n585' href='#n585'>585</a>
<a id='n586' href='#n586'>586</a>
<a id='n587' href='#n587'>587</a>
<a id='n588' href='#n588'>588</a>
<a id='n589' href='#n589'>589</a>
<a id='n590' href='#n590'>590</a>
<a id='n591' href='#n591'>591</a>
<a id='n592' href='#n592'>592</a>
<a id='n593' href='#n593'>593</a>
<a id='n594' href='#n594'>594</a>
<a id='n595' href='#n595'>595</a>
<a id='n596' href='#n596'>596</a>
<a id='n597' href='#n597'>597</a>
<a id='n598' href='#n598'>598</a>
<a id='n599' href='#n599'>599</a>
<a id='n600' href='#n600'>600</a>
<a id='n601' href='#n601'>601</a>
<a id='n602' href='#n602'>602</a>
<a id='n603' href='#n603'>603</a>
<a id='n604' href='#n604'>604</a>
<a id='n605' href='#n605'>605</a>
<a id='n606' href='#n606'>606</a>
<a id='n607' href='#n607'>607</a>
<a id='n608' href='#n608'>608</a>
<a id='n609' href='#n609'>609</a>
<a id='n610' href='#n610'>610</a>
<a id='n611' href='#n611'>611</a>
<a id='n612' href='#n612'>612</a>
<a id='n613' href='#n613'>613</a>
<a id='n614' href='#n614'>614</a>
<a id='n615' href='#n615'>615</a>
<a id='n616' href='#n616'>616</a>
<a id='n617' href='#n617'>617</a>
<a id='n618' href='#n618'>618</a>
<a id='n619' href='#n619'>619</a>
<a id='n620' href='#n620'>620</a>
<a id='n621' href='#n621'>621</a>
<a id='n622' href='#n622'>622</a>
<a id='n623' href='#n623'>623</a>
<a id='n624' href='#n624'>624</a>
<a id='n625' href='#n625'>625</a>
<a id='n626' href='#n626'>626</a>
<a id='n627' href='#n627'>627</a>
<a id='n628' href='#n628'>628</a>
<a id='n629' href='#n629'>629</a>
<a id='n630' href='#n630'>630</a>
<a id='n631' href='#n631'>631</a>
<a id='n632' href='#n632'>632</a>
<a id='n633' href='#n633'>633</a>
<a id='n634' href='#n634'>634</a>
<a id='n635' href='#n635'>635</a>
<a id='n636' href='#n636'>636</a>
<a id='n637' href='#n637'>637</a>
<a id='n638' href='#n638'>638</a>
<a id='n639' href='#n639'>639</a>
<a id='n640' href='#n640'>640</a>
<a id='n641' href='#n641'>641</a>
<a id='n642' href='#n642'>642</a>
<a id='n643' href='#n643'>643</a>
<a id='n644' href='#n644'>644</a>
<a id='n645' href='#n645'>645</a>
<a id='n646' href='#n646'>646</a>
<a id='n647' href='#n647'>647</a>
<a id='n648' href='#n648'>648</a>
<a id='n649' href='#n649'>649</a>
<a id='n650' href='#n650'>650</a>
<a id='n651' href='#n651'>651</a>
<a id='n652' href='#n652'>652</a>
<a id='n653' href='#n653'>653</a>
<a id='n654' href='#n654'>654</a>
<a id='n655' href='#n655'>655</a>
<a id='n656' href='#n656'>656</a>
<a id='n657' href='#n657'>657</a>
<a id='n658' href='#n658'>658</a>
<a id='n659' href='#n659'>659</a>
<a id='n660' href='#n660'>660</a>
<a id='n661' href='#n661'>661</a>
<a id='n662' href='#n662'>662</a>
<a id='n663' href='#n663'>663</a>
<a id='n664' href='#n664'>664</a>
<a id='n665' href='#n665'>665</a>
<a id='n666' href='#n666'>666</a>
<a id='n667' href='#n667'>667</a>
<a id='n668' href='#n668'>668</a>
<a id='n669' href='#n669'>669</a>
<a id='n670' href='#n670'>670</a>
<a id='n671' href='#n671'>671</a>
<a id='n672' href='#n672'>672</a>
<a id='n673' href='#n673'>673</a>
<a id='n674' href='#n674'>674</a>
<a id='n675' href='#n675'>675</a>
<a id='n676' href='#n676'>676</a>
<a id='n677' href='#n677'>677</a>
<a id='n678' href='#n678'>678</a>
<a id='n679' href='#n679'>679</a>
<a id='n680' href='#n680'>680</a>
<a id='n681' href='#n681'>681</a>
<a id='n682' href='#n682'>682</a>
<a id='n683' href='#n683'>683</a>
<a id='n684' href='#n684'>684</a>
<a id='n685' href='#n685'>685</a>
<a id='n686' href='#n686'>686</a>
<a id='n687' href='#n687'>687</a>
<a id='n688' href='#n688'>688</a>
<a id='n689' href='#n689'>689</a>
<a id='n690' href='#n690'>690</a>
<a id='n691' href='#n691'>691</a>
<a id='n692' href='#n692'>692</a>
<a id='n693' href='#n693'>693</a>
<a id='n694' href='#n694'>694</a>
<a id='n695' href='#n695'>695</a>
<a id='n696' href='#n696'>696</a>
<a id='n697' href='#n697'>697</a>
<a id='n698' href='#n698'>698</a>
<a id='n699' href='#n699'>699</a>
<a id='n700' href='#n700'>700</a>
<a id='n701' href='#n701'>701</a>
<a id='n702' href='#n702'>702</a>
<a id='n703' href='#n703'>703</a>
<a id='n704' href='#n704'>704</a>
<a id='n705' href='#n705'>705</a>
<a id='n706' href='#n706'>706</a>
<a id='n707' href='#n707'>707</a>
<a id='n708' href='#n708'>708</a>
<a id='n709' href='#n709'>709</a>
<a id='n710' href='#n710'>710</a>
<a id='n711' href='#n711'>711</a>
<a id='n712' href='#n712'>712</a>
<a id='n713' href='#n713'>713</a>
<a id='n714' href='#n714'>714</a>
<a id='n715' href='#n715'>715</a>
<a id='n716' href='#n716'>716</a>
<a id='n717' href='#n717'>717</a>
<a id='n718' href='#n718'>718</a>
<a id='n719' href='#n719'>719</a>
<a id='n720' href='#n720'>720</a>
<a id='n721' href='#n721'>721</a>
<a id='n722' href='#n722'>722</a>
<a id='n723' href='#n723'>723</a>
<a id='n724' href='#n724'>724</a>
<a id='n725' href='#n725'>725</a>
<a id='n726' href='#n726'>726</a>
<a id='n727' href='#n727'>727</a>
<a id='n728' href='#n728'>728</a>
<a id='n729' href='#n729'>729</a>
<a id='n730' href='#n730'>730</a>
<a id='n731' href='#n731'>731</a>
<a id='n732' href='#n732'>732</a>
<a id='n733' href='#n733'>733</a>
<a id='n734' href='#n734'>734</a>
<a id='n735' href='#n735'>735</a>
<a id='n736' href='#n736'>736</a>
<a id='n737' href='#n737'>737</a>
<a id='n738' href='#n738'>738</a>
<a id='n739' href='#n739'>739</a>
<a id='n740' href='#n740'>740</a>
<a id='n741' href='#n741'>741</a>
<a id='n742' href='#n742'>742</a>
<a id='n743' href='#n743'>743</a>
<a id='n744' href='#n744'>744</a>
<a id='n745' href='#n745'>745</a>
<a id='n746' href='#n746'>746</a>
<a id='n747' href='#n747'>747</a>
<a id='n748' href='#n748'>748</a>
<a id='n749' href='#n749'>749</a>
<a id='n750' href='#n750'>750</a>
<a id='n751' href='#n751'>751</a>
<a id='n752' href='#n752'>752</a>
<a id='n753' href='#n753'>753</a>
<a id='n754' href='#n754'>754</a>
<a id='n755' href='#n755'>755</a>
<a id='n756' href='#n756'>756</a>
<a id='n757' href='#n757'>757</a>
<a id='n758' href='#n758'>758</a>
<a id='n759' href='#n759'>759</a>
<a id='n760' href='#n760'>760</a>
<a id='n761' href='#n761'>761</a>
<a id='n762' href='#n762'>762</a>
<a id='n763' href='#n763'>763</a>
<a id='n764' href='#n764'>764</a>
<a id='n765' href='#n765'>765</a>
<a id='n766' href='#n766'>766</a>
<a id='n767' href='#n767'>767</a>
<a id='n768' href='#n768'>768</a>
<a id='n769' href='#n769'>769</a>
<a id='n770' href='#n770'>770</a>
<a id='n771' href='#n771'>771</a>
<a id='n772' href='#n772'>772</a>
<a id='n773' href='#n773'>773</a>
<a id='n774' href='#n774'>774</a>
<a id='n775' href='#n775'>775</a>
<a id='n776' href='#n776'>776</a>
<a id='n777' href='#n777'>777</a>
<a id='n778' href='#n778'>778</a>
<a id='n779' href='#n779'>779</a>
<a id='n780' href='#n780'>780</a>
<a id='n781' href='#n781'>781</a>
<a id='n782' href='#n782'>782</a>
<a id='n783' href='#n783'>783</a>
<a id='n784' href='#n784'>784</a>
<a id='n785' href='#n785'>785</a>
<a id='n786' href='#n786'>786</a>
<a id='n787' href='#n787'>787</a>
<a id='n788' href='#n788'>788</a>
<a id='n789' href='#n789'>789</a>
<a id='n790' href='#n790'>790</a>
<a id='n791' href='#n791'>791</a>
<a id='n792' href='#n792'>792</a>
<a id='n793' href='#n793'>793</a>
<a id='n794' href='#n794'>794</a>
<a id='n795' href='#n795'>795</a>
<a id='n796' href='#n796'>796</a>
<a id='n797' href='#n797'>797</a>
<a id='n798' href='#n798'>798</a>
<a id='n799' href='#n799'>799</a>
<a id='n800' href='#n800'>800</a>
<a id='n801' href='#n801'>801</a>
<a id='n802' href='#n802'>802</a>
<a id='n803' href='#n803'>803</a>
<a id='n804' href='#n804'>804</a>
<a id='n805' href='#n805'>805</a>
<a id='n806' href='#n806'>806</a>
<a id='n807' href='#n807'>807</a>
<a id='n808' href='#n808'>808</a>
<a id='n809' href='#n809'>809</a>
<a id='n810' href='#n810'>810</a>
<a id='n811' href='#n811'>811</a>
<a id='n812' href='#n812'>812</a>
<a id='n813' href='#n813'>813</a>
<a id='n814' href='#n814'>814</a>
<a id='n815' href='#n815'>815</a>
<a id='n816' href='#n816'>816</a>
<a id='n817' href='#n817'>817</a>
<a id='n818' href='#n818'>818</a>
<a id='n819' href='#n819'>819</a>
<a id='n820' href='#n820'>820</a>
<a id='n821' href='#n821'>821</a>
<a id='n822' href='#n822'>822</a>
<a id='n823' href='#n823'>823</a>
<a id='n824' href='#n824'>824</a>
<a id='n825' href='#n825'>825</a>
<a id='n826' href='#n826'>826</a>
<a id='n827' href='#n827'>827</a>
<a id='n828' href='#n828'>828</a>
<a id='n829' href='#n829'>829</a>
<a id='n830' href='#n830'>830</a>
<a id='n831' href='#n831'>831</a>
<a id='n832' href='#n832'>832</a>
<a id='n833' href='#n833'>833</a>
<a id='n834' href='#n834'>834</a>
<a id='n835' href='#n835'>835</a>
<a id='n836' href='#n836'>836</a>
<a id='n837' href='#n837'>837</a>
<a id='n838' href='#n838'>838</a>
<a id='n839' href='#n839'>839</a>
<a id='n840' href='#n840'>840</a>
<a id='n841' href='#n841'>841</a>
<a id='n842' href='#n842'>842</a>
<a id='n843' href='#n843'>843</a>
<a id='n844' href='#n844'>844</a>
<a id='n845' href='#n845'>845</a>
<a id='n846' href='#n846'>846</a>
<a id='n847' href='#n847'>847</a>
<a id='n848' href='#n848'>848</a>
<a id='n849' href='#n849'>849</a>
<a id='n850' href='#n850'>850</a>
<a id='n851' href='#n851'>851</a>
<a id='n852' href='#n852'>852</a>
<a id='n853' href='#n853'>853</a>
<a id='n854' href='#n854'>854</a>
<a id='n855' href='#n855'>855</a>
<a id='n856' href='#n856'>856</a>
<a id='n857' href='#n857'>857</a>
<a id='n858' href='#n858'>858</a>
<a id='n859' href='#n859'>859</a>
<a id='n860' href='#n860'>860</a>
<a id='n861' href='#n861'>861</a>
<a id='n862' href='#n862'>862</a>
<a id='n863' href='#n863'>863</a>
<a id='n864' href='#n864'>864</a>
<a id='n865' href='#n865'>865</a>
<a id='n866' href='#n866'>866</a>
<a id='n867' href='#n867'>867</a>
<a id='n868' href='#n868'>868</a>
<a id='n869' href='#n869'>869</a>
<a id='n870' href='#n870'>870</a>
<a id='n871' href='#n871'>871</a>
<a id='n872' href='#n872'>872</a>
<a id='n873' href='#n873'>873</a>
<a id='n874' href='#n874'>874</a>
<a id='n875' href='#n875'>875</a>
<a id='n876' href='#n876'>876</a>
<a id='n877' href='#n877'>877</a>
<a id='n878' href='#n878'>878</a>
<a id='n879' href='#n879'>879</a>
<a id='n880' href='#n880'>880</a>
<a id='n881' href='#n881'>881</a>
<a id='n882' href='#n882'>882</a>
<a id='n883' href='#n883'>883</a>
<a id='n884' href='#n884'>884</a>
<a id='n885' href='#n885'>885</a>
<a id='n886' href='#n886'>886</a>
<a id='n887' href='#n887'>887</a>
<a id='n888' href='#n888'>888</a>
<a id='n889' href='#n889'>889</a>
<a id='n890' href='#n890'>890</a>
<a id='n891' href='#n891'>891</a>
<a id='n892' href='#n892'>892</a>
<a id='n893' href='#n893'>893</a>
<a id='n894' href='#n894'>894</a>
<a id='n895' href='#n895'>895</a>
<a id='n896' href='#n896'>896</a>
<a id='n897' href='#n897'>897</a>
<a id='n898' href='#n898'>898</a>
<a id='n899' href='#n899'>899</a>
<a id='n900' href='#n900'>900</a>
<a id='n901' href='#n901'>901</a>
<a id='n902' href='#n902'>902</a>
<a id='n903' href='#n903'>903</a>
<a id='n904' href='#n904'>904</a>
<a id='n905' href='#n905'>905</a>
<a id='n906' href='#n906'>906</a>
<a id='n907' href='#n907'>907</a>
<a id='n908' href='#n908'>908</a>
<a id='n909' href='#n909'>909</a>
<a id='n910' href='#n910'>910</a>
<a id='n911' href='#n911'>911</a>
<a id='n912' href='#n912'>912</a>
<a id='n913' href='#n913'>913</a>
<a id='n914' href='#n914'>914</a>
<a id='n915' href='#n915'>915</a>
<a id='n916' href='#n916'>916</a>
<a id='n917' href='#n917'>917</a>
<a id='n918' href='#n918'>918</a>
<a id='n919' href='#n919'>919</a>
<a id='n920' href='#n920'>920</a>
<a id='n921' href='#n921'>921</a>
<a id='n922' href='#n922'>922</a>
<a id='n923' href='#n923'>923</a>
<a id='n924' href='#n924'>924</a>
<a id='n925' href='#n925'>925</a>
<a id='n926' href='#n926'>926</a>
<a id='n927' href='#n927'>927</a>
<a id='n928' href='#n928'>928</a>
<a id='n929' href='#n929'>929</a>
<a id='n930' href='#n930'>930</a>
<a id='n931' href='#n931'>931</a>
<a id='n932' href='#n932'>932</a>
<a id='n933' href='#n933'>933</a>
<a id='n934' href='#n934'>934</a>
<a id='n935' href='#n935'>935</a>
<a id='n936' href='#n936'>936</a>
<a id='n937' href='#n937'>937</a>
<a id='n938' href='#n938'>938</a>
<a id='n939' href='#n939'>939</a>
<a id='n940' href='#n940'>940</a>
<a id='n941' href='#n941'>941</a>
<a id='n942' href='#n942'>942</a>
<a id='n943' href='#n943'>943</a>
<a id='n944' href='#n944'>944</a>
<a id='n945' href='#n945'>945</a>
<a id='n946' href='#n946'>946</a>
<a id='n947' href='#n947'>947</a>
<a id='n948' href='#n948'>948</a>
<a id='n949' href='#n949'>949</a>
<a id='n950' href='#n950'>950</a>
<a id='n951' href='#n951'>951</a>
<a id='n952' href='#n952'>952</a>
<a id='n953' href='#n953'>953</a>
<a id='n954' href='#n954'>954</a>
<a id='n955' href='#n955'>955</a>
<a id='n956' href='#n956'>956</a>
<a id='n957' href='#n957'>957</a>
<a id='n958' href='#n958'>958</a>
<a id='n959' href='#n959'>959</a>
<a id='n960' href='#n960'>960</a>
<a id='n961' href='#n961'>961</a>
<a id='n962' href='#n962'>962</a>
<a id='n963' href='#n963'>963</a>
<a id='n964' href='#n964'>964</a>
<a id='n965' href='#n965'>965</a>
<a id='n966' href='#n966'>966</a>
<a id='n967' href='#n967'>967</a>
<a id='n968' href='#n968'>968</a>
<a id='n969' href='#n969'>969</a>
<a id='n970' href='#n970'>970</a>
<a id='n971' href='#n971'>971</a>
<a id='n972' href='#n972'>972</a>
<a id='n973' href='#n973'>973</a>
<a id='n974' href='#n974'>974</a>
<a id='n975' href='#n975'>975</a>
<a id='n976' href='#n976'>976</a>
<a id='n977' href='#n977'>977</a>
<a id='n978' href='#n978'>978</a>
<a id='n979' href='#n979'>979</a>
<a id='n980' href='#n980'>980</a>
<a id='n981' href='#n981'>981</a>
<a id='n982' href='#n982'>982</a>
<a id='n983' href='#n983'>983</a>
<a id='n984' href='#n984'>984</a>
<a id='n985' href='#n985'>985</a>
<a id='n986' href='#n986'>986</a>
<a id='n987' href='#n987'>987</a>
<a id='n988' href='#n988'>988</a>
<a id='n989' href='#n989'>989</a>
<a id='n990' href='#n990'>990</a>
<a id='n991' href='#n991'>991</a>
<a id='n992' href='#n992'>992</a>
<a id='n993' href='#n993'>993</a>
<a id='n994' href='#n994'>994</a>
<a id='n995' href='#n995'>995</a>
<a id='n996' href='#n996'>996</a>
<a id='n997' href='#n997'>997</a>
<a id='n998' href='#n998'>998</a>
<a id='n999' href='#n999'>999</a>
<a id='n1000' href='#n1000'>1000</a>
<a id='n1001' href='#n1001'>1001</a>
<a id='n1002' href='#n1002'>1002</a>
<a id='n1003' href='#n1003'>1003</a>
<a id='n1004' href='#n1004'>1004</a>
<a id='n1005' href='#n1005'>1005</a>
<a id='n1006' href='#n1006'>1006</a>
<a id='n1007' href='#n1007'>1007</a>
<a id='n1008' href='#n1008'>1008</a>
<a id='n1009' href='#n1009'>1009</a>
<a id='n1010' href='#n1010'>1010</a>
<a id='n1011' href='#n1011'>1011</a>
<a id='n1012' href='#n1012'>1012</a>
<a id='n1013' href='#n1013'>1013</a>
<a id='n1014' href='#n1014'>1014</a>
<a id='n1015' href='#n1015'>1015</a>
<a id='n1016' href='#n1016'>1016</a>
<a id='n1017' href='#n1017'>1017</a>
<a id='n1018' href='#n1018'>1018</a>
<a id='n1019' href='#n1019'>1019</a>
<a id='n1020' href='#n1020'>1020</a>
<a id='n1021' href='#n1021'>1021</a>
<a id='n1022' href='#n1022'>1022</a>
<a id='n1023' href='#n1023'>1023</a>
<a id='n1024' href='#n1024'>1024</a>
<a id='n1025' href='#n1025'>1025</a>
<a id='n1026' href='#n1026'>1026</a>
<a id='n1027' href='#n1027'>1027</a>
<a id='n1028' href='#n1028'>1028</a>
<a id='n1029' href='#n1029'>1029</a>
<a id='n1030' href='#n1030'>1030</a>
<a id='n1031' href='#n1031'>1031</a>
<a id='n1032' href='#n1032'>1032</a>
<a id='n1033' href='#n1033'>1033</a>
<a id='n1034' href='#n1034'>1034</a>
<a id='n1035' href='#n1035'>1035</a>
<a id='n1036' href='#n1036'>1036</a>
<a id='n1037' href='#n1037'>1037</a>
<a id='n1038' href='#n1038'>1038</a>
<a id='n1039' href='#n1039'>1039</a>
<a id='n1040' href='#n1040'>1040</a>
<a id='n1041' href='#n1041'>1041</a>
<a id='n1042' href='#n1042'>1042</a>
<a id='n1043' href='#n1043'>1043</a>
<a id='n1044' href='#n1044'>1044</a>
<a id='n1045' href='#n1045'>1045</a>
<a id='n1046' href='#n1046'>1046</a>
<a id='n1047' href='#n1047'>1047</a>
<a id='n1048' href='#n1048'>1048</a>
<a id='n1049' href='#n1049'>1049</a>
<a id='n1050' href='#n1050'>1050</a>
<a id='n1051' href='#n1051'>1051</a>
<a id='n1052' href='#n1052'>1052</a>
<a id='n1053' href='#n1053'>1053</a>
<a id='n1054' href='#n1054'>1054</a>
<a id='n1055' href='#n1055'>1055</a>
<a id='n1056' href='#n1056'>1056</a>
<a id='n1057' href='#n1057'>1057</a>
<a id='n1058' href='#n1058'>1058</a>
<a id='n1059' href='#n1059'>1059</a>
<a id='n1060' href='#n1060'>1060</a>
<a id='n1061' href='#n1061'>1061</a>
<a id='n1062' href='#n1062'>1062</a>
<a id='n1063' href='#n1063'>1063</a>
<a id='n1064' href='#n1064'>1064</a>
<a id='n1065' href='#n1065'>1065</a>
<a id='n1066' href='#n1066'>1066</a>
<a id='n1067' href='#n1067'>1067</a>
<a id='n1068' href='#n1068'>1068</a>
<a id='n1069' href='#n1069'>1069</a>
<a id='n1070' href='#n1070'>1070</a>
</pre></td>
<td class='lines'><pre><code><style>pre { line-height: 125%; margin: 0; }
td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; }
td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; }
.highlight .hll { background-color: #ffffcc }
.highlight { background: #ffffff; }
.highlight .c { color: #888888 } /* Comment */
.highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */
.highlight .k { color: #008800; font-weight: bold } /* Keyword */
.highlight .ch { color: #888888 } /* Comment.Hashbang */
.highlight .cm { color: #888888 } /* Comment.Multiline */
.highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */
.highlight .cpf { color: #888888 } /* Comment.PreprocFile */
.highlight .c1 { color: #888888 } /* Comment.Single */
.highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */
.highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */
.highlight .ge { font-style: italic } /* Generic.Emph */
.highlight .gr { color: #aa0000 } /* Generic.Error */
.highlight .gh { color: #333333 } /* Generic.Heading */
.highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */
.highlight .go { color: #888888 } /* Generic.Output */
.highlight .gp { color: #555555 } /* Generic.Prompt */
.highlight .gs { font-weight: bold } /* Generic.Strong */
.highlight .gu { color: #666666 } /* Generic.Subheading */
.highlight .gt { color: #aa0000 } /* Generic.Traceback */
.highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */
.highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */
.highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */
.highlight .kp { color: #008800 } /* Keyword.Pseudo */
.highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */
.highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */
.highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */
.highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */
.highlight .na { color: #336699 } /* Name.Attribute */
.highlight .nb { color: #003388 } /* Name.Builtin */
.highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */
.highlight .no { color: #003366; font-weight: bold } /* Name.Constant */
.highlight .nd { color: #555555 } /* Name.Decorator */
.highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */
.highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */
.highlight .nl { color: #336699; font-style: italic } /* Name.Label */
.highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */
.highlight .py { color: #336699; font-weight: bold } /* Name.Property */
.highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */
.highlight .nv { color: #336699 } /* Name.Variable */
.highlight .ow { color: #008800 } /* Operator.Word */
.highlight .w { color: #bbbbbb } /* Text.Whitespace */
.highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */
.highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */
.highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */
.highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */
.highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */
.highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */
.highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */
.highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */
.highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */
.highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */
.highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */
.highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */
.highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */
.highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */
.highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */
.highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */
.highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */
.highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */
.highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */
.highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */
.highlight .vc { color: #336699 } /* Name.Variable.Class */
.highlight .vg { color: #dd7700 } /* Name.Variable.Global */
.highlight .vi { color: #3333bb } /* Name.Variable.Instance */
.highlight .vm { color: #336699 } /* Name.Variable.Magic */
.highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */</style><div class="highlight"><pre><span></span><span class="c">% IEEEtran howto:</span>
<span class="c">% http://ftp.univie.ac.at/packages/tex/macros/latex/contrib/IEEEtran/IEEEtran_HOWTO.pdf</span>
<span class="k">\documentclass</span><span class="na">[9pt,technote,a4paper]</span><span class="nb">{</span>IEEEtran<span class="nb">}</span>

<span class="k">\usepackage</span><span class="na">[T1]</span><span class="nb">{</span>fontenc<span class="nb">}</span>   <span class="c">% required for luximono!</span>
<span class="k">\usepackage</span><span class="na">[scaled=0.8]</span><span class="nb">{</span>luximono<span class="nb">}</span>  <span class="c">% typewriter font with bold face</span>

<span class="c">% To install the luximono font files:</span>
<span class="c">% getnonfreefonts-sys --all        or</span>
<span class="c">% getnonfreefonts-sys luximono</span>
<span class="c">%</span>
<span class="c">% when there are trouble you might need to:</span>
<span class="c">% - Create /etc/texmf/updmap.d/99local-luximono.cfg</span>
<span class="c">%   containing the single line: Map ul9.map</span>
<span class="c">% - Run update-updmap followed by mktexlsr and updmap-sys</span>
<span class="c">%</span>
<span class="c">% This commands must be executed as root with a root environment</span>
<span class="c">% (i.e. run &quot;sudo su&quot; and then execute the commands in the root</span>
<span class="c">% shell, don&#39;t just prefix the commands with &quot;sudo&quot;).</span>

<span class="k">\usepackage</span><span class="na">[unicode,bookmarks=false]</span><span class="nb">{</span>hyperref<span class="nb">}</span>
<span class="k">\usepackage</span><span class="na">[english]</span><span class="nb">{</span>babel<span class="nb">}</span>
<span class="k">\usepackage</span><span class="na">[utf8]</span><span class="nb">{</span>inputenc<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>amssymb<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>amsmath<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>amsfonts<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>units<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>nicefrac<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>eurosym<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>graphicx<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>verbatim<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>algpseudocode<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>scalefnt<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>xspace<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>color<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>colortbl<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>multirow<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>hhline<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>listings<span class="nb">}</span>
<span class="k">\usepackage</span><span class="nb">{</span>float<span class="nb">}</span>

<span class="k">\usepackage</span><span class="nb">{</span>tikz<span class="nb">}</span>
<span class="k">\usetikzlibrary</span><span class="nb">{</span>calc<span class="nb">}</span>
<span class="k">\usetikzlibrary</span><span class="nb">{</span>arrows<span class="nb">}</span>
<span class="k">\usetikzlibrary</span><span class="nb">{</span>scopes<span class="nb">}</span>
<span class="k">\usetikzlibrary</span><span class="nb">{</span>through<span class="nb">}</span>
<span class="k">\usetikzlibrary</span><span class="nb">{</span>shapes.geometric<span class="nb">}</span>

<span class="k">\def\FIXME</span><span class="nb">{{</span><span class="k">\color</span><span class="nb">{</span>red<span class="nb">}</span><span class="k">\bf</span> FIXME<span class="nb">}}</span>

<span class="k">\lstset</span><span class="nb">{</span>basicstyle=<span class="k">\ttfamily</span>,frame=trBL,xleftmargin=0.7cm,xrightmargin=0.2cm,numbers=left<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>document<span class="nb">}</span>

<span class="k">\title</span><span class="nb">{</span>Yosys Application Note 011: <span class="k">\\</span> Interactive Design Investigation<span class="nb">}</span>
<span class="k">\author</span><span class="nb">{</span>Clifford Wolf <span class="k">\\</span> Original Version December 2013<span class="nb">}</span>
<span class="k">\maketitle</span>

<span class="k">\begin</span><span class="nb">{</span>abstract<span class="nb">}</span>
Yosys <span class="k">\cite</span><span class="nb">{</span>yosys<span class="nb">}</span> can be a great environment for building custom synthesis
flows. It can also be an excellent tool for teaching and learning Verilog based
RTL synthesis. In both applications it is of great importance to be able to
analyze the designs it produces easily.

This Yosys application note covers the generation of circuit diagrams with the
Yosys <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command, the selection of interesting parts of the circuit
using the <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command, and briefly discusses advanced investigation
commands for evaluating circuits and solving SAT problems.
<span class="k">\end</span><span class="nb">{</span>abstract<span class="nb">}</span>

<span class="k">\section</span><span class="nb">{</span>Installation and Prerequisites<span class="nb">}</span>

This Application Note is based on the Yosys <span class="k">\cite</span><span class="nb">{</span>yosys<span class="nb">}</span> GIT Rev. <span class="nb">{</span><span class="k">\tt</span> 2b90ba1<span class="nb">}</span> from
2013-12-08. The <span class="nb">{</span><span class="k">\tt</span> README<span class="nb">}</span> file covers how to install Yosys. The
<span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command requires a working installation of GraphViz <span class="k">\cite</span><span class="nb">{</span>graphviz<span class="nb">}</span>
and <span class="k">\cite</span><span class="nb">{</span>xdot<span class="nb">}</span> for generating the actual circuit diagrams.

<span class="k">\section</span><span class="nb">{</span>Overview<span class="nb">}</span>

This application note is structured as follows:

Sec.~<span class="k">\ref</span><span class="nb">{</span>intro<span class="nb">_</span>show<span class="nb">}</span> introduces the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command and explains the
symbols used in the circuit diagrams generated by it.

Sec.~<span class="k">\ref</span><span class="nb">{</span>navigate<span class="nb">}</span> introduces additional commands used to navigate in the
design, select portions of the design, and print additional information on
the elements in the design that are not contained in the circuit diagrams.

Sec.~<span class="k">\ref</span><span class="nb">{</span>poke<span class="nb">}</span> introduces commands to evaluate the design and solve SAT
problems within the design.

Sec.~<span class="k">\ref</span><span class="nb">{</span>conclusion<span class="nb">}</span> concludes the document and summarizes the key points.

<span class="k">\section</span><span class="nb">{</span>Introduction to the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>intro<span class="nb">_</span>show<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="s">$</span><span class="nb"> cat example.ys</span>
<span class="nb">read_verilog example.v</span>
<span class="nb">show </span><span class="o">-</span><span class="nb">pause</span>
<span class="nb">proc</span>
<span class="nb">show </span><span class="o">-</span><span class="nb">pause</span>
<span class="nb">opt</span>
<span class="nb">show </span><span class="o">-</span><span class="nb">pause</span>

<span class="s">$</span> cat example.v
module example(input clk, a, b, c,
               output reg [1:0] y);
    always @(posedge clk)
        if (c)
            y &lt;= c ? a + b : 2&#39;d0;
endmodule
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Yosys script with <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> commands and example design<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>example<span class="nb">_</span>src<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b!]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/example<span class="nb">_</span>00.pdf<span class="nb">}</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/example<span class="nb">_</span>01.pdf<span class="nb">}</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/example<span class="nb">_</span>02.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of the three <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> commands from Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>src<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

The <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command generates a circuit diagram for the design in its
current state. Various options can be used to change the appearance of the
circuit diagram, set the name and format for the output file, and so forth.
When called without any special options, it saves the circuit diagram in
a temporary file and launches <span class="nb">{</span><span class="k">\tt</span> xdot<span class="nb">}</span> to display the diagram.
Subsequent calls to <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> re-use the <span class="nb">{</span><span class="k">\tt</span> xdot<span class="nb">}</span> instance
(if still running).

<span class="k">\subsection</span><span class="nb">{</span>A simple circuit<span class="nb">}</span>

Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>src<span class="nb">}</span> shows a simple synthesis script and a Verilog file that
demonstrate the usage of <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> in a simple setting. Note that <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span>
is called with the <span class="nb">{</span><span class="k">\tt</span> -pause<span class="nb">}</span> option, that halts execution of the Yosys
script until the user presses the Enter key. The <span class="nb">{</span><span class="k">\tt</span> show -pause<span class="nb">}</span> command
also allows the user to enter an interactive shell to further investigate the
circuit before continuing synthesis.

So this script, when executed, will show the design after each of the three
synthesis commands. The generated circuit diagrams are shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}</span>.

The first diagram (from top to bottom) shows the design directly after being
read by the Verilog front-end. Input and output ports are displayed as
octagonal shapes. Cells are displayed as rectangles with inputs on the left
and outputs on the right side. The cell labels are two lines long: The first line
contains a unique identifier for the cell and the second line contains the cell
type. Internal cell types are prefixed with a dollar sign. The Yosys manual
contains a chapter on the internal cell library used in Yosys.

Constants are shown as ellipses with the constant value as label. The syntax
<span class="nb">{</span><span class="k">\tt</span> &lt;bit<span class="k">\_</span>width&gt;&#39;&lt;bits&gt;<span class="nb">}</span> is used for for constants that are not 32-bit wide
and/or contain bits that are not 0 or 1 (i.e. <span class="nb">{</span><span class="k">\tt</span> x<span class="nb">}</span> or <span class="nb">{</span><span class="k">\tt</span> z<span class="nb">}</span>). Ordinary
32-bit constants are written using decimal numbers.

Single-bit signals are shown as thin arrows pointing from the driver to the
load. Signals that are multiple bits wide are shown as think arrows.

Finally <span class="nb">{</span><span class="k">\it</span> processes<span class="k">\/</span><span class="nb">}</span> are shown in boxes with round corners. Processes
are Yosys&#39; internal representation of the decision-trees and synchronization
events modelled in a Verilog <span class="nb">{</span><span class="k">\tt</span> always<span class="nb">}</span>-block. The label reads <span class="nb">{</span><span class="k">\tt</span> PROC<span class="nb">}</span>
followed by a unique identifier in the first line and contains the source code
location of the original <span class="nb">{</span><span class="k">\tt</span> always<span class="nb">}</span>-block in the 2nd line. Note how the
multiplexer from the <span class="nb">{</span><span class="k">\tt</span> ?:<span class="nb">}</span>-expression is represented as a <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>mux<span class="nb">}</span> cell
but the multiplexer from the <span class="nb">{</span><span class="k">\tt</span> if<span class="nb">}</span>-statement is yet still hidden within the
process.

<span class="k">\medskip</span>

The <span class="nb">{</span><span class="k">\tt</span> proc<span class="nb">}</span> command transforms the process from the first diagram into a
multiplexer and a d-type flip-flip, which brings us to the 2nd diagram.

The Rhombus shape to the right is a dangling wire. (Wire nodes are only shown
if they are dangling or have ``public&#39;&#39; names, for example names assigned from
the Verilog input.) Also note that the design now contains two instances of a
<span class="nb">{</span><span class="k">\tt</span> BUF<span class="nb">}</span>-node. This are artefacts left behind by the <span class="nb">{</span><span class="k">\tt</span> proc<span class="nb">}</span>-command. It is
quite usual to see such artefacts after calling commands that perform changes
in the design, as most commands only care about doing the transformation in the
least complicated way, not about cleaning up after them. The next call to <span class="nb">{</span><span class="k">\tt</span>
clean<span class="nb">}</span> (or <span class="nb">{</span><span class="k">\tt</span> opt<span class="nb">}</span>, which includes <span class="nb">{</span><span class="k">\tt</span> clean<span class="nb">}</span> as one of its operations) will
clean up this artefacts.  This operation is so common in Yosys scripts that it
can simply be abbreviated with the <span class="nb">{</span><span class="k">\tt</span> ;;<span class="nb">}</span> token, which doubles as
separator for commands. Unless one wants to specifically analyze this artefacts
left behind some operations, it is therefore recommended to always call <span class="nb">{</span><span class="k">\tt</span> clean<span class="nb">}</span>
before calling <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span>.

<span class="k">\medskip</span>

In this script we directly call <span class="nb">{</span><span class="k">\tt</span> opt<span class="nb">}</span> as next step, which finally leads us to
the 3rd diagram in Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}</span>. Here we see that the <span class="nb">{</span><span class="k">\tt</span> opt<span class="nb">}</span> command
not only has removed the artifacts left behind by <span class="nb">{</span><span class="k">\tt</span> proc<span class="nb">}</span>, but also determined
correctly that it can remove the first <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>mux<span class="nb">}</span> cell without changing the behavior
of the circuit.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b!]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 2cm 0 0]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/splice.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> yosys -p &#39;proc; opt; show&#39; splice.v<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>splice<span class="nb">_</span>dia<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b!]
<span class="k">\lstinputlisting</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/splice.v<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span><span class="k">\tt</span> splice.v<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>splice<span class="nb">_</span>src<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t!]
<span class="k">\includegraphics</span><span class="na">[height=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/cmos<span class="nb">_</span>00.pdf<span class="nb">}</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/cmos<span class="nb">_</span>01.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Effects of <span class="nb">{</span><span class="k">\tt</span> splitnets<span class="nb">}</span> command and of providing a cell library. (The
circuit is a half-adder built from simple CMOS gates.)<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>splitnets<span class="nb">_</span>libfile<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\subsection</span><span class="nb">{</span>Break-out boxes for signal vectors<span class="nb">}</span>

As has been indicated by the last example, Yosys is can manage signal vectors (aka.
multi-bit wires or buses) as native objects. This provides great advantages
when analyzing circuits that operate on wide integers. But it also introduces
some additional complexity when the individual bits of of a signal vector
are accessed. The example show in Fig.~<span class="k">\ref</span><span class="nb">{</span>splice<span class="nb">_</span>dia<span class="nb">}</span> and <span class="k">\ref</span><span class="nb">{</span>splice<span class="nb">_</span>src<span class="nb">}</span>
demonstrates how such circuits are visualized by the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command.

The key elements in understanding this circuit diagram are of course the boxes
with round corners and rows labeled <span class="nb">{</span><span class="k">\tt</span> &lt;MSB<span class="k">\_</span>LEFT&gt;:&lt;LSB<span class="k">\_</span>LEFT&gt; -- &lt;MSB<span class="k">\_</span>RIGHT&gt;:&lt;LSB<span class="k">\_</span>RIGHT&gt;<span class="nb">}</span>.
Each of this boxes has one signal per row on one side and a common signal for all rows on the
other side. The <span class="nb">{</span><span class="k">\tt</span> &lt;MSB&gt;:&lt;LSB&gt;<span class="nb">}</span> tuples specify which bits of the signals are broken out
and connected. So the top row of the box connecting the signals <span class="nb">{</span><span class="k">\tt</span> a<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> x<span class="nb">}</span> indicates
that the bit 0 (i.e. the range 0:0) from signal <span class="nb">{</span><span class="k">\tt</span> a<span class="nb">}</span> is connected to bit 1 (i.e. the range
1:1) of signal <span class="nb">{</span><span class="k">\tt</span> x<span class="nb">}</span>.

Lines connecting such boxes together and lines connecting such boxes to cell
ports have a slightly different look to emphasise that they are not actual signal
wires but a necessity of the graphical representation. This distinction seems
like a technicality, until one wants to debug a problem related to the way
Yosys internally represents signal vectors, for example when writing custom
Yosys commands.

<span class="k">\subsection</span><span class="nb">{</span>Gate level netlists<span class="nb">}</span>

Finally Fig.~<span class="k">\ref</span><span class="nb">{</span>splitnets<span class="nb">_</span>libfile<span class="nb">}</span> shows two common pitfalls when working
with designs mapped to a cell library. The top figure has two problems: First
Yosys did not have access to the cell library when this diagram was generated,
resulting in all cell ports defaulting to being inputs. This is why all ports
are drawn on the left side the cells are awkwardly arranged in a large column.
Secondly the two-bit vector <span class="nb">{</span><span class="k">\tt</span> y<span class="nb">}</span> requires breakout-boxes for its individual
bits, resulting in an unnecessary complex diagram.

For the 2nd diagram Yosys has been given a description of the cell library as
Verilog file containing blackbox modules. There are two ways to load cell
descriptions into Yosys: First the Verilog file for the cell library can be
passed directly to the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command using the <span class="nb">{</span><span class="k">\tt</span> -lib &lt;filename&gt;<span class="nb">}</span>
option. Secondly it is possible to load cell libraries into the design with
the <span class="nb">{</span><span class="k">\tt</span> read<span class="k">\_</span>verilog -lib &lt;filename&gt;<span class="nb">}</span> command. The 2nd method has the great
advantage that the library only needs to be loaded once and can then be used
in all subsequent calls to the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command.

In addition to that, the 2nd diagram was generated after <span class="nb">{</span><span class="k">\tt</span> splitnet -ports<span class="nb">}</span>
was run on the design. This command splits all signal vectors into individual
signal bits, which is often desirable when looking at gate-level circuits. The
<span class="nb">{</span><span class="k">\tt</span> -ports<span class="nb">}</span> option is required to also split module ports. Per default the
command only operates on interior signals.

<span class="k">\subsection</span><span class="nb">{</span>Miscellaneous notes<span class="nb">}</span>

Per default the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command outputs a temporary <span class="nb">{</span><span class="k">\tt</span> dot<span class="nb">}</span> file and launches
<span class="nb">{</span><span class="k">\tt</span> xdot<span class="nb">}</span> to display it. The options <span class="nb">{</span><span class="k">\tt</span> -format<span class="nb">}</span>, <span class="nb">{</span><span class="k">\tt</span> -viewer<span class="nb">}</span>
and <span class="nb">{</span><span class="k">\tt</span> -prefix<span class="nb">}</span> can be used to change format, viewer and filename prefix.
Note that the <span class="nb">{</span><span class="k">\tt</span> pdf<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> ps<span class="nb">}</span> format are the only formats that support
plotting multiple modules in one run.

In densely connected circuits it is sometimes hard to keep track of the
individual signal wires. For this cases it can be useful to call <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span>
with the <span class="nb">{</span><span class="k">\tt</span> -colors &lt;integer&gt;<span class="nb">}</span> argument, which randomly assigns colors to the
nets.  The integer (&gt; 0) is used as seed value for the random color
assignments. Sometimes it is necessary it try some values to find an assignment
of colors that looks good.

The command <span class="nb">{</span><span class="k">\tt</span> help show<span class="nb">}</span> prints a complete listing of all options supported
by the <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> command.

<span class="k">\section</span><span class="nb">{</span>Navigating the design<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>navigate<span class="nb">}</span>

Plotting circuit diagrams for entire modules in the design brings us only helps
in simple cases. For complex modules the generated circuit diagrams are just stupidly big
and are no help at all. In such cases one first has to select the relevant
portions of the circuit.

In addition to <span class="nb">{</span><span class="k">\it</span> what<span class="k">\/</span><span class="nb">}</span> to display one also needs to carefully decide
<span class="nb">{</span><span class="k">\it</span> when<span class="k">\/</span><span class="nb">}</span> to display it, with respect to the synthesis flow. In general
it is a good idea to troubleshoot a circuit in the earliest state in which
a problem can be reproduced. So if, for example, the internal state before calling
the <span class="nb">{</span><span class="k">\tt</span> techmap<span class="nb">}</span> command already fails to verify, it is better to troubleshoot
the coarse-grain version of the circuit before <span class="nb">{</span><span class="k">\tt</span> techmap<span class="nb">}</span> than the gate-level
circuit after <span class="nb">{</span><span class="k">\tt</span> techmap<span class="nb">}</span>.

<span class="k">\medskip</span>

Note: It is generally recommended to verify the internal state of a design by
writing it to a Verilog file using <span class="nb">{</span><span class="k">\tt</span> write<span class="k">\_</span>verilog -noexpr<span class="nb">}</span> and using the
simulation models from <span class="nb">{</span><span class="k">\tt</span> simlib.v<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> simcells.v<span class="nb">}</span> from the Yosys data
directory (as printed by <span class="nb">{</span><span class="k">\tt</span> yosys-config -<span class="nb">{}</span>-datdir<span class="nb">}</span>).

<span class="k">\subsection</span><span class="nb">{</span>Interactive Navigation<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
yosys&gt; ls

1 modules:
  example

yosys&gt; cd example

yosys [example]&gt; ls

7 wires:
  <span class="s">$</span><span class="m">0</span><span class="nv">\y</span><span class="o">[</span><span class="m">1</span><span class="nb">:</span><span class="m">0</span><span class="o">]</span><span class="nb"></span>
<span class="nb">  </span><span class="s">$</span>add<span class="s">$</span><span class="nb">example.v:</span><span class="m">5</span><span class="s">$</span>2<span class="nb">_</span>Y
  a
  b
  c
  clk
  y

3 cells:
  <span class="s">$</span><span class="nb">add</span><span class="s">$</span>example.v:5<span class="s">$</span><span class="m">2</span><span class="nb"></span>
<span class="nb">  </span><span class="s">$</span>procdff<span class="s">$</span><span class="m">7</span><span class="nb"></span>
<span class="nb">  </span><span class="s">$</span>procmux<span class="s">$</span><span class="m">5</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nv">\caption</span><span class="nb">{Demonstration of {</span><span class="nv">\tt</span><span class="nb"> ls} and {</span><span class="nv">\tt</span><span class="nb"> cd} using {</span><span class="nv">\tt</span><span class="nb"> example.v} from Fig.~</span><span class="nv">\ref</span><span class="nb">{example_src}}</span>
<span class="nv">\label</span><span class="nb">{lscd}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">b</span><span class="o">]</span><span class="nb"></span>
<span class="nv">\begin</span><span class="nb">{lstlisting}</span>
<span class="nb">  attribute </span><span class="nv">\src</span><span class="nb"> &quot;example.v:</span><span class="m">5</span><span class="nb">&quot;</span>
<span class="nb">  cell </span><span class="s">$</span>add <span class="s">$</span><span class="nb">add</span><span class="s">$</span>example.v:5<span class="s">$</span><span class="m">2</span><span class="nb"></span>
<span class="nb">    parameter </span><span class="nv">\A</span><span class="nb">_SIGNED </span><span class="m">0</span><span class="nb"></span>
<span class="nb">    parameter </span><span class="nv">\A</span><span class="nb">_WIDTH </span><span class="m">1</span><span class="nb"></span>
<span class="nb">    parameter </span><span class="nv">\B</span><span class="nb">_SIGNED </span><span class="m">0</span><span class="nb"></span>
<span class="nb">    parameter </span><span class="nv">\B</span><span class="nb">_WIDTH </span><span class="m">1</span><span class="nb"></span>
<span class="nb">    parameter </span><span class="nv">\Y</span><span class="nb">_WIDTH </span><span class="m">2</span><span class="nb"></span>
<span class="nb">    connect </span><span class="nv">\A</span><span class="nb"> </span><span class="nv">\a</span><span class="nb"></span>
<span class="nb">    connect </span><span class="nv">\B</span><span class="nb"> </span><span class="nv">\b</span><span class="nb"></span>
<span class="nb">    connect </span><span class="nv">\Y</span><span class="nb"> </span><span class="s">$</span>add<span class="s">$</span><span class="nb">example.v:</span><span class="m">5</span><span class="s">$</span>2<span class="nb">_</span>Y
  end
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> dump <span class="k">\$</span>2<span class="nb">}</span> using the design from Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>src<span class="nb">}</span> and  Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>dump2<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

Once the right state within the synthesis flow for debugging the circuit has
been identified, it is recommended to simply add the <span class="nb">{</span><span class="k">\tt</span> shell<span class="nb">}</span> command
to the matching place in the synthesis script. This command will stop the
synthesis at the specified moment and go to shell mode, where the user can
interactively enter commands.

For most cases, the shell will start with the whole design selected (i.e.  when
the synthesis script does not already narrow the selection). The command <span class="nb">{</span><span class="k">\tt</span>
ls<span class="nb">}</span> can now be used to create a list of all modules. The command <span class="nb">{</span><span class="k">\tt</span> cd<span class="nb">}</span> can
be used to switch to one of the modules (type <span class="nb">{</span><span class="k">\tt</span> cd ..<span class="nb">}</span> to switch back). Now
the <span class="nb">{</span><span class="k">\tt</span> ls<span class="nb">}</span> command lists the objects within that module. Fig.~<span class="k">\ref</span><span class="nb">{</span>lscd<span class="nb">}</span>
demonstrates this using the design from Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>src<span class="nb">}</span>.

There is a thing to note in Fig.~<span class="k">\ref</span><span class="nb">{</span>lscd<span class="nb">}</span>: We can see that the cell names
from Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}</span> are just abbreviations of the actual cell names,
namely the part after the last dollar-sign. Most auto-generated names (the ones
starting with a dollar sign) are rather long and contains some additional
information on the origin of the named object. But in most cases those names
can simply be abbreviated using the last part.

Usually all interactive work is done with one module selected using the <span class="nb">{</span><span class="k">\tt</span> cd<span class="nb">}</span>
command. But it is also possible to work from the design-context (<span class="nb">{</span><span class="k">\tt</span> cd ..<span class="nb">}</span>). In
this case all object names must be prefixed with <span class="nb">{</span><span class="k">\tt</span> &lt;module<span class="k">\_</span>name&gt;/<span class="nb">}</span>. For
example <span class="nb">{</span><span class="k">\tt</span> a*/b*<span class="nb">}</span> would refer to all objects whose names start with <span class="nb">{</span><span class="k">\tt</span> b<span class="nb">}</span> from
all modules whose names start with <span class="nb">{</span><span class="k">\tt</span> a<span class="nb">}</span>.

The <span class="nb">{</span><span class="k">\tt</span> dump<span class="nb">}</span> command can be used to print all information about an object.
For example <span class="nb">{</span><span class="k">\tt</span> dump <span class="k">\$</span>2<span class="nb">}</span> will print Fig.~<span class="k">\ref</span><span class="nb">{</span>dump2<span class="nb">}</span>. This can for example
be useful to determine the names of nets connected to cells, as the net-names
are usually suppressed in the circuit diagram if they are auto-generated.

For the remainder of this document we will assume that the commands are run from
module-context and not design-context.

<span class="k">\subsection</span><span class="nb">{</span>Working with selections<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/example<span class="nb">_</span>03.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span> after <span class="nb">{</span><span class="k">\tt</span> select <span class="k">\$</span>2<span class="nb">}</span> or <span class="nb">{</span><span class="k">\tt</span> select t:<span class="k">\$</span>add<span class="nb">}</span>
(see also Fig.~<span class="k">\ref</span><span class="nb">{</span>example<span class="nb">_</span>out<span class="nb">}</span>)<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>seladd<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

When a module is selected using the <span class="nb">{</span><span class="k">\tt</span> cd<span class="nb">}</span> command, all commands (with a few
exceptions, such as the <span class="nb">{</span><span class="k">\tt</span> read<span class="k">\_*</span><span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> write<span class="k">\_*</span><span class="nb">}</span> commands) operate
only on the selected module. This can also be useful for synthesis scripts
where different synthesis strategies should be applied to different modules
in the design.

But for most interactive work we want to further narrow the set of selected
objects. This can be done using the <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command.

For example, if the command <span class="nb">{</span><span class="k">\tt</span> select <span class="k">\$</span>2<span class="nb">}</span> is executed, a subsequent <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span>
command will yield the diagram shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>seladd<span class="nb">}</span>. Note that the nets are
now displayed in ellipses. This indicates that they are not selected, but only
shown because the diagram contains a cell that is connected to the net. This
of course makes no difference for the circuit that is shown, but it can be a useful
information when manipulating selections.

Objects can not only be selected by their name but also by other properties.
For example <span class="nb">{</span><span class="k">\tt</span> select t:<span class="k">\$</span>add<span class="nb">}</span> will select all cells of type <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>add<span class="nb">}</span>. In
this case this is also yields the diagram shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>seladd<span class="nb">}</span>.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b]
<span class="k">\lstinputlisting</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/foobaraddsub.v<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Test module for operations on selections<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>foobaraddsub<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

The output of <span class="nb">{</span><span class="k">\tt</span> help select<span class="nb">}</span> contains a complete syntax reference for
matching different properties.

Many commands can operate on explicit selections. For example the command <span class="nb">{</span><span class="k">\tt</span>
dump t:<span class="k">\$</span>add<span class="nb">}</span> will print information on all <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>add<span class="nb">}</span> cells in the active
module. Whenever a command has <span class="nb">{</span><span class="k">\tt</span> [selection]<span class="nb">}</span> as last argument in its usage
help, this means that it will use the engine behind the <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command
to evaluate additional arguments and use the resulting selection instead of
the selection created by the last <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command.

Normally the <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command overwrites a previous selection. The
commands <span class="nb">{</span><span class="k">\tt</span> select -add<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> select -del<span class="nb">}</span> can be used to add
or remove objects from the current selection.

The command <span class="nb">{</span><span class="k">\tt</span> select -clear<span class="nb">}</span> can be used to reset the selection to the
default, which is a complete selection of everything in the current module.

<span class="k">\subsection</span><span class="nb">{</span>Operations on selections<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t]
<span class="k">\lstinputlisting</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod.v<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Another test module for operations on selections<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>sumprod<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>00.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> show a:sumstuff<span class="nb">}</span> on Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>sumprod<span class="nb">_</span>00<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

The <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command is actually much more powerful than it might seem on
the first glimpse. When it is called with multiple arguments, each argument is
evaluated and pushed separately on a stack. After all arguments have been
processed it simply creates the union of all elements on the stack. So the
following command will select all <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>add<span class="nb">}</span> cells and all objects with
the <span class="nb">{</span><span class="k">\tt</span> foo<span class="nb">}</span> attribute set:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
select t:<span class="s">$</span><span class="nb">add a:foo</span>
<span class="nv">\end</span><span class="nb">{verbatim}</span>

<span class="o">(</span><span class="nb">Try this with the design shown in Fig.~</span><span class="nv">\ref</span><span class="nb">{foobaraddsub}. Use the {</span><span class="nv">\tt</span><span class="nb"></span>
<span class="nb">select </span><span class="o">-</span><span class="nb">list} command to list the current selection.</span><span class="o">)</span><span class="nb"></span>

<span class="nb">In many cases simply adding more and more stuff to the selection is an</span>
<span class="nb">ineffective way of selecting the interesting part of the design. Special</span>
<span class="nb">arguments can be used to combine the elements on the stack.</span>
<span class="nb">For example the {</span><span class="nv">\tt</span><span class="nb"> </span><span class="nv">\%</span><span class="nb">i} arguments pops the last two elements from</span>
<span class="nb">the stack, intersects them, and pushes the result back on the stack. So the</span>
<span class="nb">following command will select all {</span><span class="nv">\$</span><span class="nb">add} cells that have the {</span><span class="nv">\tt</span><span class="nb"> foo}</span>
<span class="nb">attribute set:</span>

<span class="nv">\begin</span><span class="nb">{verbatim}</span>
<span class="nb">select t:</span><span class="s">$</span>add a:foo <span class="c">%i</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

The listing in Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">}</span> uses the Yosys non-standard <span class="nb">{</span><span class="k">\tt</span> <span class="k">\{*</span> ... *<span class="k">\}</span><span class="nb">}</span>
syntax to set the attribute <span class="nb">{</span><span class="k">\tt</span> sumstuff<span class="nb">}</span> on all cells generated by the first
assign statement. (This works on arbitrary large blocks of Verilog code an
can be used to mark portions of code for analysis.)

Selecting <span class="nb">{</span><span class="k">\tt</span> a:sumstuff<span class="nb">}</span> in this module will yield the circuit diagram shown
in Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">_</span>00<span class="nb">}</span>. As only the cells themselves are selected, but not
the temporary wire <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>1<span class="k">\_</span>Y<span class="nb">}</span>, the two adders are shown as two disjunct
parts. This can be very useful for global signals like clock and reset signals: just
unselect them using a command such as <span class="nb">{</span><span class="k">\tt</span> select -del clk rst<span class="nb">}</span> and each cell
using them will get its own net label.

In this case however we would like to see the cells connected properly. This
can be achieved using the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>x<span class="nb">}</span> action, that broadens the selection, i.e.
for each selected wire it selects all cells connected to the wire and vice
versa. So <span class="nb">{</span><span class="k">\tt</span> show a:sumstuff <span class="k">\%</span>x<span class="nb">}</span> yields the diagram shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">_</span>01<span class="nb">}</span>.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>01.pdf<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> show a:sumstuff <span class="k">\%</span>x<span class="nb">}</span> on Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>sumprod<span class="nb">_</span>01<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\subsection</span><span class="nb">{</span>Selecting logic cones<span class="nb">}</span>

Fig.~<span class="k">\ref</span><span class="nb">{</span>sumprod<span class="nb">_</span>01<span class="nb">}</span> shows what is called the <span class="nb">{</span><span class="k">\it</span> input cone<span class="k">\/</span><span class="nb">}</span> of <span class="nb">{</span><span class="k">\tt</span> sum<span class="nb">}</span>, i.e.
all cells and signals that are used to generate the signal <span class="nb">{</span><span class="k">\tt</span> sum<span class="nb">}</span>. The <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span>
action can be used to select the input cones of all object in the top selection
in the stack maintained by the <span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command.

As the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>x<span class="nb">}</span> action, this commands broadens the selection by one ``step&#39;&#39;. But
this time the operation only works against the direction of data flow. That means,
wires only select cells via output ports and cells only select wires via input ports.

Fig.~<span class="k">\ref</span><span class="nb">{</span>select<span class="nb">_</span>prod<span class="nb">}</span> show the sequence of diagrams generated by the following
commands:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show prod
show prod <span class="c">%ci</span>
show prod <span class="c">%ci %ci</span>
show prod <span class="c">%ci %ci %ci</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

When selecting many levels of logic, repeating <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> over and over again
can be a bit dull. So there is a shortcut for that: the number of iterations
can be appended to the action. So for example the action <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci3<span class="nb">}</span> is
identical to performing the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> action three times.

The action <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci*<span class="nb">}</span> performs the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> action over and over again until
it has no effect anymore.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t]
<span class="k">\hfill</span> <span class="k">\includegraphics</span><span class="na">[width=4cm,trim=0 1cm 0 1cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>02.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 0cm 0 1cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>03.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 0cm 0 1cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>04.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 2cm 0 1cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/sumprod<span class="nb">_</span>05.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\caption</span><span class="nb">{</span>Objects selected by <span class="nb">{</span><span class="k">\tt</span> select prod <span class="k">\%</span>ci...<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>select<span class="nb">_</span>prod<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\medskip</span>

In most cases there are certain cell types and/or ports that should not be considered for the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span>
action, or we only want to follow certain cell types and/or ports. This can be achieved using additional
patterns that can be appended to the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> action.

Lets consider the design from Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>src<span class="nb">}</span>. It serves no purpose other than being a non-trivial
circuit for demonstrating some of the advanced Yosys features. We synthesize the circuit using <span class="nb">{</span><span class="k">\tt</span> proc;
opt; memory; opt<span class="nb">}</span> and change to the <span class="nb">{</span><span class="k">\tt</span> memdemo<span class="nb">}</span> module with <span class="nb">{</span><span class="k">\tt</span> cd memdemo<span class="nb">}</span>. If we type <span class="nb">{</span><span class="k">\tt</span> show<span class="nb">}</span>
now we see the diagram shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>00<span class="nb">}</span>.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b!]
<span class="k">\lstinputlisting</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/memdemo.v<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Demo circuit for demonstrating some advanced Yosys features<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>memdemo<span class="nb">_</span>src<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure*<span class="nb">}</span>[t]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 0cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/memdemo<span class="nb">_</span>00.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\caption</span><span class="nb">{</span>Complete circuit diagram for the design shown in Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>src<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>memdemo<span class="nb">_</span>00<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure*<span class="nb">}</span>

But maybe we are only interested in the tree of multiplexers that select the
output value. In order to get there, we would start by just showing the output signal
and its immediate predecessors:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

From this we would learn that <span class="nb">{</span><span class="k">\tt</span> y<span class="nb">}</span> is driven by a <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>dff cell<span class="nb">}</span>, that
<span class="nb">{</span><span class="k">\tt</span> y<span class="nb">}</span> is connected to the output port <span class="nb">{</span><span class="k">\tt</span> Q<span class="nb">}</span>, that the <span class="nb">{</span><span class="k">\tt</span> clk<span class="nb">}</span> signal goes
into the <span class="nb">{</span><span class="k">\tt</span> CLK<span class="nb">}</span> input port of the cell, and that the data comes from a
auto-generated wire into the input <span class="nb">{</span><span class="k">\tt</span> D<span class="nb">}</span> of the flip-flop cell.

As we are not interested in the clock signal we add an additional pattern to the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span>
action, that tells it to only follow ports <span class="nb">{</span><span class="k">\tt</span> Q<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> D<span class="nb">}</span> of <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>dff<span class="nb">}</span> cells:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2:+$dff[Q,D]</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

To add a pattern we add a colon followed by the pattern to the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span>
action. The pattern it self starts with <span class="nb">{</span><span class="k">\tt</span> -<span class="nb">}</span> or <span class="nb">{</span><span class="k">\tt</span> +<span class="nb">}</span>, indicating if it is
an include or exclude pattern, followed by an optional comma separated list
of cell types, followed by an optional comma separated list of port names in
square brackets.

Since we know that the only cell considered in this case is a <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>dff<span class="nb">}</span> cell,
we could as well only specify the port names:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2:+[Q,D]</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

Or we could decide to tell the <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> action to not follow the <span class="nb">{</span><span class="k">\tt</span> CLK<span class="nb">}</span> input:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2:-[CLK]</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 0cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/memdemo<span class="nb">_</span>01.pdf<span class="nb">}</span> <span class="k">\\</span>
<span class="k">\caption</span><span class="nb">{</span>Output of <span class="nb">{</span><span class="k">\tt</span> show y <span class="k">\%</span>ci2:+<span class="k">\$</span>dff[Q,D] <span class="k">\%</span>ci*:-<span class="k">\$</span>mux[S]:-<span class="k">\$</span>dff<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>memdemo<span class="nb">_</span>01<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

Next we would investigate the next logic level by adding another <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci2<span class="nb">}</span> to
the command:

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2:-[CLK] %ci2</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

From this we would learn that the next cell is a <span class="nb">{</span><span class="k">\tt</span> <span class="k">\$</span>mux<span class="nb">}</span> cell and we would add additional
pattern to narrow the selection on the path we are interested. In the end we would end up
with a command such as

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
show y <span class="c">%ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

in which the first <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> jumps over the initial d-type flip-flop and the
2nd action selects the entire input cone without going over multiplexer select
inputs and flip-flop cells. The diagram produces by this command is shown in
Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>01<span class="nb">}</span>.

<span class="k">\medskip</span>

Similar to <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>ci<span class="nb">}</span> exists an action <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>co<span class="nb">}</span> to select output cones that
accepts the same syntax for pattern and repetition. The <span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>x<span class="nb">}</span> action mentioned
previously also accepts this advanced syntax.

This actions for traversing the circuit graph, combined with the actions for
boolean operations such as intersection (<span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>i<span class="nb">}</span>) and difference (<span class="nb">{</span><span class="k">\tt</span> <span class="k">\%</span>d<span class="nb">}</span>)
are powerful tools for extracting the relevant portions of the circuit under
investigation.

See <span class="nb">{</span><span class="k">\tt</span> help select<span class="nb">}</span> for a complete list of actions available in selections.

<span class="k">\subsection</span><span class="nb">{</span>Storing and recalling selections<span class="nb">}</span>

The current selection can be stored in memory with the command <span class="nb">{</span><span class="k">\tt</span> select -set
&lt;name&gt;<span class="nb">}</span>. It can later be recalled using <span class="nb">{</span><span class="k">\tt</span> select @&lt;name&gt;<span class="nb">}</span>. In fact, the <span class="nb">{</span><span class="k">\tt</span>
@&lt;name&gt;<span class="nb">}</span> expression pushes the stored selection on the stack maintained by the
<span class="nb">{</span><span class="k">\tt</span> select<span class="nb">}</span> command. So for example

<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
select @foo @bar <span class="c">%i</span>
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>

will select the intersection between the stored selections <span class="nb">{</span><span class="k">\tt</span> foo<span class="nb">}</span> and <span class="nb">{</span><span class="k">\tt</span> bar<span class="nb">}</span>.

<span class="k">\medskip</span>

In larger investigation efforts it is highly recommended to maintain a script that
sets up relevant selections, so they can easily be recalled, for example when
Yosys needs to be re-run after a design or source code change.

The <span class="nb">{</span><span class="k">\tt</span> history<span class="nb">}</span> command can be used to list all recent interactive commands.
This feature can be useful for creating such a script from the commands used in
an interactive session.

<span class="k">\section</span><span class="nb">{</span>Advanced investigation techniques<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>poke<span class="nb">}</span>

When working with very large modules, it is often not enough to just select the
interesting part of the module. Instead it can be useful to extract the
interesting part of the circuit into a separate module. This can for example be
useful if one wants to run a series of synthesis commands on the critical part
of the module and wants to carefully read all the debug output created by the
commands in order to spot a problem. This kind of troubleshooting is much easier
if the circuit under investigation is encapsulated in a separate module.

Fig.~<span class="k">\ref</span><span class="nb">{</span>submod<span class="nb">}</span> shows how the <span class="nb">{</span><span class="k">\tt</span> submod<span class="nb">}</span> command can be used to split the
circuit from Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>src<span class="nb">}</span> and <span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>00<span class="nb">}</span> into its components.
The <span class="nb">{</span><span class="k">\tt</span> -name<span class="nb">}</span> option is used to specify the name of the new module and
also the name of the new cell in the current module.

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[t]
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 1.3cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/submod<span class="nb">_</span>00.pdf<span class="nb">}</span> <span class="k">\\</span> <span class="k">\centerline</span><span class="nb">{</span><span class="k">\tt</span> memdemo<span class="nb">}</span> <span class="k">\vskip</span>1em<span class="k">\par</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 1.3cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/submod<span class="nb">_</span>01.pdf<span class="nb">}</span> <span class="k">\\</span> <span class="k">\centerline</span><span class="nb">{</span><span class="k">\tt</span> scramble<span class="nb">}</span> <span class="k">\vskip</span>1em<span class="k">\par</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 1.3cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/submod<span class="nb">_</span>02.pdf<span class="nb">}</span> <span class="k">\\</span> <span class="k">\centerline</span><span class="nb">{</span><span class="k">\tt</span> outstage<span class="nb">}</span> <span class="k">\vskip</span>1em<span class="k">\par</span>
<span class="k">\includegraphics</span><span class="na">[width=\linewidth,trim=0 1.3cm 0 0cm]</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/submod<span class="nb">_</span>03.pdf<span class="nb">}</span> <span class="k">\\</span> <span class="k">\centerline</span><span class="nb">{</span><span class="k">\tt</span> selstage<span class="nb">}</span> <span class="k">\vskip</span>1em<span class="k">\par</span>
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[basicstyle=<span class="k">\ttfamily\scriptsize</span>]
select -set outstage y <span class="c">%ci2:+$dff[Q,D] %ci*:-$mux[S]:-$dff</span>
select -set selstage y <span class="c">%ci2:+$dff[Q,D] %ci*:-$dff @outstage %d</span>
select -set scramble mem* <span class="c">%ci2 %ci*:-$dff mem* %d @selstage %d</span>
submod -name scramble @scramble
submod -name outstage @outstage
submod -name selstage @selstage
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>The circuit from Fig.~<span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>src<span class="nb">}</span> and <span class="k">\ref</span><span class="nb">{</span>memdemo<span class="nb">_</span>00<span class="nb">}</span> broken up using <span class="nb">{</span><span class="k">\tt</span> submod<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>submod<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\subsection</span><span class="nb">{</span>Evaluation of combinatorial circuits<span class="nb">}</span>

The <span class="nb">{</span><span class="k">\tt</span> eval<span class="nb">}</span> command can be used to evaluate combinatorial circuits.
For example (see Fig.~<span class="k">\ref</span><span class="nb">{</span>submod<span class="nb">}</span> for the circuit diagram of <span class="nb">{</span><span class="k">\tt</span> selstage<span class="nb">}</span>):

<span class="nb">{</span><span class="k">\scriptsize</span>
<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
   yosys [selstage]&gt; eval -set s2,s1 4&#39;b1001 -set d 4&#39;hc -show n2 -show n1

   9. Executing EVAL pass (evaluate the circuit given an input).
   Full command line: eval -set s2,s1 4&#39;b1001 -set d 4&#39;hc -show n2 -show n1
   Eval result: <span class="k">\n</span>2 = 2&#39;10.
   Eval result: <span class="k">\n</span>1 = 2&#39;10.
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>
<span class="k">\par</span><span class="nb">}</span>

So the <span class="nb">{</span><span class="k">\tt</span> -set<span class="nb">}</span> option is used to set input values and the <span class="nb">{</span><span class="k">\tt</span> -show<span class="nb">}</span> option
is used to specify the nets to evaluate. If no <span class="nb">{</span><span class="k">\tt</span> -show<span class="nb">}</span> option is specified,
all selected output ports are used per default.

If a necessary input value is not given, an error is produced. The option
<span class="nb">{</span><span class="k">\tt</span> -set-undef<span class="nb">}</span> can be used to instead set all unspecified input nets to
undef (<span class="nb">{</span><span class="k">\tt</span> x<span class="nb">}</span>).

The <span class="nb">{</span><span class="k">\tt</span> -table<span class="nb">}</span> option can be used to create a truth table. For example:

<span class="nb">{</span><span class="k">\scriptsize</span>
<span class="k">\begin</span><span class="nb">{</span>verbatim<span class="nb">}</span>
   yosys [selstage]&gt; eval -set-undef -set d[3:1] 0 -table s1,d[0]

   10. Executing EVAL pass (evaluate the circuit given an input).
   Full command line: eval -set-undef -set d[3:1] 0 -table s1,d[0]

     <span class="k">\s</span>1 <span class="k">\d</span> [0] |  <span class="k">\n</span>1  <span class="k">\n</span>2
    ---- ------ | ---- ----
    2&#39;00    1&#39;0 | 2&#39;00 2&#39;00
    2&#39;00    1&#39;1 | 2&#39;xx 2&#39;00
    2&#39;01    1&#39;0 | 2&#39;00 2&#39;00
    2&#39;01    1&#39;1 | 2&#39;xx 2&#39;01
    2&#39;10    1&#39;0 | 2&#39;00 2&#39;00
    2&#39;10    1&#39;1 | 2&#39;xx 2&#39;10
    2&#39;11    1&#39;0 | 2&#39;00 2&#39;00
    2&#39;11    1&#39;1 | 2&#39;xx 2&#39;11

   Assumed undef (x) value for the following signals: <span class="k">\s</span>2
<span class="k">\end</span><span class="nb">{</span>verbatim<span class="nb">}</span>
<span class="nb">}</span>

Note that the <span class="nb">{</span><span class="k">\tt</span> eval<span class="nb">}</span> command (as well as the <span class="nb">{</span><span class="k">\tt</span> sat<span class="nb">}</span> command discussed in
the next sections) does only operate on flattened modules. It can not analyze
signals that are passed through design hierarchy levels. So the <span class="nb">{</span><span class="k">\tt</span> flatten<span class="nb">}</span>
command must be used on modules that instantiate other modules before this
commands can be applied.

<span class="k">\subsection</span><span class="nb">{</span>Solving combinatorial SAT problems<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[b]
<span class="k">\lstinputlisting</span><span class="nb">{</span>APPNOTE<span class="nb">_</span>011<span class="nb">_</span>Design<span class="nb">_</span>Investigation/primetest.v<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>A simple miter circuit for testing if a number is prime. But it has a
problem (see main text and Fig.~<span class="k">\ref</span><span class="nb">{</span>primesat<span class="nb">}</span>).<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>primetest<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure*<span class="nb">}</span>[!t]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[basicstyle=<span class="k">\ttfamily\small</span>]
yosys [primetest]&gt; sat -prove ok 1 -set p 31

8. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31

Setting up SAT problem:
Import set-constraint: <span class="k">\p</span> = 16&#39;0000000000011111
Final constraint equation: <span class="k">\p</span> = 16&#39;0000000000011111
Imported 6 cells to SAT database.
Import proof-constraint: <span class="k">\ok</span> = 1&#39;1
Final proof equation: <span class="k">\ok</span> = 1&#39;1

Solving problem with 2790 variables and 8241 clauses..
SAT proof finished - model found: FAIL!

   <span class="nb">______</span>                   <span class="nb">___</span>       <span class="nb">___</span>       <span class="nb">_</span> <span class="nb">_</span>            <span class="nb">_</span> <span class="nb">_</span>
  (<span class="nb">_____</span> <span class="k">\ </span>                / <span class="nb">__</span>)     / <span class="nb">__</span>)     (<span class="nb">_</span>) |          | | |
   <span class="nb">_____</span>) )<span class="nb">___</span> <span class="nb">___</span>   <span class="nb">___</span> <span class="nb">_</span>| |<span class="nb">__</span>    <span class="nb">_</span>| |<span class="nb">__</span> <span class="nb">_____</span> <span class="nb">_</span>| | <span class="nb">_____</span>  <span class="nb">__</span>| | |
  |  <span class="nb">____</span>/ <span class="nb">___</span>) <span class="nb">_</span> <span class="k">\ </span>/ <span class="nb">_</span> (<span class="nb">_</span>   <span class="nb">__</span>)  (<span class="nb">_</span>   <span class="nb">__</span>|<span class="nb">____</span> | | || <span class="nb">___</span> |/ <span class="nb">_</span>  |<span class="nb">_</span>|
  | |   | |  | |<span class="nb">_</span>| | |<span class="nb">_</span>| || |       | |  / <span class="nb">___</span> | | || <span class="nb">____</span>( (<span class="nb">_</span>| |<span class="nb">_</span>
  |<span class="nb">_</span>|   |<span class="nb">_</span>|   <span class="k">\_</span><span class="nb">__</span>/ <span class="k">\_</span><span class="nb">__</span>/ |<span class="nb">_</span>|       |<span class="nb">_</span>|  <span class="k">\_</span><span class="nb">____</span>|<span class="nb">_</span>|<span class="k">\_</span>)<span class="nb">_____</span>)<span class="k">\_</span><span class="nb">___</span>|<span class="nb">_</span>|


  Signal Name                 Dec        Hex                   Bin
  -------------------- ---------- ---------- ---------------------
  <span class="k">\a</span>                        15029       3ab5      0011101010110101
  <span class="k">\b</span>                         4099       1003      0001000000000011
  <span class="k">\ok</span>                           0          0                     0
  <span class="k">\p</span>                           31         1f      0000000000011111

yosys [primetest]&gt; sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0

9. Executing SAT pass (solving SAT problems in the circuit).
Full command line: sat -prove ok 1 -set p 31 -set a[15:8],b[15:8] 0

Setting up SAT problem:
Import set-constraint: <span class="k">\p</span> = 16&#39;0000000000011111
Import set-constraint: <span class="nb">{</span> <span class="k">\a</span> [15:8] <span class="k">\b</span> [15:8] <span class="nb">}</span> = 16&#39;0000000000000000
Final constraint equation: <span class="nb">{</span> <span class="k">\a</span> [15:8] <span class="k">\b</span> [15:8] <span class="k">\p</span> <span class="nb">}</span> = <span class="nb">{</span> 16&#39;0000000000000000 16&#39;0000000000011111 <span class="nb">}</span>
Imported 6 cells to SAT database.
Import proof-constraint: <span class="k">\ok</span> = 1&#39;1
Final proof equation: <span class="k">\ok</span> = 1&#39;1

Solving problem with 2790 variables and 8257 clauses..
SAT proof finished - no model found: SUCCESS!

                  /<span class="sb">$$</span><span class="s">$$</span><span class="sb">$$</span><span class="nb">      </span><span class="o">/</span><span class="s">$$</span><span class="sb">$$</span><span class="s">$$</span><span class="sb">$$</span><span class="nb">     </span><span class="o">/</span><span class="s">$$</span><span class="sb">$$</span><span class="s">$$$</span><span class="nb"></span>
<span class="nb">                 </span><span class="o">/</span><span class="s">$$</span><span class="nb">__  </span><span class="s">$$</span><span class="nb">    | </span><span class="s">$$</span><span class="nb">_____</span><span class="o">/</span><span class="nb">    | </span><span class="s">$$</span><span class="nb">__  </span><span class="s">$$</span><span class="nb"></span>
<span class="nb">                | </span><span class="s">$$</span><span class="nb">  </span><span class="nv">\ </span><span class="s">$$</span><span class="nb">    | </span><span class="s">$$</span><span class="nb">          | </span><span class="s">$$</span><span class="nb">  </span><span class="nv">\ </span><span class="s">$$</span><span class="nb"></span>
<span class="nb">                | </span><span class="s">$$</span><span class="nb">  | </span><span class="s">$$</span><span class="nb">    | </span><span class="s">$</span><span class="sb">$$</span><span class="s">$$</span>       | <span class="sb">$$</span><span class="nb">  | </span><span class="s">$$</span>
                | <span class="sb">$$</span><span class="nb">  | </span><span class="s">$$</span>    | <span class="sb">$$</span><span class="nb">__</span><span class="o">/</span><span class="nb">       | </span><span class="s">$$</span>  | <span class="sb">$$</span><span class="nb"></span>
<span class="nb">                | </span><span class="s">$$</span>/<span class="sb">$$</span><span class="nb"> </span><span class="s">$$</span>    | <span class="sb">$$</span><span class="nb">          | </span><span class="s">$$</span>  | <span class="sb">$$</span><span class="nb"></span>
<span class="nb">                |  </span><span class="s">$$</span><span class="sb">$$</span><span class="s">$$</span>/ /<span class="sb">$$</span><span class="nb">| </span><span class="s">$$</span><span class="sb">$$</span><span class="s">$$</span><span class="sb">$$</span><span class="nb"> </span><span class="o">/</span><span class="s">$$</span>| <span class="sb">$$</span><span class="s">$$</span><span class="sb">$$</span><span class="nb">$</span><span class="o">//</span><span class="s">$$</span>
                 <span class="k">\_</span><span class="nb">___</span> <span class="sb">$$</span><span class="nb">$|__</span><span class="o">/</span><span class="nb">|________</span><span class="o">/</span><span class="nb">|__</span><span class="o">/</span><span class="nb">|_______</span><span class="o">/</span><span class="nb">|__</span><span class="o">/</span><span class="nb"></span>
<span class="nb">                       </span><span class="nv">\_</span><span class="nb">_</span><span class="o">/</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nv">\caption</span><span class="nb">{Experiments with the miter circuit from Fig.~</span><span class="nv">\ref</span><span class="nb">{primetest}. The first attempt of proving that </span><span class="m">31</span><span class="nb"></span>
<span class="nb">is prime failed because the SAT solver found a creative way of factorizing </span><span class="m">31</span><span class="nb"> using integer overflow.}</span>
<span class="nv">\label</span><span class="nb">{primesat}</span>
<span class="nv">\end</span><span class="nb">{figure</span><span class="o">*</span><span class="nb">}</span>

<span class="nb">Often the opposite of the {</span><span class="nv">\tt</span><span class="nb"> eval} command is needed, i.e. the circuits</span>
<span class="nb">output is given and we want to find the matching input signals. For small</span>
<span class="nb">circuits with only a few input bits this can be accomplished by trying all</span>
<span class="nb">possible input combinations, as it is done by the {</span><span class="nv">\tt</span><span class="nb"> eval </span><span class="o">-</span><span class="nb">table} command.</span>
<span class="nb">For larger circuits however, Yosys provides the {</span><span class="nv">\tt</span><span class="nb"> sat} command that uses</span>
<span class="nb">a SAT </span><span class="nv">\cite</span><span class="nb">{CircuitSAT} solver </span><span class="nv">\cite</span><span class="nb">{MiniSAT} to solve this kind of problems.</span>

<span class="nb">The {</span><span class="nv">\tt</span><span class="nb"> sat} command works very similar to the {</span><span class="nv">\tt</span><span class="nb"> eval} command. The main</span>
<span class="nb">difference is that it is now also possible to set output values and find the</span>
<span class="nb">corresponding input values. For Example:</span>

<span class="nb">{</span><span class="nv">\scriptsize</span><span class="nb"></span>
<span class="nv">\begin</span><span class="nb">{verbatim}</span>
<span class="nb">   yosys </span><span class="o">[</span><span class="nb">selstage</span><span class="o">]</span><span class="nb">&gt; sat </span><span class="o">-</span><span class="nb">show s</span><span class="m">1</span><span class="nb">,s</span><span class="m">2</span><span class="nb">,d </span><span class="o">-</span><span class="nb">set s</span><span class="m">1</span><span class="nb"> s</span><span class="m">2</span><span class="nb"> </span><span class="o">-</span><span class="nb">set n</span><span class="m">2</span><span class="nb">,n</span><span class="m">1</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;b</span><span class="m">1001</span><span class="nb"></span>

<span class="nb">   </span><span class="m">11</span><span class="nb">. Executing SAT pass </span><span class="o">(</span><span class="nb">solving SAT problems in the circuit</span><span class="o">)</span><span class="nb">.</span>
<span class="nb">   Full command line: sat </span><span class="o">-</span><span class="nb">show s</span><span class="m">1</span><span class="nb">,s</span><span class="m">2</span><span class="nb">,d </span><span class="o">-</span><span class="nb">set s</span><span class="m">1</span><span class="nb"> s</span><span class="m">2</span><span class="nb"> </span><span class="o">-</span><span class="nb">set n</span><span class="m">2</span><span class="nb">,n</span><span class="m">1</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;b</span><span class="m">1001</span><span class="nb"></span>

<span class="nb">   Setting up SAT problem:</span>
<span class="nb">   Import set</span><span class="o">-</span><span class="nb">constraint: </span><span class="nv">\s</span><span class="m">1</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="nv">\s</span><span class="m">2</span><span class="nb"></span>
<span class="nb">   Import set</span><span class="o">-</span><span class="nb">constraint: { </span><span class="nv">\n</span><span class="m">2</span><span class="nb"> </span><span class="nv">\n</span><span class="m">1</span><span class="nb"> } </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">1001</span><span class="nb"></span>
<span class="nb">   Final constraint equation: { </span><span class="nv">\n</span><span class="m">2</span><span class="nb"> </span><span class="nv">\n</span><span class="m">1</span><span class="nb"> </span><span class="nv">\s</span><span class="m">1</span><span class="nb"> } </span><span class="o">=</span><span class="nb"> { </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">1001</span><span class="nb"> </span><span class="nv">\s</span><span class="m">2</span><span class="nb"> }</span>
<span class="nb">   Imported </span><span class="m">3</span><span class="nb"> cells to SAT database.</span>
<span class="nb">   Import show expression: { </span><span class="nv">\s</span><span class="m">1</span><span class="nb"> </span><span class="nv">\s</span><span class="m">2</span><span class="nb"> </span><span class="nv">\d</span><span class="nb"> }</span>

<span class="nb">   Solving problem with </span><span class="m">81</span><span class="nb"> variables and </span><span class="m">207</span><span class="nb"> clauses..</span>
<span class="nb">   SAT solving finished </span><span class="o">-</span><span class="nb"> model found:</span>

<span class="nb">     Signal Name                 Dec        Hex             Bin</span>
<span class="nb">     </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="nv">\d</span><span class="nb">                            </span><span class="m">9</span><span class="nb">          </span><span class="m">9</span><span class="nb">            </span><span class="m">1001</span><span class="nb"></span>
<span class="nb">     </span><span class="nv">\s</span><span class="m">1</span><span class="nb">                           </span><span class="m">0</span><span class="nb">          </span><span class="m">0</span><span class="nb">              </span><span class="m">00</span><span class="nb"></span>
<span class="nb">     </span><span class="nv">\s</span><span class="m">2</span><span class="nb">                           </span><span class="m">0</span><span class="nb">          </span><span class="m">0</span><span class="nb">              </span><span class="m">00</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{verbatim}</span>
<span class="nb">}</span>

<span class="nb">Note that the {</span><span class="nv">\tt</span><span class="nb"> sat} command supports signal names in both arguments</span>
<span class="nb">to the {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">set} option. In the above example we used {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">set s</span><span class="m">1</span><span class="nb"> s</span><span class="m">2</span><span class="nb">}</span>
<span class="nb">to constraint {</span><span class="nv">\tt</span><span class="nb"> s</span><span class="m">1</span><span class="nb">} and {</span><span class="nv">\tt</span><span class="nb"> s</span><span class="m">2</span><span class="nb">} to be equal. When more complex</span>
<span class="nb">constraints are needed, a wrapper circuit must be constructed that</span>
<span class="nb">checks the constraints and signals if the constraint was met using an</span>
<span class="nb">extra output port, which then can be forced to a value using the {</span><span class="nv">\tt</span><span class="nb"></span>
<span class="o">-</span><span class="nb">set} option. </span><span class="o">(</span><span class="nb">Such a circuit that contains the circuit under test</span>
<span class="nb">plus additional constraint checking circuitry is called a {</span><span class="nv">\it</span><span class="nb"> miter</span><span class="nv">\/</span><span class="nb">}</span>
<span class="nb">circuit.</span><span class="o">)</span><span class="nb"></span>

<span class="nb">Fig.~</span><span class="nv">\ref</span><span class="nb">{primetest} shows a miter circuit that is supposed to be used as a</span>
<span class="nb">prime number test. If {</span><span class="nv">\tt</span><span class="nb"> ok} is </span><span class="m">1</span><span class="nb"> for all input values {</span><span class="nv">\tt</span><span class="nb"> a} and {</span><span class="nv">\tt</span><span class="nb"> b}</span>
<span class="nb">for a given {</span><span class="nv">\tt</span><span class="nb"> p}, then {</span><span class="nv">\tt</span><span class="nb"> p} is prime, or at least that is the idea.</span>

<span class="nb">The Yosys shell session shown in Fig.~</span><span class="nv">\ref</span><span class="nb">{primesat} demonstrates that SAT</span>
<span class="nb">solvers can even find the unexpected solutions to a problem: Using integer</span>
<span class="nb">overflow there actually is a way of ``factorizing&#39;&#39; </span><span class="m">31</span><span class="nb">. The clean solution</span>
<span class="nb">would of course be to perform the test in </span><span class="m">32</span><span class="nb"> bits, for example by replacing</span>
<span class="nb">{</span><span class="nv">\tt</span><span class="nb"> p </span><span class="o">!=</span><span class="nb"> a</span><span class="o">*</span><span class="nb">b} in the miter with {</span><span class="nv">\tt</span><span class="nb"> p </span><span class="o">!=</span><span class="nb"> </span><span class="nv">\{</span><span class="m">16</span><span class="nb">&#39;d</span><span class="m">0</span><span class="nb">,a</span><span class="nv">\}</span><span class="o">*</span><span class="nb">b}, or by using a</span>
<span class="nb">temporary variable for the </span><span class="m">32</span><span class="nb"> bit product {</span><span class="nv">\tt</span><span class="nb"> a</span><span class="o">*</span><span class="nb">b}. But as </span><span class="m">31</span><span class="nb"> fits well into</span>
<span class="m">8</span><span class="nb"> bits </span><span class="o">(</span><span class="nb">and as the purpose of this document is to show off Yosys features</span><span class="o">)</span><span class="nb"></span>
<span class="nb">we can also simply force the upper </span><span class="m">8</span><span class="nb"> bits of {</span><span class="nv">\tt</span><span class="nb"> a} and {</span><span class="nv">\tt</span><span class="nb"> b} to zero for</span>
<span class="nb">the {</span><span class="nv">\tt</span><span class="nb"> sat} call, as is done in the second command in Fig.~</span><span class="nv">\ref</span><span class="nb">{primesat}</span>
<span class="o">(</span><span class="nb">line </span><span class="m">31</span><span class="o">)</span><span class="nb">.</span>

<span class="nb">The {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">prove} option used in this example works similar to {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">set}, but</span>
<span class="nb">tries to find a case in which the two arguments are not equal. If such a case is</span>
<span class="nb">not found, the property is proven to hold for all inputs that satisfy the other</span>
<span class="nb">constraints.</span>

<span class="nb">It might be worth noting, that SAT solvers are not particularly efficient at</span>
<span class="nb">factorizing large numbers. But if a small factorization problem occurs as</span>
<span class="nb">part of a larger circuit problem, the Yosys SAT solver is perfectly capable</span>
<span class="nb">of solving it.</span>

<span class="nv">\subsection</span><span class="nb">{Solving sequential SAT problems}</span>

<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">t</span><span class="o">!]</span><span class="nb"></span>
<span class="nv">\begin</span><span class="nb">{lstlisting}</span><span class="o">[</span><span class="nb">basicstyle</span><span class="o">=</span><span class="nv">\ttfamily\scriptsize</span><span class="o">]</span><span class="nb"></span>
<span class="nb">yosys </span><span class="o">[</span><span class="nb">memdemo</span><span class="o">]</span><span class="nb">&gt; sat </span><span class="o">-</span><span class="nb">seq </span><span class="m">6</span><span class="nb"> </span><span class="o">-</span><span class="nb">show y </span><span class="o">-</span><span class="nb">show d </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">init</span><span class="o">-</span><span class="nb">undef </span><span class="err">\</span><span class="nb"></span>
<span class="nb">	</span><span class="o">-</span><span class="nb">max_undef </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">4</span><span class="nb"> y </span><span class="m">1</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">5</span><span class="nb"> y </span><span class="m">2</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">6</span><span class="nb"> y </span><span class="m">3</span><span class="nb"></span>

<span class="m">6</span><span class="nb">. Executing SAT pass </span><span class="o">(</span><span class="nb">solving SAT problems in the circuit</span><span class="o">)</span><span class="nb">.</span>
<span class="nb">Full command line: sat </span><span class="o">-</span><span class="nb">seq </span><span class="m">6</span><span class="nb"> </span><span class="o">-</span><span class="nb">show y </span><span class="o">-</span><span class="nb">show d </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">init</span><span class="o">-</span><span class="nb">undef</span>
<span class="nb">	</span><span class="o">-</span><span class="nb">max_undef </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">4</span><span class="nb"> y </span><span class="m">1</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">5</span><span class="nb"> y </span><span class="m">2</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">6</span><span class="nb"> y </span><span class="m">3</span><span class="nb"></span>

<span class="nb">Setting up time step </span><span class="m">1</span><span class="nb">:</span>
<span class="nb">Final constraint equation: { } </span><span class="o">=</span><span class="nb"> { }</span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up time step </span><span class="m">2</span><span class="nb">:</span>
<span class="nb">Final constraint equation: { } </span><span class="o">=</span><span class="nb"> { }</span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up time step </span><span class="m">3</span><span class="nb">:</span>
<span class="nb">Final constraint equation: { } </span><span class="o">=</span><span class="nb"> { }</span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up time step </span><span class="m">4</span><span class="nb">:</span>
<span class="nb">Import set</span><span class="o">-</span><span class="nb">constraint for timestep: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0001</span><span class="nb"></span>
<span class="nb">Final constraint equation: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0001</span><span class="nb"></span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up time step </span><span class="m">5</span><span class="nb">:</span>
<span class="nb">Import set</span><span class="o">-</span><span class="nb">constraint for timestep: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0010</span><span class="nb"></span>
<span class="nb">Final constraint equation: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0010</span><span class="nb"></span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up time step </span><span class="m">6</span><span class="nb">:</span>
<span class="nb">Import set</span><span class="o">-</span><span class="nb">constraint for timestep: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0011</span><span class="nb"></span>
<span class="nb">Final constraint equation: </span><span class="nv">\y</span><span class="nb"> </span><span class="o">=</span><span class="nb"> </span><span class="m">4</span><span class="nb">&#39;</span><span class="m">0011</span><span class="nb"></span>
<span class="nb">Imported </span><span class="m">29</span><span class="nb"> cells to SAT database.</span>

<span class="nb">Setting up initial state:</span>
<span class="nb">Final constraint equation: { </span><span class="nv">\y</span><span class="nb"> </span><span class="nv">\s</span><span class="m">2</span><span class="nb"> </span><span class="nv">\s</span><span class="m">1</span><span class="nb"> </span><span class="nv">\mem</span><span class="o">[</span><span class="m">3</span><span class="o">]</span><span class="nb"> </span><span class="nv">\mem</span><span class="o">[</span><span class="m">2</span><span class="o">]</span><span class="nb"> </span><span class="nv">\mem</span><span class="o">[</span><span class="m">1</span><span class="o">]</span><span class="nb"></span>
<span class="nb">			</span><span class="nv">\mem</span><span class="o">[</span><span class="m">0</span><span class="o">]</span><span class="nb"> } </span><span class="o">=</span><span class="nb"> </span><span class="m">24</span><span class="nb">&#39;xxxxxxxxxxxxxxxxxxxxxxxx</span>

<span class="nb">Import show expression: </span><span class="nv">\y</span><span class="nb"></span>
<span class="nb">Import show expression: </span><span class="nv">\d</span><span class="nb"></span>

<span class="nb">Solving problem with </span><span class="m">10322</span><span class="nb"> variables and </span><span class="m">27881</span><span class="nb"> clauses..</span>
<span class="nb">SAT model found. maximizing number of undefs.</span>
<span class="nb">SAT solving finished </span><span class="o">-</span><span class="nb"> model found:</span>

<span class="nb">  Time Signal Name                 Dec        Hex             Bin</span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">  init </span><span class="nv">\mem</span><span class="o">[</span><span class="m">0</span><span class="o">]</span><span class="nb">                      </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  init </span><span class="nv">\mem</span><span class="o">[</span><span class="m">1</span><span class="o">]</span><span class="nb">                      </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  init </span><span class="nv">\mem</span><span class="o">[</span><span class="m">2</span><span class="o">]</span><span class="nb">                      </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  init </span><span class="nv">\mem</span><span class="o">[</span><span class="m">3</span><span class="o">]</span><span class="nb">                      </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  init </span><span class="nv">\s</span><span class="m">1</span><span class="nb">                          </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">              xx</span>
<span class="nb">  init </span><span class="nv">\s</span><span class="m">2</span><span class="nb">                          </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">              xx</span>
<span class="nb">  init </span><span class="nv">\y</span><span class="nb">                           </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">1</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                            </span><span class="m">0</span><span class="nb">          </span><span class="m">0</span><span class="nb">            </span><span class="m">0000</span><span class="nb"></span>
<span class="nb">     </span><span class="m">1</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                           </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">2</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                            </span><span class="m">1</span><span class="nb">          </span><span class="m">1</span><span class="nb">            </span><span class="m">0001</span><span class="nb"></span>
<span class="nb">     </span><span class="m">2</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                           </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">3</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                            </span><span class="m">2</span><span class="nb">          </span><span class="m">2</span><span class="nb">            </span><span class="m">0010</span><span class="nb"></span>
<span class="nb">     </span><span class="m">3</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                            </span><span class="m">0</span><span class="nb">          </span><span class="m">0</span><span class="nb">            </span><span class="m">0000</span><span class="nb"></span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">4</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                            </span><span class="m">3</span><span class="nb">          </span><span class="m">3</span><span class="nb">            </span><span class="m">0011</span><span class="nb"></span>
<span class="nb">     </span><span class="m">4</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                            </span><span class="m">1</span><span class="nb">          </span><span class="m">1</span><span class="nb">            </span><span class="m">0001</span><span class="nb"></span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">5</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                           </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            </span><span class="m">001</span><span class="nb">x</span>
<span class="nb">     </span><span class="m">5</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                            </span><span class="m">2</span><span class="nb">          </span><span class="m">2</span><span class="nb">            </span><span class="m">0010</span><span class="nb"></span>
<span class="nb">  </span><span class="o">----</span><span class="nb"> </span><span class="o">--------------------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">----------</span><span class="nb"> </span><span class="o">---------------</span><span class="nb"></span>
<span class="nb">     </span><span class="m">6</span><span class="nb"> </span><span class="nv">\d</span><span class="nb">                           </span><span class="o">--</span><span class="nb">         </span><span class="o">--</span><span class="nb">            xxxx</span>
<span class="nb">     </span><span class="m">6</span><span class="nb"> </span><span class="nv">\y</span><span class="nb">                            </span><span class="m">3</span><span class="nb">          </span><span class="m">3</span><span class="nb">            </span><span class="m">0011</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nv">\caption</span><span class="nb">{Solving a sequential SAT problem in the {</span><span class="nv">\tt</span><span class="nb"> memdemo} module from Fig.~</span><span class="nv">\ref</span><span class="nb">{memdemo_src}.}</span>
<span class="nv">\label</span><span class="nb">{memdemo_sat}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nb">The SAT solver functionality in Yosys can not only be used to solve</span>
<span class="nb">combinatorial problems, but can also solve sequential problems. Let&#39;s consider</span>
<span class="nb">the entire {</span><span class="nv">\tt</span><span class="nb"> memdemo} module from Fig.~</span><span class="nv">\ref</span><span class="nb">{memdemo_src} and suppose we</span>
<span class="nb">want to know which sequence of input values for {</span><span class="nv">\tt</span><span class="nb"> d} will cause the output</span>
<span class="nb">{</span><span class="nv">\tt</span><span class="nb"> y} to produce the sequence </span><span class="m">1</span><span class="nb">, </span><span class="m">2</span><span class="nb">, </span><span class="m">3</span><span class="nb"> from any initial state.</span>
<span class="nb">Fig.~</span><span class="nv">\ref</span><span class="nb">{memdemo_sat} show the solution to this question, as produced by</span>
<span class="nb">the following command:</span>

<span class="nv">\begin</span><span class="nb">{verbatim}</span>
<span class="nb">   sat </span><span class="o">-</span><span class="nb">seq </span><span class="m">6</span><span class="nb"> </span><span class="o">-</span><span class="nb">show y </span><span class="o">-</span><span class="nb">show d </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">init</span><span class="o">-</span><span class="nb">undef </span><span class="err">\</span><span class="nb"></span>
<span class="nb">     </span><span class="o">-</span><span class="nb">max_undef </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">4</span><span class="nb"> y </span><span class="m">1</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">5</span><span class="nb"> y </span><span class="m">2</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at </span><span class="m">6</span><span class="nb"> y </span><span class="m">3</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{verbatim}</span>

<span class="nb">The {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">seq </span><span class="m">6</span><span class="nb">} option instructs the {</span><span class="nv">\tt</span><span class="nb"> sat} command to solve a sequential</span>
<span class="nb">problem in </span><span class="m">6</span><span class="nb"> time steps. </span><span class="o">(</span><span class="nb">Experiments with lower number of steps have show that</span>
<span class="nb">at least </span><span class="m">3</span><span class="nb"> cycles are necessary to bring the circuit in a state from which</span>
<span class="nb">the sequence </span><span class="m">1</span><span class="nb">, </span><span class="m">2</span><span class="nb">, </span><span class="m">3</span><span class="nb"> can be produced.</span><span class="o">)</span><span class="nb"></span>

<span class="nb">The {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">init</span><span class="o">-</span><span class="nb">undef} option tells the {</span><span class="nv">\tt</span><span class="nb"> sat} command to initialize</span>
<span class="nb">all registers to the undef </span><span class="o">(</span><span class="nb">{</span><span class="nv">\tt</span><span class="nb"> x}</span><span class="o">)</span><span class="nb"> state. The way the {</span><span class="nv">\tt</span><span class="nb"> x} state</span>
<span class="nb">is treated in Verilog will ensure that the solution will work for any</span>
<span class="nb">initial state.</span>

<span class="nb">The {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">max</span><span class="nv">\_</span><span class="nb">undef} option instructs the {</span><span class="nv">\tt</span><span class="nb"> sat} command to find a solution</span>
<span class="nb">with a maximum number of undefs. This way we can see clearly which inputs bits</span>
<span class="nb">are relevant to the solution.</span>

<span class="nb">Finally the three {</span><span class="nv">\tt</span><span class="nb"> </span><span class="o">-</span><span class="nb">set</span><span class="o">-</span><span class="nb">at} options add constraints for the {</span><span class="nv">\tt</span><span class="nb"> y}</span>
<span class="nb">signal to play the </span><span class="m">1</span><span class="nb">, </span><span class="m">2</span><span class="nb">, </span><span class="m">3</span><span class="nb"> sequence, starting with time step </span><span class="m">4</span><span class="nb">.</span>

<span class="nb">It is not surprising that the solution sets {</span><span class="nv">\tt</span><span class="nb"> d </span><span class="o">=</span><span class="nb"> </span><span class="m">0</span><span class="nb">} in the first step, as</span>
<span class="nb">this is the only way of setting the {</span><span class="nv">\tt</span><span class="nb"> s</span><span class="m">1</span><span class="nb">} and {</span><span class="nv">\tt</span><span class="nb"> s</span><span class="m">2</span><span class="nb">} registers to a known</span>
<span class="nb">value. The input values for the other steps are a bit harder to work out</span>
<span class="nb">manually, but the SAT solver finds the correct solution in an instant.</span>

<span class="nv">\medskip</span><span class="nb"></span>

<span class="nb">There is much more to write about the {</span><span class="nv">\tt</span><span class="nb"> sat} command. For example, there is</span>
<span class="nb">a set of options that can be used to performs sequential proofs using temporal</span>
<span class="nb">induction </span><span class="nv">\cite</span><span class="nb">{tip}. The command {</span><span class="nv">\tt</span><span class="nb"> help sat} can be used to print a list</span>
<span class="nb">of all options with short descriptions of their functions.</span>

<span class="nv">\section</span><span class="nb">{Conclusion}</span>
<span class="nv">\label</span><span class="nb">{conclusion}</span>

<span class="nb">Yosys provides a wide range of functions to analyze and investigate designs. For</span>
<span class="nb">many cases it is sufficient to simply display circuit diagrams, maybe use some</span>
<span class="nb">additional commands to narrow the scope of the circuit diagrams to the interesting</span>
<span class="nb">parts of the circuit. But some cases require more than that. For this applications</span>
<span class="nb">Yosys provides commands that can be used to further inspect the behavior of the</span>
<span class="nb">circuit, either by evaluating which output values are generated from certain input values</span>
<span class="o">(</span><span class="nb">{</span><span class="nv">\tt</span><span class="nb"> eval}</span><span class="o">)</span><span class="nb"> or by evaluation which input values and initial conditions can result</span>
<span class="nb">in a certain behavior at the outputs </span><span class="o">(</span><span class="nb">{</span><span class="nv">\tt</span><span class="nb"> sat}</span><span class="o">)</span><span class="nb">. The SAT command can even be used</span>
<span class="nb">to prove </span><span class="o">(</span><span class="nb">or disprove</span><span class="o">)</span><span class="nb"> theorems regarding the circuit, in more advanced cases</span>
<span class="nb">with the additional help of a miter circuit.</span>

<span class="nb">This features can be powerful tools for the circuit designer using Yosys as a</span>
<span class="nb">utility for building circuits and the software developer using Yosys as a</span>
<span class="nb">framework for new algorithms alike.</span>

<span class="nv">\begin</span><span class="nb">{thebibliography}{</span><span class="m">9</span><span class="nb">}</span>

<span class="nv">\bibitem</span><span class="nb">{yosys}</span>
<span class="nb">Clifford Wolf. The Yosys Open SYnthesis Suite.</span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">www.clifford.at</span><span class="o">/</span><span class="nb">yosys</span><span class="o">/</span><span class="nb">}</span>

<span class="nv">\bibitem</span><span class="nb">{graphviz}</span>
<span class="nb">Graphviz </span><span class="o">-</span><span class="nb"> Graph Visualization Software.</span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">www.graphviz.org</span><span class="o">/</span><span class="nb">}</span>

<span class="nv">\bibitem</span><span class="nb">{xdot}</span>
<span class="nb">xdot.py </span><span class="o">-</span><span class="nb"> an interactive viewer for graphs written in Graphviz&#39;s dot language.</span>
<span class="nv">\url</span><span class="nb">{https:</span><span class="o">//</span><span class="nb">github.com</span><span class="o">/</span><span class="nb">jrfonseca</span><span class="o">/</span><span class="nb">xdot.py}</span>

<span class="nv">\bibitem</span><span class="nb">{CircuitSAT}</span>
<span class="nb">{</span><span class="nv">\it</span><span class="nb"> Circuit satisfiability problem} on Wikipedia</span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">en.wikipedia.org</span><span class="o">/</span><span class="nb">wiki</span><span class="o">/</span><span class="nb">Circuit_satisfiability}</span>

<span class="nv">\bibitem</span><span class="nb">{MiniSAT}</span>
<span class="nb">MiniSat: a minimalistic open</span><span class="o">-</span><span class="nb">source SAT solver.</span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">minisat.se</span><span class="o">/</span><span class="nb">}</span>

<span class="nv">\bibitem</span><span class="nb">{tip}</span>
<span class="nb">Niklas Een and Niklas S</span><span class="nv">\&quot;</span><span class="nb">orensson </span><span class="o">(</span><span class="m">2003</span><span class="o">)</span><span class="nb">.</span>
<span class="nb">Temporal Induction by Incremental SAT Solving.</span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">citeseerx.ist.psu.edu</span><span class="o">/</span><span class="nb">viewdoc</span><span class="o">/</span><span class="nb">summary?doi</span><span class="o">=</span><span class="m">10</span><span class="nb">.</span><span class="m">1</span><span class="nb">.</span><span class="m">1</span><span class="nb">.</span><span class="m">4</span><span class="nb">.</span><span class="m">8161</span><span class="nb">}</span>

<span class="nv">\end</span><span class="nb">{thebibliography}</span>

<span class="nv">\end</span><span class="nb">{document}</span>
</pre></div>
</code></pre></td></tr></table>
</div> <!-- class=content -->
<div class='footer'>generated by <a href='https://git.zx2c4.com/cgit/about/'>cgit v1.2.3</a> (<a href='https://git-scm.com/'>git 2.25.1</a>) at 2025-09-01 22:19:40 +0000</div>
</div> <!-- id=cgit -->
</body>
</html>
