<!DOCTYPE html>
<html lang='en'>
<head>
<title>CHAPTER_Approach.tex « manual - iCE40/yosys - clone of https://github.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/CHAPTER_Approach.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='f7fb21f1853ec6a0a711624e4f53a75321639b18'/><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=f7fb21f1853ec6a0a711624e4f53a75321639b18'>refs</a><a href='/cgit/iCE40/yosys/log/manual/CHAPTER_Approach.tex'>log</a><a class='active' href='/cgit/iCE40/yosys/tree/manual/CHAPTER_Approach.tex?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>tree</a><a href='/cgit/iCE40/yosys/commit/manual/CHAPTER_Approach.tex?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>commit</a><a href='/cgit/iCE40/yosys/diff/manual/CHAPTER_Approach.tex?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>diff</a><a href='/cgit/iCE40/yosys/stats/manual/CHAPTER_Approach.tex'>stats</a></td><td class='form'><form class='right' method='get' action='/cgit/iCE40/yosys/log/manual/CHAPTER_Approach.tex'>
<input type='hidden' name='id' value='f7fb21f1853ec6a0a711624e4f53a75321639b18'/><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=f7fb21f1853ec6a0a711624e4f53a75321639b18'>root</a>/<a href='/cgit/iCE40/yosys/tree/manual?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>manual</a>/<a href='/cgit/iCE40/yosys/tree/manual/CHAPTER_Approach.tex?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>CHAPTER_Approach.tex</a></div><div class='content'>blob: 691225805996fd72b6420a2f2609f1213ba2ffa0 (<a href='/cgit/iCE40/yosys/plain/manual/CHAPTER_Approach.tex?id=f7fb21f1853ec6a0a711624e4f53a75321639b18'>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>
</pre></td>
<td class='lines'><pre><code>' 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>
</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">\lstset</span><span class="nb">{</span>basicstyle=<span class="k">\ttfamily</span>,frame=trBL,xleftmargin=2em,xrightmargin=1em,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 012: <span class="k">\\</span> Converting Verilog to BTOR<span class="nb">}</span>
<span class="k">\author</span><span class="nb">{</span>Ahmed Irfan and Clifford Wolf <span class="k">\\</span> April 2015<span class="nb">}</span>
<span class="k">\maketitle</span>

<span class="k">\begin</span><span class="nb">{</span>abstract<span class="nb">}</span>
Verilog-2005 is a powerful Hardware Description Language (HDL) that
can be used to easily create complex designs from small HDL code.
BTOR~<span class="k">\cite</span><span class="nb">{</span>btor<span class="nb">}</span> is a bit-precise word-level format for model
checking.  It is a simple format and easy to parse. It allows to model
the model checking problem over the theory of bit-vectors with
one-dimensional arrays, thus enabling to model Verilog designs with
registers and memories.  Yosys~<span class="k">\cite</span><span class="nb">{</span>yosys<span class="nb">}</span> is an Open-Source Verilog
synthesis tool that can be used to convert Verilog designs with simple
assertions to BTOR format.

<span class="k">\end</span><span class="nb">{</span>abstract<span class="nb">}</span>

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

Yosys written in C++ (using features from C++11) and is tested on
modern Linux.  It should compile fine on most UNIX systems with a
C++11 compiler. The README file contains useful information on
building Yosys and its prerequisites.

Yosys is a large and feature-rich program with some dependencies. For
this work, we may deactivate other extra features such as <span class="nb">{</span><span class="k">\tt</span> TCL<span class="nb">}</span>
and <span class="nb">{</span><span class="k">\tt</span> ABC<span class="nb">}</span> support in the <span class="nb">{</span><span class="k">\tt</span> Makefile<span class="nb">}</span>.

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

This Application Note is based on GIT Rev. <span class="nb">{</span><span class="k">\tt</span> 082550f<span class="nb">}</span> from
2015-04-04 of Yosys~<span class="k">\cite</span><span class="nb">{</span>yosys<span class="nb">}</span>.

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

We assume that the Verilog design is synthesizable and we also assume
that the design does not have multi-dimensional memories.  As BTOR
implicitly initializes registers to zero value and memories stay
uninitilized, we assume that the Verilog design does
not contain initial blocks. For more details about the BTOR format,
please refer to~<span class="k">\cite</span><span class="nb">{</span>btor<span class="nb">}</span>.

We provide a shell script <span class="nb">{</span><span class="k">\tt</span> verilog2btor.sh<span class="nb">}</span> which can be used to
convert a Verilog design to BTOR. The script can be found in the
<span class="nb">{</span><span class="k">\tt</span> backends/btor<span class="nb">}</span> directory. The following example shows its usage:

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[H]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[language=sh,numbers=none]
verilog2btor.sh fsm.v fsm.btor test
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
 <span class="k">\renewcommand</span><span class="nb">{</span><span class="k">\figurename</span><span class="nb">}{</span>Listing<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Using verilog2btor script<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

The script <span class="nb">{</span><span class="k">\tt</span> verilog2btor.sh<span class="nb">}</span> takes three parameters.  In the above
example, the first parameter <span class="nb">{</span><span class="k">\tt</span> fsm.v<span class="nb">}</span> is the input design, the second
parameter <span class="nb">{</span><span class="k">\tt</span> fsm.btor<span class="nb">}</span> is the file name of BTOR output, and the third
parameter <span class="nb">{</span><span class="k">\tt</span> test<span class="nb">}</span> is the name of top module in the design.

To specify the properties (that need to be checked), we have two
options:
<span class="k">\begin</span><span class="nb">{</span>itemize<span class="nb">}</span>
<span class="k">\item</span> We can use the Verilog <span class="nb">{</span><span class="k">\tt</span> assert<span class="nb">}</span> statement in the procedural block
  or module body of the Verilog design, as shown in
  Listing~<span class="k">\ref</span><span class="nb">{</span>specifying<span class="nb">_</span>property<span class="nb">_</span>assert<span class="nb">}</span>. This is the preferred option.
<span class="k">\item</span> We can use a single-bit output wire, whose name starts with
  <span class="nb">{</span><span class="k">\tt</span> safety<span class="nb">}</span>.  The value of this output wire needs to be driven low
  when the property is met, i.e. the solver will try to find a model
  that makes the safety pin go high. This is demonstrated in
  Listing~<span class="k">\ref</span><span class="nb">{</span>specifying<span class="nb">_</span>property<span class="nb">_</span>output<span class="nb">}</span>.
<span class="k">\end</span><span class="nb">{</span>itemize<span class="nb">}</span>

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[H]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[language=Verilog,numbers=none]
module test(input clk, input rst, output y);

  reg [2:0] state;

  always @(posedge clk) begin
    if (rst || state == 3) begin
      state &lt;= 0;
    end else begin
      assert(state &lt; 3);
      state &lt;= state + 1;
    end
  end

  assign y = state[2];

  assert property (y !== 1&#39;b1);

endmodule
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\renewcommand</span><span class="nb">{</span><span class="k">\figurename</span><span class="nb">}{</span>Listing<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Specifying property in Verilog design with <span class="nb">{</span><span class="k">\tt</span> assert<span class="nb">}}</span>
<span class="k">\label</span><span class="nb">{</span>specifying<span class="nb">_</span>property<span class="nb">_</span>assert<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>[H]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[language=Verilog,numbers=none]
module test(input clk, input rst,
    output y, output safety1);

  reg [2:0] state;

  always @(posedge clk) begin
    if (rst || state == 3)
      state &lt;= 0;
    else
      state &lt;= state + 1;
  end

  assign y = state[2];

  assign safety1 = !(y !== 1&#39;b1);

endmodule
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\renewcommand</span><span class="nb">{</span><span class="k">\figurename</span><span class="nb">}{</span>Listing<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Specifying property in Verilog design with output wire<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>specifying<span class="nb">_</span>property<span class="nb">_</span>output<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

We can run Boolector~<span class="k">\cite</span><span class="nb">{</span>boolector<span class="nb">}</span>~<span class="s">$</span><span class="m">1</span><span class="nb">.</span><span class="m">4</span><span class="nb">.</span><span class="m">1</span><span class="s">$</span><span class="k">\footnote</span><span class="nb">{</span>
Newer version of Boolector do not support sequential models.
Boolector 1.4.1 can be built with picosat-951. Newer versions
of picosat have an incompatible API.<span class="nb">}</span> on the generated BTOR
file:

<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[H]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[language=sh,numbers=none]
<span class="s">$</span><span class="nb"> boolector fsm.btor </span>
<span class="nb">unsat</span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nb"> </span><span class="nv">\renewcommand</span><span class="nb">{</span><span class="nv">\figurename</span><span class="nb">}{Listing}</span>
<span class="nv">\caption</span><span class="nb">{Running boolector on BTOR file}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nb">We can also use nuXmv~</span><span class="nv">\cite</span><span class="nb">{nuxmv}, but on BTOR designs it does not</span>
<span class="nb">support memories yet. With the next release of nuXmv, we will be also</span>
<span class="nb">able to verify designs with memories.</span>

<span class="nv">\section</span><span class="nb">{Detailed Flow}</span>

<span class="nb">Yosys is able to synthesize Verilog designs up to the gate level.</span>
<span class="nb">We are interested in keeping registers and memories when synthesizing</span>
<span class="nb">the design. For this purpose, we describe a customized Yosys synthesis</span>
<span class="nb">flow, that is also provided by the {</span><span class="nv">\tt</span><span class="nb"> verilog</span><span class="m">2</span><span class="nb">btor.sh} script.</span>
<span class="nb">Listing~</span><span class="nv">\ref</span><span class="nb">{btor_script_memory} shows the Yosys commands that are</span>
<span class="nb">executed by {</span><span class="nv">\tt</span><span class="nb"> verilog</span><span class="m">2</span><span class="nb">btor.sh}.</span>

<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">H</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">language</span><span class="o">=</span><span class="nb">sh</span><span class="o">]</span><span class="nb"></span>
<span class="nb">read_verilog </span><span class="o">-</span><span class="nb">sv </span><span class="s">$</span>1; 
hierarchy -top <span class="s">$</span><span class="m">3</span><span class="nb">; hierarchy </span><span class="o">-</span><span class="nb">libdir </span><span class="s">$</span>DIR; 
hierarchy -check; 
proc; opt; 
opt<span class="nb">_</span>const -mux<span class="nb">_</span>undef; opt;
rename -hide;;;
splice; opt;
memory<span class="nb">_</span>dff -wr<span class="nb">_</span>only; memory<span class="nb">_</span>collect;;
flatten;;
memory<span class="nb">_</span>unpack; 
splitnets -driver;
setundef -zero -undriven;
opt;;;
write<span class="nb">_</span>btor <span class="s">$</span><span class="m">2</span><span class="nb">;</span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nb"> </span><span class="nv">\renewcommand</span><span class="nb">{</span><span class="nv">\figurename</span><span class="nb">}{Listing}</span>
<span class="nv">\caption</span><span class="nb">{Synthesis Flow for BTOR with memories}</span>
<span class="nv">\label</span><span class="nb">{btor_script_memory}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nb">Here is short description of what is happening in the script line by</span>
<span class="nb">line:</span>

<span class="nv">\begin</span><span class="nb">{enumerate}</span>
<span class="nv">\item</span><span class="nb"> Reading the input file.</span>
<span class="nv">\item</span><span class="nb"> Setting the top module in the hierarchy and trying to read</span>
<span class="nb">  automatically the files which are given as {</span><span class="nv">\tt</span><span class="nb"> include} in the file</span>
<span class="nb">  read in first line.</span>
<span class="nv">\item</span><span class="nb"> Checking the design hierarchy.</span>
<span class="nv">\item</span><span class="nb"> Converting processes to multiplexers </span><span class="o">(</span><span class="nb">muxs</span><span class="o">)</span><span class="nb"> and flip</span><span class="o">-</span><span class="nb">flops.</span>
<span class="nv">\item</span><span class="nb"> Removing undef signals from muxs.</span>
<span class="nv">\item</span><span class="nb"> Hiding all signal names that are not used as module ports.</span>
<span class="nv">\item</span><span class="nb"> Explicit type conversion, by introducing slice and concat cells</span>
<span class="nb">  in the circuit.</span>
<span class="nv">\item</span><span class="nb"> Converting write memories to synchronous memories, and</span>
<span class="nb">  collecting the memories to multi</span><span class="o">-</span><span class="nb">port memories.</span>
<span class="nv">\item</span><span class="nb"> Flattening the design to get only one module.</span>
<span class="nv">\item</span><span class="nb"> Separating read and write memories.</span>
<span class="nv">\item</span><span class="nb"> Splitting the signals that are partially assigned </span>
<span class="nv">\item</span><span class="nb"> Setting undef to zero value.</span>
<span class="nv">\item</span><span class="nb"> Final optimization pass.</span>
<span class="nv">\item</span><span class="nb"> Writing BTOR file.</span>
<span class="nv">\end</span><span class="nb">{enumerate}</span>

<span class="nb">For detailed description of the commands mentioned above, please refer</span>
<span class="nb">to the Yosys documentation, or run {</span><span class="nv">\tt</span><span class="nb"> yosys </span><span class="o">-</span><span class="nb">h </span><span class="nv">\it</span><span class="nb"> command</span><span class="nv">\_</span><span class="nb">name}.</span>

<span class="nb">The script presented earlier can be easily modified to have a BTOR</span>
<span class="nb">file that does not contain memories. This is done by removing the line</span>
<span class="nb">number~</span><span class="m">8</span><span class="nb"> and </span><span class="m">10</span><span class="nb">, and introduces a new command {</span><span class="nv">\tt</span><span class="nb"> memory} at line</span>
<span class="nb">number~</span><span class="m">8</span><span class="nb">. Listing~</span><span class="nv">\ref</span><span class="nb">{btor_script_without_memory} shows the</span>
<span class="nb">modified Yosys script file:</span>

<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">H</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">language</span><span class="o">=</span><span class="nb">sh,numbers</span><span class="o">=</span><span class="nb">none</span><span class="o">]</span><span class="nb"></span>
<span class="nb">read_verilog </span><span class="o">-</span><span class="nb">sv </span><span class="s">$</span>1; 
hierarchy -top <span class="s">$</span><span class="m">3</span><span class="nb">; hierarchy </span><span class="o">-</span><span class="nb">libdir </span><span class="s">$</span>DIR; 
hierarchy -check; 
proc; opt; 
opt<span class="nb">_</span>const -mux<span class="nb">_</span>undef; opt;
rename -hide;;;
splice; opt;
memory;;
flatten;;
splitnets -driver;
setundef -zero -undriven;
opt;;;
write<span class="nb">_</span>btor <span class="s">$</span><span class="m">2</span><span class="nb">;</span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nb"> </span><span class="nv">\renewcommand</span><span class="nb">{</span><span class="nv">\figurename</span><span class="nb">}{Listing}</span>
<span class="nv">\caption</span><span class="nb">{Synthesis Flow for BTOR without memories}</span>
<span class="nv">\label</span><span class="nb">{btor_script_without_memory}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nv">\section</span><span class="nb">{Example}</span>

<span class="nb">Here is an example Verilog design that we want to convert to BTOR:</span>

<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">H</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">language</span><span class="o">=</span><span class="nb">Verilog,numbers</span><span class="o">=</span><span class="nb">none</span><span class="o">]</span><span class="nb"></span>
<span class="nb">module array</span><span class="o">(</span><span class="nb">input clk</span><span class="o">)</span><span class="nb">;</span>

<span class="nb">  reg </span><span class="o">[</span><span class="m">7</span><span class="nb">:</span><span class="m">0</span><span class="o">]</span><span class="nb"> counter;</span>
<span class="nb">  reg </span><span class="o">[</span><span class="m">7</span><span class="nb">:</span><span class="m">0</span><span class="o">]</span><span class="nb"> mem </span><span class="o">[</span><span class="m">7</span><span class="nb">:</span><span class="m">0</span><span class="o">]</span><span class="nb">;</span>

<span class="nb">  always @</span><span class="o">(</span><span class="nb">posedge clk</span><span class="o">)</span><span class="nb"> begin</span>
<span class="nb">    counter &lt;</span><span class="o">=</span><span class="nb"> counter </span><span class="o">+</span><span class="nb"> </span><span class="m">8</span><span class="nb">&#39;d</span><span class="m">1</span><span class="nb">;</span>
<span class="nb">    mem</span><span class="o">[</span><span class="nb">counter</span><span class="o">]</span><span class="nb"> &lt;</span><span class="o">=</span><span class="nb"> counter;</span>
<span class="nb">  end</span>

<span class="nb">  assert property </span><span class="o">(!(</span><span class="nb">counter &gt; </span><span class="m">8</span><span class="nb">&#39;d</span><span class="m">0</span><span class="o">)</span><span class="nb"> || </span>
<span class="nb">    mem</span><span class="o">[</span><span class="nb">counter </span><span class="o">-</span><span class="nb"> </span><span class="m">8</span><span class="nb">&#39;d</span><span class="m">1</span><span class="o">]</span><span class="nb"> </span><span class="o">==</span><span class="nb"> counter </span><span class="o">-</span><span class="nb"> </span><span class="m">8</span><span class="nb">&#39;d</span><span class="m">1</span><span class="o">)</span><span class="nb">;</span>

<span class="nb">endmodule</span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nv">\renewcommand</span><span class="nb">{</span><span class="nv">\figurename</span><span class="nb">}{Listing}</span>
<span class="nv">\caption</span><span class="nb">{Example </span><span class="o">-</span><span class="nb"> Verilog Design}</span>
<span class="nv">\label</span><span class="nb">{example_verilog}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nb">The generated BTOR file that contain memories, using the script shown</span>
<span class="nb">in Listing~</span><span class="nv">\ref</span><span class="nb">{btor_script_memory}:</span>
<span class="nv">\begin</span><span class="nb">{figure}</span><span class="o">[</span><span class="nb">H</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">numbers</span><span class="o">=</span><span class="nb">none</span><span class="o">]</span><span class="nb"></span>
<span class="m">1</span><span class="nb"> var </span><span class="m">1</span><span class="nb"> clk</span>
<span class="m">2</span><span class="nb"> array </span><span class="m">8</span><span class="nb"> </span><span class="m">3</span><span class="nb"></span>
<span class="m">3</span><span class="nb"> var </span><span class="m">8</span><span class="nb"> </span><span class="s">$</span>auto<span class="s">$</span><span class="nb">rename.cc:</span><span class="m">150</span><span class="nb">:execute</span><span class="s">$</span>20
4 const 8 00000001
5 sub 8 3 4
6 slice 3 5 2 0
7 read 8 2 6
8 slice 3 3 2 0
9 add 8 3 4
10 const 8 00000000
11 ugt 1 3 10
12 not 1 11
13 const 8 11111111
14 slice 1 13 0 0
15 one 1
16 eq 1 1 15
17 and 1 16 14
18 write 8 3 2 8 3
19 acond 8 3 17 18 2
20 anext 8 3 2 19
21 eq 1 7 5
22 or 1 12 21
23 const 1 1
24 one 1
25 eq 1 23 24
26 cond 1 25 22 24
27 root 1 -26
28 cond 8 1 9 3
29 next 8 3 28
<span class="k">\end</span><span class="nb">{</span>lstlisting<span class="nb">}</span>
<span class="k">\renewcommand</span><span class="nb">{</span><span class="k">\figurename</span><span class="nb">}{</span>Listing<span class="nb">}</span>
<span class="k">\caption</span><span class="nb">{</span>Example - Converted BTOR with memory<span class="nb">}</span>
<span class="k">\label</span><span class="nb">{</span>example<span class="nb">_</span>btor<span class="nb">}</span>
<span class="k">\end</span><span class="nb">{</span>figure<span class="nb">}</span>

And the BTOR file obtained by the script shown in
Listing~<span class="k">\ref</span><span class="nb">{</span>btor<span class="nb">_</span>script<span class="nb">_</span>without<span class="nb">_</span>memory<span class="nb">}</span>, which expands the memory
into individual elements:
<span class="k">\begin</span><span class="nb">{</span>figure<span class="nb">}</span>[H]
<span class="k">\begin</span><span class="nb">{</span>lstlisting<span class="nb">}</span>[numbers=none,escapechar=@]
1 var 1 clk
2 var 8 mem[0]
3 var 8 <span class="s">$</span><span class="nb">auto</span><span class="s">$</span>rename.cc:150:execute<span class="s">$</span><span class="m">20</span><span class="nb"></span>
<span class="m">4</span><span class="nb"> slice </span><span class="m">3</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">2</span><span class="nb"> </span><span class="m">0</span><span class="nb"></span>
<span class="m">5</span><span class="nb"> slice </span><span class="m">1</span><span class="nb"> </span><span class="m">4</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">6</span><span class="nb"> not </span><span class="m">1</span><span class="nb"> </span><span class="m">5</span><span class="nb"></span>
<span class="m">7</span><span class="nb"> slice </span><span class="m">1</span><span class="nb"> </span><span class="m">4</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">8</span><span class="nb"> not </span><span class="m">1</span><span class="nb"> </span><span class="m">7</span><span class="nb"></span>
<span class="m">9</span><span class="nb"> slice </span><span class="m">1</span><span class="nb"> </span><span class="m">4</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">10</span><span class="nb"> not </span><span class="m">1</span><span class="nb"> </span><span class="m">9</span><span class="nb"></span>
<span class="m">11</span><span class="nb"> and </span><span class="m">1</span><span class="nb"> </span><span class="m">8</span><span class="nb"> </span><span class="m">10</span><span class="nb"></span>
<span class="m">12</span><span class="nb"> and </span><span class="m">1</span><span class="nb"> </span><span class="m">6</span><span class="nb"> </span><span class="m">11</span><span class="nb"></span>
<span class="m">13</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">12</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">2</span><span class="nb"></span>
<span class="m">14</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">1</span><span class="nb"> </span><span class="m">13</span><span class="nb"> </span><span class="m">2</span><span class="nb"></span>
<span class="m">15</span><span class="nb"> next </span><span class="m">8</span><span class="nb"> </span><span class="m">2</span><span class="nb"> </span><span class="m">14</span><span class="nb"></span>
<span class="m">16</span><span class="nb"> const </span><span class="m">8</span><span class="nb"> </span><span class="m">00000001</span><span class="nb"></span>
<span class="m">17</span><span class="nb"> add </span><span class="m">8</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">16</span><span class="nb"></span>
<span class="m">18</span><span class="nb"> const </span><span class="m">8</span><span class="nb"> </span><span class="m">00000000</span><span class="nb"></span>
<span class="m">19</span><span class="nb"> ugt </span><span class="m">1</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">18</span><span class="nb"></span>
<span class="m">20</span><span class="nb"> not </span><span class="m">1</span><span class="nb"> </span><span class="m">19</span><span class="nb"></span>
<span class="m">21</span><span class="nb"> var </span><span class="m">8</span><span class="nb"> mem</span><span class="o">[</span><span class="m">2</span><span class="o">]</span><span class="nb"></span>
<span class="m">22</span><span class="nb"> and </span><span class="m">1</span><span class="nb"> </span><span class="m">7</span><span class="nb"> </span><span class="m">10</span><span class="nb"></span>
<span class="m">23</span><span class="nb"> and </span><span class="m">1</span><span class="nb"> </span><span class="m">6</span><span class="nb"> </span><span class="m">22</span><span class="nb"></span>
<span class="m">24</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">23</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">21</span><span class="nb"></span>
<span class="m">25</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">1</span><span class="nb"> </span><span class="m">24</span><span class="nb"> </span><span class="m">21</span><span class="nb"></span>
<span class="m">26</span><span class="nb"> next </span><span class="m">8</span><span class="nb"> </span><span class="m">21</span><span class="nb"> </span><span class="m">25</span><span class="nb"></span>
<span class="m">27</span><span class="nb"> sub </span><span class="m">8</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">16</span><span class="nb"></span>

<span class="nb">@</span><span class="nv">\vbox</span><span class="nb"> to </span><span class="m">0</span><span class="nb">pt{</span><span class="nv">\vss\vdots\vskip</span><span class="m">3</span><span class="nb">pt}@</span>
<span class="m">54</span><span class="nb"> cond </span><span class="m">1</span><span class="nb"> </span><span class="m">53</span><span class="nb"> </span><span class="m">50</span><span class="nb"> </span><span class="m">52</span><span class="nb"></span>
<span class="m">55</span><span class="nb"> root </span><span class="m">1</span><span class="nb"> </span><span class="o">-</span><span class="m">54</span><span class="nb"></span>

<span class="nb">@</span><span class="nv">\vbox</span><span class="nb"> to </span><span class="m">0</span><span class="nb">pt{</span><span class="nv">\vss\vdots\vskip</span><span class="m">3</span><span class="nb">pt}@</span>
<span class="m">77</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">76</span><span class="nb"> </span><span class="m">3</span><span class="nb"> </span><span class="m">44</span><span class="nb"></span>
<span class="m">78</span><span class="nb"> cond </span><span class="m">8</span><span class="nb"> </span><span class="m">1</span><span class="nb"> </span><span class="m">77</span><span class="nb"> </span><span class="m">44</span><span class="nb"></span>
<span class="m">79</span><span class="nb"> next </span><span class="m">8</span><span class="nb"> </span><span class="m">44</span><span class="nb"> </span><span class="m">78</span><span class="nb"></span>
<span class="nv">\end</span><span class="nb">{lstlisting}</span>
<span class="nv">\renewcommand</span><span class="nb">{</span><span class="nv">\figurename</span><span class="nb">}{Listing}</span>
<span class="nv">\caption</span><span class="nb">{Example </span><span class="o">-</span><span class="nb"> Converted BTOR without memory}</span>
<span class="nv">\label</span><span class="nb">{example_btor}</span>
<span class="nv">\end</span><span class="nb">{figure}</span>

<span class="nv">\section</span><span class="nb">{Limitations}</span>

<span class="nb">BTOR does not support initialization of memories and registers, i.e. they are</span>
<span class="nb">implicitly initialized to value zero, so the initial block for</span>
<span class="nb">memories need to be removed when converting to BTOR. It should</span>
<span class="nb">also be kept in consideration that BTOR does not support the {</span><span class="nv">\tt</span><span class="nb"> x} or {</span><span class="nv">\tt</span><span class="nb"> z}</span>
<span class="nb">values of Verilog.</span>

<span class="nb">Another thing to bear in mind is that Yosys will convert multi</span><span class="o">-</span><span class="nb">dimensional</span>
<span class="nb">memories to one</span><span class="o">-</span><span class="nb">dimensional memories and address decoders. Therefore</span>
<span class="nb">out</span><span class="o">-</span><span class="nb">of</span><span class="o">-</span><span class="nb">bounds memory accesses can yield unexpected results.</span>

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

<span class="nb">Using the described flow, we can use Yosys to generate word</span><span class="o">-</span><span class="nb">level</span>
<span class="nb">verification benchmarks with or without memories from Verilog designs.</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">\\</span><span class="nb"></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">{boolector}</span>
<span class="nb">Robert Brummayer and Armin Biere, Boolector: An Efficient SMT Solver for Bit</span><span class="o">-</span><span class="nb">Vectors and Arrays</span><span class="nv">\\</span><span class="nb"></span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">fmv.jku.at</span><span class="o">/</span><span class="nb">boolector</span><span class="o">/</span><span class="nb">}</span>

<span class="nv">\bibitem</span><span class="nb">{btor}</span>
<span class="nb">Robert Brummayer and Armin Biere and Florian Lonsing, BTOR:</span>
<span class="nb">Bit</span><span class="o">-</span><span class="nb">Precise Modelling of Word</span><span class="o">-</span><span class="nb">Level Problems for Model Checking</span><span class="nv">\\</span><span class="nb"></span>
<span class="nv">\url</span><span class="nb">{http:</span><span class="o">//</span><span class="nb">fmv.jku.at</span><span class="o">/</span><span class="nb">papers</span><span class="o">/</span><span class="nb">BrummayerBiereLonsing</span><span class="o">-</span><span class="nb">BPR</span><span class="m">08</span><span class="nb">.pdf}</span>

<span class="nv">\bibitem</span><span class="nb">{nuxmv} </span>
<span class="nb">Roberto Cavada and Alessandro Cimatti and Michele Dorigatti and</span>
<span class="nb">Alberto Griggio and Alessandro Mariotti and Andrea Micheli and Sergio</span>
<span class="nb">Mover and Marco Roveri and Stefano Tonetta, The nuXmv Symbolic Model</span>
<span class="nb">Checker</span><span class="nv">\\</span><span class="nb"></span>
<span class="nv">\url</span><span class="nb">{https:</span><span class="o">//</span><span class="nb">es</span><span class="o">-</span><span class="nb">static.fbk.eu</span><span class="o">/</span><span class="nb">tools</span><span class="o">/</span><span class="nb">nuxmv</span><span class="o">/</span><span class="nb">index.php}</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-12-08 01:34:15 +0000</div>
</div> <!-- id=cgit -->
</body>
</html>
