From af3f969cbde48839c30dd189d438b10fc084234a Mon Sep 17 00:00:00 2001 From: Satnam Singh Date: Mon, 17 May 2021 13:07:08 -0700 Subject: [PATCH] Generate HTML for sum8 ILA capture (#785) * Generate HTML for sum8 ILA capture * Update demos/tutorial.v Co-authored-by: jadephilipoom * Remove runshaskell lines * Delete Setup.hs Co-authored-by: jadephilipoom --- demos/tutorial.v | 7 +++-- docs/demo/alectryon.css | 58 ++++++++++++++++++++-------------------- docs/demo/sum8_ila.png | Bin 0 -> 25589 bytes docs/demo/sum8_sim.png | Bin 0 -> 13434 bytes docs/demo/tutorial.html | 49 +++++++++++++++++++++++++++------ 5 files changed, 73 insertions(+), 41 deletions(-) create mode 100644 docs/demo/sum8_ila.png create mode 100644 docs/demo/sum8_sim.png diff --git a/demos/tutorial.v b/demos/tutorial.v index f98c951ba..bd4565fd5 100644 --- a/demos/tutorial.v +++ b/demos/tutorial.v @@ -941,10 +941,9 @@ Definition sum8_tb := (*| The circuit netlist and testbench can be converted in SystemVerilog and -simulated using a SystemVerilog simulator like Verilator: +simulated using a SystemVerilog simulator like Verilator:: -clang++ -L/usr/local/opt/sqlite/lib sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a -o Vsum8_tb -lm -lstdc++ -obj_dir/Vsum8_tb + clang++ -L/usr/local/opt/sqlite/lib sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a -o Vsum8_tb -lm -lstdc++ obj_dir/Vsum8_tb 10: tick = 0, i = 3, o = 3 20: tick = 1, i = 5, o = 8 30: tick = 2, i = 7, o = 15 @@ -970,7 +969,7 @@ run and observe this actually running on an FPGA and capture its output: :width: 70% :alt: Logic analyzer trace capture for the sum8 circuit. -Reassuring the actual circuit behaves as predicted by the Cava model +Reassuringly, the actual circuit behaves as predicted by the Cava model in Coq and the SystemVerilog simulation. |*) diff --git a/docs/demo/alectryon.css b/docs/demo/alectryon.css index ff4ec7572..318c74fd3 100644 --- a/docs/demo/alectryon.css +++ b/docs/demo/alectryon.css @@ -105,7 +105,7 @@ In any case, make an exception for comments: .alectryon-toggle-label, .alectryon-extra-goal-label { display: block; - font-size: 0.8rem; + font-size: 0.8em; } .alectryon-io .alectryon-input { @@ -122,33 +122,33 @@ In any case, make an exception for comments: .alectryon-io label.alectryon-input:after, .alectryon-io .alectryon-extra-goal-label:before { border: 1px solid #babdb6; - border-radius: 1rem; + border-radius: 1em; box-sizing: border-box; content: ''; display: inline-block; font-weight: bold; - height: 0.25rem; - margin-bottom: 0.15rem; + height: 0.25em; + margin-bottom: 0.15em; vertical-align: middle; - width: 0.75rem; + width: 0.75em; } .alectryon-toggle-label:before, .alectryon-io .alectryon-extra-goal-label:before { - margin-right: 0.25rem; + margin-right: 0.25em; } .alectryon-io .alectryon-extra-goal-label::before { - margin-top: -0.35rem; + margin-top: -0.35em; } .alectryon-io label.alectryon-input { - padding-right: 1rem; /* Prevent line wraps before the checkbox bubble */ + padding-right: 1em; /* Prevent line wraps before the checkbox bubble */ } .alectryon-io label.alectryon-input:after { - margin-left: 0.25rem; - margin-right: -1rem; /* Compensate for the anti-wrapping space */ + margin-left: 0.25em; + margin-right: -1em; /* Compensate for the anti-wrapping space */ } .alectryon-failed { @@ -158,7 +158,7 @@ In any case, make an exception for comments: text-decoration: red dotted underline; text-decoration-skip-ink: none; /* Chrome prints background images in low resolution, yielding a blurry underline */ - /* background: bottom / 0.3rem auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */ + /* background: bottom / 0.3em auto repeat-x url(data:image/svg+xml;base64,PHN2ZyB4bWxucz0iaHR0cDovL3d3dy53My5vcmcvMjAwMC9zdmciIHZpZXdCb3g9IjAgMCAyLjY0NiAxLjg1MiIgaGVpZ2h0PSI4IiB3aWR0aD0iMTAiPjxwYXRoIGQ9Ik0wIC4yNjVjLjc5NCAwIC41MyAxLjMyMiAxLjMyMyAxLjMyMi43OTQgMCAuNTMtMS4zMjIgMS4zMjMtMS4zMjIiIGZpbGw9Im5vbmUiIHN0cm9rZT0icmVkIiBzdHJva2Utd2lkdGg9Ii41MjkiLz48L3N2Zz4=); */ } /* Wrapping :hover rules in a media query ensures that tapping a Coq sentence @@ -208,7 +208,7 @@ In any case, make an exception for comments: left: 0; right: 0; position: absolute; - padding: 0.25rem 0; + padding: 0.25em 0; overflow: visible; /* Let box-shadows overflow */ z-index: 1; /* Default to an index lower than that used by :hover */ } @@ -256,7 +256,7 @@ In any case, make an exception for comments: background: #eeeeec; border: thin solid #d3d7cf; /* Convenient when pre's background is already #EEE */ display: block; - padding: 0.25rem; + padding: 0.25em; } .alectryon-message::before { @@ -279,7 +279,7 @@ In any case, make an exception for comments: position: static; width: unset; background: unset; /* Override the backgrounds set in floating in windowed mode */ - padding: 0.25rem 0; /* Re-assert so that later :hover rules don't override this padding */ + padding: 0.25em 0; /* Re-assert so that later :hover rules don't override this padding */ } .alectryon-toggle:checked + label + .alectryon-container label.alectryon-input + .alectryon-output .goal-hyps, @@ -314,12 +314,12 @@ In any case, make an exception for comments: .alectryon-io .alectryon-goal, .alectryon-io .goal-hyp, .alectryon-io .goal-conclusion { - border-radius: 0.15rem; + border-radius: 0.15em; } .alectryon-io .alectryon-goal, .alectryon-io .alectryon-message { - margin: 0.25rem; + margin: 0.25em; } .alectryon-io .alectryon-goal, @@ -328,7 +328,7 @@ In any case, make an exception for comments: background: #d3d7cf; display: block; flex-direction: column; - padding: 0.5rem; + padding: 0.5em; position: relative; } @@ -339,21 +339,21 @@ In any case, make an exception for comments: flex-flow: column nowrap; /* re-stated in windowed mode */ justify-content: space-around; /* LATER use a ‘gap’ property instead of margins once supported */ - margin: -0.15rem -0.25rem; /* -0.15rem to cancel the item spacing */ - padding-bottom: 0.5rem; + margin: -0.15em -0.25em; /* -0.15em to cancel the item spacing */ + padding-bottom: 0.5em; } .alectryon-io .goal-hyp, .alectryon-io .goal-conclusion { background: #eeeeec; display: inline-block; - padding: 0.15rem 0.35rem; + padding: 0.15em 0.35em; } .alectryon-io .goal-hyp { align-items: baseline; display: inline-flex; - margin: 0.15rem 0.25rem; + margin: 0.15em 0.25em; } .alectryon-io .hyp-names { @@ -365,7 +365,7 @@ In any case, make an exception for comments: .alectryon-io .hyp-punct { font-weight: 600; - margin: 0 0.5rem; + margin: 0 0.5em; } .alectryon-io .hyp-body-block, @@ -387,7 +387,7 @@ In any case, make an exception for comments: display: block; flex-grow: 1; height: 0; - margin: 0 0 0.5rem 0; + margin: 0 0 0.5em 0; } .alectryon-io .goal-separator .goal-name { @@ -403,9 +403,9 @@ In any case, make an exception for comments: background: #eeeeec; border: 1px solid #babcbd; font-size: 0.75em; - padding: 0.25rem; + padding: 0.25em; text-align: center; - margin: 1rem 0; + margin: 1em 0; } .alectryon-banner a { @@ -443,7 +443,7 @@ In any case, make an exception for comments: top: 0; left: 100%; right: -100%; - padding: 0 0.5rem; + padding: 0 0.5em; position: absolute; } @@ -503,7 +503,7 @@ In any case, make an exception for comments: /* See note about specificity below */ .alectryon-windowed .alectryon-sentence:hover .alectryon-output, .alectryon-windowed .alectryon-sentence.alectryon-target .alectryon-toggle ~ .alectryon-output { - padding: 0.5rem; + padding: 0.5em; overflow-y: auto; /* Windowed contents may need to scroll */ } @@ -562,7 +562,7 @@ In any case, make an exception for comments: } .alectryon-coqdoc .doc .paragraph { - height: 0.75rem; + height: 0.75em; } /* Centered, Floating */ @@ -591,7 +591,7 @@ In any case, make an exception for comments: margin: 0; overflow-y: auto; position: absolute; - padding: 0 1rem; + padding: 0 1em; } .alectryon-standalone .alectryon-windowed > * { diff --git a/docs/demo/sum8_ila.png b/docs/demo/sum8_ila.png new file mode 100644 index 0000000000000000000000000000000000000000..96c2bdef1e636dc5c25bb1a35e11b8807d605fac GIT binary patch literal 25589 zcmbSzbySpH*Ec2#A`*gtfOL1aN=vCU3~(deF@&^=w17x6gn)pwG(!qV4&B`_Fmw*h zcTn%=d)~F)Kfd*y<&ujlPVIg6{_TB!hoG0rvN%|zSQr=>IP!8*uQ4!g@nB$F`*`O% zxMRXfBLjZifIgR3yL0Ex#GJ}3_?5&-TFXh*&eX}((9s0L%+}7vgbixsXkuauHMeux zx=}BVf$;=GUh0|J+r;%L4~Uxcg~T@6Q0l?0Yit9*;(s;|5!x9uXLf#-jIf}CXH2-3 z5%G5&4)=~6R$IoN+Yk+GRw$J`(G*avC&@M`;%dL=#@0+0ZF6(s9^-c=>O0iek?7X< zO@?tK-S^Cv?{%&n$4M+F3L!nkJ-f~P-FlEMKUft&H?PW*NDMd_&hIiia`K?>JXg6b z3Fq$}2|s@5-%BAXZp=TIp9!e{bMv5RY{sF@+_(ge>xUVZMn;1 zFf#WelW*UOyqPi25Ji0*uZ4C=r26V@YHD0lva8Qxviruj#8a3+phgVvgD2C6BleBgce(mZj`J?c8Cq}_5AS_~ zJ?bh}vn(pkt8rT+2cHId2!t3$l_bBN4`MJqDAib-R!V9w&NF74Kq2>YkY>aNBhZ=X?lEU-2V1irTq-Hj%WGDW5TX`O`pdq$0jw}Y&s5YxD()6jn|2f z1?ElN=1t2EOt_3wEbzBWQzpXp60Br;Tf`+rjqT590G5^yeq_ zZDRbe1MrZr=+8B{Y@>7TOiy-sQef9eJ;Jl|=atY7BWepTT(~|7&7`@# zS!FFh8Eh2^C!Z;c4^?)5ll^5vRO98hL`vdr&U@)<&7a4t#b5F23yCKN77!(I^4yco zUFXLTZjajyYg^DPh|=jWWzwx@i`9M+6xSval^nRQoG6I*-~p%i*<0_P_DF^x^Tv;N z-zcNU@NKIr9hduQi$jG(z9~RPtQJfiA9&4~?ufdVRJ9%7?Pt|av&PLKKMXaC+pavu z9RR&D5c1ApwT=1meLZUGMn#x3X@n`m=uFMjFZ9YB!aM z6~0xVGU~6bO7rBy$`&)2 zV9j-7yv%B(AUZa-wWWogmNpRn{OQxDa&mIW^Miu}Ha4~beJVl0%8U$YMcDBWD(C*h zz4XL`k6*?cOW2F7e=Y9N1P0#rmwli)_`U#{LWJhgQTDmOhM!Md_ZSUZATh36V2Ae7zzp3!>gv>AUh=fNkZ>h4W zYws#(2g}blIhI$gNHHN~#?{{C4A&P`eV-kD=pWQq8Zh6XT_T)C9b`MB8ph9(n?I$S zltxoK-An52I?BC-3JTnZXDXIe@hOgERFccF4D51GR8&Uk6mGCwzkdBbg{Yhq#NPX8 zdrmUoe$ZLg@5!`ENJs#x@=OX34^LiRJ~cIUq|o4Ue?X;BuUZ2F5p`J~eSf3+zU1@g z&nes%Bf3u|&bFJtj0d&*cRfsi!J4I(Z#2;a!5x>53c4WgW=}j<@#bzMS(ldxEDaU- zXo$S%Hf*sTC#xPC9i?NZn0<32#svQT>F9@%hbe4^n*AGuS}q@9&5=mcF{efbYJ6UY ziRO>tDJg2TW9Iy}{Hm>-)f>dY$`7AzGb{8lN08sG%9=n&EmY3Iu;W5r2R*YAYJO?XV%%`vnj65c93XTpzO9JYDA;P zC8g%vqSK|J+oOi}>Jvly$DM^%l?2|^qn!m?sartu_>EnT(WL?*xQKKH=t4l~-3e%aEp?(uh?RR7E;4YzUvk@t%fiL2_w!k7#5LomWB78loUH)Mc+Y z-w@v2R?dZ@?W$1AR8C6x{Mmkc_Swg!tC0-gkn*l1du+my$sR|qmM)Kbe7ciFWTkFk z-mlpxpQuU6h>3|I6R-_TxE5yE*eY>!6Rlq1d}OYEpiV6!L4T*dO`&7cvOSEONLh-e zMJ1R~Oalx`#w;f=G?90@sms+`;0=!fqhSRkyY9t{f}li%mhsWkN!DcCsXXP-(GN93 zI>Cwg;_CK!!5MMiGMEvWXZ=REvZBszI$!BRjM;Ard9IKK(^0cspV%`RaMnz&z`xt z3E|<8@msfiA}Kbe;pE(|JKbEX>Pj>L7HCgl!n8`RfMD(Cw%nUXB^jSYik7%#4K+uAUaM=vK%9oT{p8Iy|BrNkxNOooxSdm z!LM#5r!wNo!ih|nmrt>p=T{=B8!t+t)a@=y^f?&PbVS|(!+(06K{;`@akqN2ibY5W z?sIwJxb#gWMO?2Up68R}^6T*mi^!r4D*-YgxQ+KRu+s8Fu-&efuH|9AlrL$n%du53 zs@TjL#{@3wwD%n%)M4s+hL2)GD=g6|r z2lW9heqni&vC{T7@+D(!)=5?YIl&u{Q^;CN*Cex9pS*nE@%=q|2u*(3WnX=!7EJxh5v!#C>q+umh2eu9MDcNt(k#a`S&TsJ3$@yFHyOLS}|qS zmO8+_Ba=Ym7`5%0O0e7a9?crtx^S(JTH!szz3b5qE(cYT~>dcoSfiFob_&cR}{W$dwf+T2F97Pjm-vdU^+TF5V0cQ zr53A}=C2+Hj+-L+T}f|u7WeV*Is2~Lmw0}$U$6M=LGv@Cmh|e=QNs#Z_t>iSyv^x{ z58`j&;WaUuiS69HJ$rbkQd?XepsjducfPAPx1IG06K-E!fs*XY59Kh_jtQK6)PynJ zTFknsX7|CB^6Jr%pw#m8&tmJRPciUrVPYbZi0%Ec=YZ$1&vM7S@W-F_x_WE2=|Q}Q zq=JHioZKC}=9ZR@tJkbFaPHo1NJ5bxk-d0}z5wPWz?FBll^8UFsa;U&GW zIf<+F@y^4VX0Is#H$*7ZFmCpDnXs*96BV7jL2~1FB^cY-e5d?F|*q8NCz!u)(b zSeK!pAr}`HMcZ%e3zpdya#;}SZwP#w|2-0Jla8od%|Z=LO$8X+pGq(!`ld)`K`5Z8 z*m=B%q-*~hNxZ9%_{a9JxA&!D&don>&Qjc^-t#^``46PG55E~9)Wpe(aJjsKi&w>4 z?!&($!yL}@;YP49qn1E z_Gg&Jv{2)2&R02oQfk|)btRJ&F>Do{DpFE2x*Zc~l_jU*Y){fm=@IYMDk}?GqgT-hpY04!0%s6^K4|bEw16+O+Ogc zLww2fpp#8kZ>s$grt&84<4|<;>vPTqJ)6_{@0$i!0Wb!}*NQI^+;%u!$3(l5$7DJN z=ApwAI(-C2GNmcBD=yR12T2e2-7Ca)i}EKAw4aSw&PA|#Y%dvRlLZFyf4fgczwSD< z6LlDdZtR}68CxB_TO$@3Zo@`w3YXmS5=fe&Z&SCjwUNOrwH-g(uz|S=^hV54qq3B$K!0(=G zMyjs^UMV-DZu%SIYp5?iKsz=w*ENqWM*-<6C2{BRX1#HK?h)yDfoNjPPIGjgV9KZ3 z@E<%&?C2P>J|31u2u(#)l%iyOPC3I5}Td))y6VNl5qr=(^An3iZBq zJkd!)Zwba<;0II^&L~Qs&8Nd*rp;cp_}uCus(IqpR6bk-jdP5t?Q)d%@C-`*X3Y1P zEYN%`Sh`8O+;gG|M=IzfBfoYY?kkWtvHTqezQ;5Wiz2X58G9;Ee*J*o#tcU@bhCzO zrEZ3+SvkM|a4+V&Pd?j^EkTN}O&V61A90QY0;|Lrf65nCyFUA^Oz*bpPHkuEyrQF{ z1#Bl*fYs5{n}S1;hZ_^mq$dePO<&`n)^ zXspC6DG{*)vJ~tZY*%s}a!;F}DN{;DMVtrf=gmTM;y_xf_Ji@%m zA7`zcO-bvqvkMs3ps@2}gkyxod)p4qr0v8H!}KN|m8v&`pl)oS3d;#3<6s#{A^XO* zbE_sSx%3mi_0ja}ZeM5*P;odS^$6X^#@gd%@NMh2pU;NajuMp04E z<<9s&Q9=&_k(-;#!o)-(=I*4W6-Qj$2cR@2rRR^mi>YeYk)a`Hx0Cg;67=R2;uaEu z5TcBcm67RA7OO_Ew9S|*4~h?-v5v%gmFARbx||jqzWox88@mKn`c)b4Je?XhKU=Na z9VU7U`^QOJS$ZwV#?zeiu>9_5RiuEo)6dj1oG3wb5W_NkzyFzJzVG#q=?8kfCPjbD zU1d&rxkkooX<6CU=4L;CfBaYV-sg=?O>oUCyl=Jn3+vv!L@^H+V`Ez4M1yJP#cm;`0tJph-o&VKIs%a^@g=qY5EQ-$r+c)gDg1J6%qxFzXb(>LLtJ|zl4 zm+QPvrCiKs9vsy#(m+f8=-0ax=-}iUL|r|4?*=su%~VGiwzcUSWJ}^i=kVqk*1t~u zsrT{m@gEpCV$M6?bAqnF+&IJFVw(o`VW!rjV(R?OZm%1?3v9Lqp^p*Rd5(7_X6M<8 zP!l0#*(r}X%io=yO|i7HT0^0(kfN|c#%pJZ)tDF}uC*8uZqFlo>S7Brq%U++9m(1K z7g|20m=uH>#KZom9>!0J|3H)f&UpU++*GBsqj#CGsc_@@3nwsAT;lK8{EJR@{|lY` zuaM<`z3CIw2{2`Z@M~F=9C&H?D0mp|+fng+)nTYIuErUyue-+)}ykOs``07aM&YAs~o{h2S{Q zMBAu1Gg(r<&RW@r-|70JUKmx`;R>=a$Aj_FhZG$z%$B0nMI5o~kLRqj53;_eMx@K$ z_pPfrJVXF>^=2x9N@D z>2b-ItljQI4g_;fpt<3Tv!lLONx0^=w#STHl>y=pSj{-H{c+1rU)wea zy!NbA-cma=B*1j7#r@72%oq>`)6R{iNKKCJNd9OP3Pr$Rts2j7qhtT0Rbnxz+GS%L zf_spMdyr z=F#L-fE6E|skAfF&cD`#4x?qcx<2-{UyxQH!gN?2!~5zMt-=FrF_5K&7HM-HefKHE{Tn z%1M%@B}$AizCPyQ_=5+7$3_4{1Q5#x7m?VW0qGWP1x z`X06oyFl`@|4$1o&$~ShP6l>X+JW5?`J!`IYX&$4lAE1aag;k$vd_LZJ)dePRB&6%Dg=%)C zR+mH%8>8@HsPqx^TTRRT@VCbi?a9h?AXNdJRilzh7UOGx3u$O*#GH0|dwb<0>B&Xk z_DYUmVr;VjE2AQQS%^wFscxNdIDVmLqjv)jNJZ@UtUk?OW?kaM=;c2tt|J#6L$eUb zXu2Z8Xu!H$??nsUL*m?-GtIi^c-t*GvRO)>=3H|8ag}|Xmg6EMFONpZflU#%7&qT? zwL+T#6A~+m?vdWx1TUD%*&C=Zj7(1MZibzE;CfwVnJ^`vTC(pi(x4MX_4H?YE784Z zh`qQbK`fA7WEKKmh^Q48tWeRMZIXgGF*ec8GNim3-526Lym_K9rn(_K@zBaGP z896cg267=_ zSZMM^DG86GIhZBoWOkqBW*fT#?O*lqqh6=RxbH13nFDn5Rce(8TU^xVz`Ju5JqPAh zVcbpU8~So>KrEZk<=tp2NC2L9{bI!N4GTLgf%;VF9EFFgh+|n%%WJE<8vA4qFL>rI z>bwXgn$sPw)e?Cc$0lVjW;A9aQjx( zWZepZMC8P1gs#?1?@`F<7Rb;~e>zHGGsv^GwRQ7B8*1+kS0`0L_KTJVT$Sx0Ui&7J z$NDf$7)-Z(UHB}-Y+C5$QM&7{k&p+|xzDu69A%2Vgp}LhN3K_%kWw(!KK)zwu-5mM z6Ql`Rq#|Y&O0r7kMAVuvH-PX@E^E*=-eyo9t35bPDmmOQG*n4}m{yU*2NRD^ph69j zw=8VOphS5N?9JQ#^NSr~2GDK{yWGlSk6eFT{R;(WC=?MknNIP-3pfRDU z;P_>MN?c-3cx_$ZQ>o?gFKH|cez>?9T299>2@0KfH`EqI71$1bCkyPj*r3AJ+a<~_SHi0d ztjN{xX4}8&<>9a;C{KiXoc&mWh%9vXUNk_y+poTul1-u9d-)vLpqN130UulRkb$`1 z!4&za7}^`D3cTicC`_p_mM|EjYd>XerfUy^I@|s%Fv5DWr3uYcA#JaBLLaSwU8eIC zBLACca_3f?lY?Pj-9eOUWUUYNmnB3ZaKpS}cJD zYI@^eXU!t=B42d3yS@ZunMD_r1hqhsgl$nYg>SSE`!f_OCLKd2Nv?rJXDTrL?i1GL zR1IFlUDdiGMx7UpU)ZW~HAe;sUO9Ii0Q06PLK+ebz)()28a50Ws@yE4_WFrV%8b7tUW7Gb1JE+(t`^@eNmPoO@dVb#z_VWvPf6IYiXQ$X z45vRislE-9h|isNyoD_Oxb%3ex(qk?(e|)H2&IopI&0T5_{6}+JJnTuc-ZTdA5VQy z9lvkMpV=1Lk-sA)S@XF{j}_s)*Cl}E*9eO^ZVn-~t3A*tq#MyTGBN^YL_`7;;~l%r z4Agi)7W3F=40{vSDJ{d*p?k`B{i1Fao4Po$HtH<5K8rRCYEcshuw&HP*y^-34hf+< z&~)Gg)BMNdu`=NBjPe4*wy&I&@kN;e@NuoZpd}vvxPYxVpOr?t3MwR_YeRB9Zvv&!~}Pg(TR8sgY6S(s~B+K&0ei#>b8Q zM&0s$^yPZdGOFb=tc~WG0`R|x&=DXEgFZ3O1=E3Mg)$ZK`gj8}DK2;5Wg(gA~s{Q36IYZ8w^4<12-$0Z*W;y4)e% z{|Y6&)Ou6Vz9QEbKVIeEzOZ=rzDI>!uChQ$m+O@9@oG_hJfF4yHk}{!>EPE)27?y)SbG* z=h~VZP0NpmB7H3W)nfyM1U3b!8KU=ze-re)CN9ncLiCMA^;Xl9w)tt|e z;GVbI3ViOOB&SY$<=Qr!fb<&TI~XpBHL*Y_B#56poN59%p`%P{vhr1h3d~pp9>l;J zrr#)boQa~Pj3~NEt6%FL9auw| zNK8x|8ym|K-BDuJ&8wj3!RcVXEf^m=a?faMb5z3SO{r3S2SCjAb>cMC7{(F18IBbu#6w8|rbGSn*k;G83a5>jWr*qDN|-x8~ty8Yt;$0r^J zYTMv-V7I6f#Ju(a^q#34`-T2NPRRB2@O|ZUUnhUP<8!;bqt}&t=adx&-|M%}q>@T4 zGNwh~v$>S(bu%0W@WXKQr^R;kDZs(VjZ0gwu+4s5cADZ>Qg$c$ATR4^)BMmgOR0ly zK&?RVdw~oB$ehsI%54L#X6JGrKotExF;M_fVrcXgN^X$&LgyZT=6;PsSu+`8{a zKZ2k%XK4|amO5p@1rk{KIxA-z87Q9nnTng0oqf5{5grvCee3pZ8Ch8mp1$#M9qKB; z4hkg`us%HPzV3*DQMZ18B-XEllz1L!0IVogx=@ntMR+Y?RYJmZvL?f(fBw-@{?=NG zlk>3|*UWL01*6fk4=AjH^po7MsZin)o}~05}MW6^gPU~#?t->qv`z? z#i``s63fW4{Y0k#CaQ7#wEqYMI}9l^i3dKXl~hY00EI~imjbH?APKhW zyaK{|_a%x!B{o)5!(ky8mz-nDr!>xIwRh*sheGe8NC0A>3fTu~UGMDWI~7PTVXdYP z;q6Az5H0r86GMpo=2F9plC1FQ?RgFpT!hf{*~IzcjjjkPNqG=l8Og<02F%!;BAO^%K5U#@#Map z6tD5i@41FTL66OnQ~L-ag5|d=XH=mj1bsZ=RsidWAFZ#XT$Z0^)TP|NPx*4Dx9vO| z%IDyGAaDU3BQR5Ye)M6}#@4^$yuD7mbPuLHnstdU*I(UApViq;7+XdMSLj!3j})rZ z7vUMz#8BGZw{oS3fz~RX8_!n&W3%l?Q%_#)iOP4KBH~^&Xx6<{uW=synNsUClB4@U zY**}}hh^D6z|V7gtdGymbGN@r1=#A`f^6jGEwuOLnr_Mx5uw}4c^z0|bB0s^-Jc|F z7}S;2Hf`a7+4srGnTpVjtGLuv`F63m2RlCKWcU=+e`!H=*`IrvbkZ3zQE739L)}2c ztqQU$F2b*uX~ys=LW~vp7QU3|QI8OGXfMmOQXXcAtT8&Csn=aw$=I#pwis}vwe78} zSMuT0qS{NFpPQSDq*oFKv?3_9gq37vrryWX)AQ*&&9&s`sc}FuUS6k1@2}mstr*Ao z?2r;{__=>ZXclZppsYz&C0i9h7zRnol~Xh>=r$fxj4c?q!IJ(7T}9I?QP$e@jLckW zX#-Vn`}*Tob~;4@PtpARkmk&>0A7-)-bG7hEqiDVCi3K96@B*W6EXJXOuhGLf@Yno z^>t@8S3qWo&#uhR$NAQipzNJ+*Pjz z(v)@4;XfIBx&3wVDj7iQp_dIG8`t%P_UL{VZO^h4q)hY>rUJ{AntLQBkM*oJU6anB zVm&0dC!_W&+3iCdGKsc@sjt88;NpgdgopsT(a-lc?CNX1L=`~(lTL+&KGW-ombCOO zMDfnfPO)Ne!Ar)EdlT~FBjgxQ3pE{fn9;_-!Exy4)Y`-SCmw@X3t0a`l_ZBPt7wjH zj8?F~+sk5sYuUlm@sc!}zOaLT&hEV-CVCEOv{5yvvKq>~tkHaJByKPxj$vo4wcih{ z)F4%|UP};bGG-gijH?S2Eg}8 z)7M8{SsWVd9^Mnl>t><}m>1{zx+4$9>&v+E>rx#W;}|#3y+Ig;d`&5UI@G)r88Xe{ zJSbEVg2?_j1q+p#L#>rjq_ajtU%NSUY3Dj+-WvzL_Ya^^jmbYz9-Xv7qSVH49x)PAgUN-|JMV8h%w2)vC@pP5tx z6otH&B%%+Zktk-{EeUJ$wq7ng3H0;+8z-2TXuD0_IQ%WYQfvDIX2u`k+g2wa)ipqA z6OJ#Im09qfT3Sg$Uv=b(8!EDuImOevWY6gJRuZdQRoETu#A=ShdMiOk)F<@JmM1D8 zJT}wg$!}==!>j6BarvfySFZYyGbBVfmY`h~?Ik}T+xlsH5PzVApoLW~*;s(J-b?PN zmZufJFVHYqkCVe|FxX0ITK^|xSLR56c39UA2N%7bL&*dBRJ}N zX=U1#Fto(wI_+i_+X^zRW}R)rg`1O)*SD-Mci(^8f%FO+zl`%3A$%CGdqpjE04zT2 z7A2B8f!_33i}cQVY+6ToEOeEUmWN3w}Qm12_47 z*8J2S@9Zp%Nq#sj(BZ1k%=9)!UJAN7kNOm0Jz( zR`gN(K>wJl_9)N)aYyl;iMFBm7}gH1uPlGF*-r(6f;zjJ{VOB*^A|cI9Q@yu$QJ** z%`f{)YPqjyJPjXq=wKxu!OuT_vGX?p{Uj!?4U(;t;iT@L?G?@>8LgbH<0kX(=KDVN zJw!3OP`JU)=Wti*6jL|}Hf78Wwt~7g-3kY5e@gf`^p4w_5dEp_E3r1zjSl|9GC?@f zghwpyZxSD)o;Fk9&z2kp#@paX5VSOK-itJ}^y-hdU;H;4U)dyYcX)WQX6a=7mx;W6 zZ{PG^QgY-~sAHJ5P&JkGx8t* zNj3}Y3{__3<$Vg2`SfUR1%s=0EZwL~nvP#@q$v4HI{UmX3pO|BKqIeAOWaz+$VFV% zIbmI4VR!`bEM?hI1s$AaTU;jJ`{9DIUNlm6q!!LvjEB$4+8>mV$rDjBN* zb`3CTY)ev84Nng@Ty(nue-ouR4DSrOM`LkuH9eEGpK|rEy8C{DJrjIp7M2M(lz}(~ za2zc_E>mi-xAzAWscbt6|GaYWo44Z5Q4KBsJ8)|NhRe#zq?A)o=h)Bk1KyxVOR zjh!Om{_qvJQwc~*XPWgVLz)I&%@r}&UGY2&AZHgGKdrdS6A4#7wGKP3@(}nk~%NX9s)YaIc#U zMSjwYtq;xE(6bL+T*t?2J?c0IQr_nFwsnDF=vJoqln99gL%8Fye1SC3;U`grJaM73s*HR9ic_f z7|v+qlhR6{iXONg{)Uf0-t(ok8IA{#e{$iEfu>_`FfxN>TJEcUu5RGcSC|$Kt!bP{ z8Rao)&Tvtf@VcXfdF|2_b+e(5>U2sXZRj%vT!I6nUzruNB8q__OD4Zoz*EfM8~?{I z{2UR|<5Nnq_@tmYcJm9E4w+~Qv;EMxaG33sfBMjX;#iX88{n;)Lcrc9xsQ*%%a1^- z^4lv{o1^RnmBZPWADAjs*J>k=H$cxo`RVFhlnfUxvAMQ)DBdrWO=MsZQU*Hdy1t|& z1=(__4n1#PEp~&wU7KO-RanAy8WXi_$tWktzNBN4Z!drGW6g zn-7Eps<~}4lndv=c}+%FH3}7VNn(@P&q{#J)^hrH6wY|@1b17ED>@>xi9K4y*TDAf zs@?LV^_$C5D8i(MZj=QuRbMh5>dUIve7W@a9X+czI(J1`xXE}Er@sj2*{vNDdE9A= zD_E+<2|JlclO6@^WXTR0g1jCl4@Q}H@D zEVMn5QY+dQnj5E>X)%yF=CvAKMSO(Z3Bad#J9|x_02f1SFj>q)xPFZUI5QrMUf5{- zc<98Cg{_O?FtAwqfIewrvIMZX?}ras4Oj+YocEx>C<0z#-4q%Jf9PK}9|pw$_VDk6 zLK1Y=xWxSNMn$|p1+{i4Ex($|x3FYk-%1lOwBcJlH>6A6qz) z|NDLIANWHT&1^)Aa5WdW@?wZICwCn)T+!`!A!dJH+jo3J4Sk)tR5T7&ZC~kTuc`K^ zqUM5Q8lb^|gi5T+jY}esxuT@xnDh-EEODyy#lZN&5+!ow6{e_|xf$lu_DXH(HFR}F z0AJHq|K?d2IA3FZ_?7yAHEHX~?^f;r00&HsEf$Qaoz#MrrCI&wRx0&1j3aoro&y&7 zI#}%6UTG7ZbiRRDwC{ueV7uCn)zFe^Y^9_pchzWrSF^$=)zy_;&KC`Ny4N=kOl4IWa^=j|Ms(x$}!PxQV#Y2l9a|n z2m|B;!nJN+o3VOfZfb6BYR3i-6E^Ft^V~yhm-)U43Ve0i@{IM`TX+!>c)93_VIr5y zobED2gY?TK+A1IiPi ziGP(=;LD7h|6L(QBEc9;FR9%$CulIfrPAqP6KBr8piwfyw=-z+zIkP&=K6HmhqnEI zP)y-XyL#4YpM%+kh>dW*(+LC1v3gVc#o2~j+)~Pte-yM4@A)Dcl?`fRpZ7)CnReTS}$Fmii=SVHH$2%c#nC$4b zA~p5v%Z;GbU&T(CNOJU7EN2JI->d3t=*ks}yJH+Tsi^WHM!>WMrFT`$ zO0zG2eiWPaSd5>q9lY$oVeK>Ki0g}3^G@=nBmcB}SfAMkT0**;$! zf)??3j1C>CbuL?m9b*6smTWD^{5bJr`E96%l(gf1%>soQm6_{<-vWC3W|)V;%B7fD zth=q)Mr`y?`08NvO=wNy2C0t*_Q;Uucw`|%fzM$+rh(#k^Ol_<;6V$oj$PNe=xgTV zc?9UCH#nvadv(vW`HAt$j`wAeBc1;|lE1+E{L@wh_F^?WB^U`Eb*#*PgTt+OICE65GJmrJ+z!-!WcRY@Y{)P9Ix z&L)uDwOt|+%@KLOu|I~eIM=Ur-~0S-y9lw(EQC5zHexGVRZ(X4jQ#=M4_jmOVew zZZ&j|tVU0=vv`)fUKk~LvL8>FRZo}1)b=yuz zzN+sWWOxloM5h;cePAVeZ&Ah2mHUZp&+GZHuGq(PNhjLi^LV~mp1}{A*4b{nR_>=z zn&FAyu+?p{o1aSx`1UZ!B#4fl%7O&%p=kAN_${eYYnSH%CY?!|w1#3uLI4YVI;45! zmpJpRp6)F6$r;jeudvbV((G+ydhzw@D(fC8lHK)~htp0jLQF)1bYyQ%2)`ycyu42> z#LNiBviv>IUBiT6z?9;*k^G|bC{b4-xU`66Qto9iKeT&Wx^PV*DUZc`ss~UfE6CHO zBb~ARt)Eb*nFv+KWQdo(mq29jL#a)VI4U$Jclv(>5Z&|2-6&h4RL_%ta=Xa?tjZNT zlYuP@C%?j3yWeSU=n*Q1y3FJqAb{FUs0**B;^fQHqr%s9_%qJs)Tr#svb1qg_H;s* z>(NMxsOYzhEISZp7DJCHvy!FA?J;(WY2W$OykBeiCUo@NnwF~a86A(t>Ru;Yr7^UL zVyla*C2CwwP{G)_Hiev?JLT9RA`o~J1$EkevoXl8<4l{XsSARqFQ#g-2S(I1@*F(* z0v@)@mw}nwNcjHz0^t@bTJ6SPi?S3y?4EHt56CrH>UkU;O>+V9FNjgc zJwee6X(BpO;Ao0<&jN|3wfH@+w1rL}jb_!`@V#P`cFG3uomZ!muXv8jWt$+_Qgn=I z4ozLYIAJ5F^$)%&KJC_T+VKWv`08vM-hH}}+^TYM{l|c0M zY;<80lrOxsY~SJrBQ3R$ZJtHwrYLypLfE6#dzk3}`42w&AodNxhrcmrfy}Zw>gIpY zS0NQWcX-$kQM8sk+o#5SI%&YyEXewwSnCRdWh?zpFgoA;VL34CDUk1PtKX|Dcm)$b z$;{MQ^m3luFU%_B$+(M|67s?1`;`*>dC3aAG!)MYTdhs}eFGemqIs2@DgS*Cvc5!^ zs`>mcB-8gb)IPjWXE@sE(N8wt;=FPvQ~#8xnpu;%*>cAN(zmI=drg%7Y)U=v(a`1+ z(OHzzjI+PtV#nRe);{t{aPVWLFMX*E4`ctuBudav?=d(B`K0XV=xvM%3kwU_=Y2#- zNNc*z*2D=87gV|*peDR#oYXMn0Sqh&s2YAVoqKX;s)9kF|FCxTZ zH#%O3Mn%i{`ALb{9O#gw>IVfB|zAb!&KQ?aUulT((3j*cDy|_+o>!L};CtYN6pixjsnh zL_x%a(s+vFqZ&$+0Xs4;Vw|H*Psz+!Rq8^h7e|-|_65O7+Q4tM{?-Gan;M!rqmtBc zUMgzMc`D8MW77f*cR~kf35+{#(V7Jh5BymM5`V)Zn{2;;01ksX&$&iFaBh&;L)pIV zkqtAta<5MI%Vup#Ao%aH`;=l1t!gjV3f(6ynoHpK@EczgU*lxz6E-4u3jb__V^J#>gZ{mfQM#jcxS5Xh|8T$KcppPyrhAr z`GY#^qiyVjy*tnU{vnMAl8SaN&>|{!>9Iq#*e?M16DHAv za+cb6Z@I-kMVUPK@dMF~&2}?Hod|lNePVtnxUONUEpX~*&A?NqZ8l+}iT#hmu95M) zXV0(C)?;B~`^~%p|Jxj5>=V{$*xBqF3A{wtb=$e^W~A*!yq>>{z)T4hBlTg~u`7@z z7ytoF+5j>k5W7>g?1iNlDcMGmHRuGnxTm0ifGarcicQ3N2MY@yI=o~T-W|v5vOHM* zM)pE6H=d8d@WoJtY;`p5REGg??z!JVQ`>cXuLRw_0{(HGb-S*3FYH0FLwyU6wrFb~!k$<3* zObnTAod&QE%wjNsoSd90K-!j)`uIF`Wp{QN7HascbG9vTAgf-&ao-#Qnfw++aC<)k zJP7_-w`uY;HjRHtcneEU%~Fr+#Y7RZ%0;cTthB9`_StK9B^fMO8jYARNQ^%XUq01S z_u@CIdpi1!$yHzYbLE}{VDwi`uXmJ+@^_g|@Elt_eDL4_8QJMddboy~n)O(5MqS-> zdjs-?Pfg_o$9peAo=g>*G{AfTQ>Uq+*8l77vukSGJtKDfd^0r;O$U&`JDu&@bHq^x zfid?sQr$Eq2d-iK%=MJ`cFjJluu6PXeQ4ylQgWfQ2|6k9&Rv+6SH9)@TzgCpVTasI zw<&PI-{&CLAPJlpLd39vQ^DQ1(1_JBE) z{TDmx>P7DLTRCM{tUJ!F^#1fE2xZ5!3nZv#`c%nn(eX6m153w{0P zwQ_g0OMh<4cB$b*6q2`h4g#s3Q{$3FS866Wn8t+_vG4e@O=evp-Vdz@7PU2*?IVDY z11^i+7~&<3nYBmsWP*sA_l2b&8*;TZK^ej=?JM zUXyun>GSSKlmZH0%bgK6iGKsc6sIr$T4nHbTE)H7 z3}Cn?Df|^98Kvocr=j&0%Bcb$ZTmdN_W4W}^1!UywRq^vgQWLNkQ;Yd2V9YBfcXBB zeDokX8qn@PO|PEW^5E$=>e9RB9cX%F(D-TR8g(Dc0$>;i{2B;jo({Zv%`KaFWPs5* za74;wU;j7V0LFW0?~shi-60VE>E95 zyPN*^<0J6qkPTvQ)&-;B`8mQ7Z8l=A;?JKR+!=O^I^7gnRw*cF`d}qFd70x;=^KX<| zB)lH;c2@q(WslhS^?&JCEiP1B@6FNC(Z@$Q3_&4L>!ZU_QBf7S{HHn3s(bl*czCRT z>I}6cy?QfM!>Zn0_iq@o;oq^z>bf6@j0iF-hHf414L(FG-A9xlZ=f^HIH&JFet;1Z z@OU-vi6)?o0&fg_?y2kz_2~J6n9)!Izog<9zE9)pzaqItb%@`2=Hjz3Q}>dIwpnS% zVd*KCA6#>lqsZo5G4<^78EIyM>}rC*V=fT{9%L>Mcs#^6OMT_EaFBvM@gm0dv*jJn zT0~~Fky299ZIMY;Udbsk2NmW5`#z{5=L4G$kZWwj3rfnquTgCs`;>hqTR^Vc#MJcQ z!GmC}7nD`<_VU=8`|A88V?($>ucKNVl!AJ2g z>q-s0>8b*+IP3~REb4yYLNz+8=gtYHNC9yPiId^T%Muc`xPy~BpS+hoORvb@c93$j zXBAo`b{Weo_DbLi`j#G;JpJCNT*|%r(|nmvV>l~k@W&5-z_Z5V@l_6Ar7S<57ZttH zW0i(cS8>3OWSEj;`KZtj&OfuGFPjti1AIJeUt)jUWmgQV&^^O7>~t2Df>EfvT0S$j zeztH3m9C~A#j#8uYuuScb*aK8`v(@_ybdu2GGAWa`g5mC;b}B?IsD~u;X(&`)mUc5 z$-yO|nlCn2YE)&~#$*TG=s3dz(Pz?iRY}g{x+1sYn&JKEI5(fy_79)`G;Y$zj{ z|E*($pXX)VD^Fbu6m9D4gAd~H9C7#@9hoe%g)R7`-@UGGcDz)rPL|jAJzNw z`@rax$ECzgOi9M(P_22d*nCfM<*{V5Obv3)fNDI8L)QpcJMQR zeOaU)?C-cW-!Z#397+F@Qs+3!bQR8<+TY1 zNkt<|({OsP;9rdDM!6MGoAO#*6{Q$e+7hrL2s#f z8G0qoJ6kPyRR^{`0BWv}W$%WQ2cYz6qxl8*VcLs2!Dud#38Nw%qZ~DE^yW}Urq3h> z2214UJ98Gb`Yw;ck08aWHwqAZ$yF0%L(}0Y8`3x?DAT;Va*v8$F2W!p9&Xe`ZOo+> z9+Zi3ZY<#9l-D?{Lh1H36;4_bN!b!$6)x9_lxZ)!ure&xDK_XB4#=J$t)HXx;P-Tz zy#`{_<5v=$C{4c*eaqBz?R{b4iO&|8kTI;&O>et8vFPsv0(~Y&Iw3A@8ooZiNhbHJ z4R35w6znFLNJs<)R#oNm5KTWCF|z6sA%lAsyy;LYO%|YlGbv8t_>I0Id)UOrls85F zFBan3K>zg~ zM=b;zf3I4+*yVKJjITva24!S%+r6SXm2Xna>X*e6x~`<9Q(6z8(gLA{kHKq1$^^oD zrZ4A-PPboNTpaC>i1$Ruf<^dLs!c`nCaYkyA|Z5Psev9|ZOO02{0qUG|2>7e4jrSw zt}JyduIQjEJyZX-u4Qh(a!b^}`t10^Fks9lykx_yY%h2>t%ST~jU6+g4K4Nd zR`FKbAhhhpC(d~qp_n1ef`8cDQiqnE>l68$tjt9pnAhaolX-#8Y=hj+trWi}x?Cz# z_M-YG5sV5{Z_LC9go7}!{fzBi2k+qf6-!c>R8p{4MF;9DZ16sP0;|a0;^JHM6Y2y9_bof)Sq3^ zXq&_erefJ?0pqS3E%WvwvGas-3!xiCP2W8@_HgnjC=^jqQAwUb2K5A z$#>VNfpbeA?V@9i?AseOw@ZH~1sf4uv6qrx|4bb%xS8(F8?;L(xOvAH&S$TS0?EK) zHtxKhUpRw?Yx2g-f=Qi1@NO+0ZSW^FHQ1LRom2sk8L_91hSM(`SA8E)|GuU>43-;i zZP}xoi7da~yN@wdT=XA#EFv7norgXUSvq4n2u5~Zx1%R2+EJt#mhHp+zRsyTwHZMX zhHE>0w^*4g`^2w@fa33KN2B&dGVZRul@j7|wyQa6`{mEA@j$2#H5}?{~=xSM|{u)JuJ0%L{Qz#X=ZSv8|QIVuFH=_V$kWFf)hnHM$@7 zZX^v>e~}zonAmyl+ngpGgi6VcpixZS?t-FZ^TwAu1p9Sb1AdC5c6aB*=jg}nnPNAL zT<)D;q#AlI1WCoLov}64$6504xu9GOPHKJghXsG_D)JYGKyLMw-aY!s-bfPThMVU- z)u68w-u63n_pvUu7Z$!m3IEveH3rdJW!jiWEh4XLpoqTg2|v|#h6&Vmjv#@X^I!9YBZ!vuky4k$5A5hxMd@9I9es7e%A|v8$RIAbFGHVhA13Z{%D<3a ziQf3pAHI;G6JpN_&FIw_=tm<6H^=M|aVHU&P)g2f*x9j<@EGTij`&Nvmp&h%#;cX?_6l@# zdd=e82!F)u;JxY89FU?k`yi%I6rf=!1jK>}CSn2OX&v4c1GWz&>O9r7=(7-_rV=ga z;v*kRvTC5A<5T)$8tLnm5nDU<*`93m2N`pu%IufQT0_KY7j1#;4n7X{RjHEj%}E*t zK^hOzx&E}U`QygiKrVV9Ph+>wyR!VgX9=whPP zU7)@o`GfmSV%m`-;bAy)AXadc1HGph(MU<5)22jYt-UN)TIVSD>Q8(Kt}pUlFKVs~ zqt4M)6#qtnwq^)hjZJM44U|hvzJc$GseO{a=uN@xhKofLyY_dx!)kI5f!QHrQ7V~{ zx4UH#a9mz6I?70cMKE-=Q$#S@%wdY!I`~Ao2R!BF-kiLpNt%^muE**6hp-(|n6xJW zdsf@{$F3>|Y!my~W^eV2OBKxT-i(0y)-G9HZO3Yzb$r9q2=pgK+TWfurcX)2(AMX@ z>&7j&7X z&P>3pt%k#>Ex>4Ml#$dRe!H-*+b9?^RED@p)>3WJzMo5TBS-OA{HzP#TJqkMbafZ41YBYn!3k6tD<>MVqN;zo%( zen#={5d2GxE?TSu$2r0<*}hWOv;`UYp#UZ{J}gms&dlL>!F9YL1E|{ zHgh9cdL63F%er1A+GmijECGWkSZJ}4m(S2Irv8p=zz6hW3{jx043ciUA+%;|Q0C=r z9e}`^gLhiif&KR9?0X3^!Yz?(+0O>v)xSY(uX+mV5+bpQJxq~e*d%`@?spgcXUo#p z%|o}vG{U&;oz~44){9Qw_RMqX(@JJBKB=9`nH-g&_ADYj%LMex_cXNVw>pxXrkmCx zaZV2vnTXnGwJBQ^$y8-DV4iK2U@dV1)H=@2&fY-9cDW=n}^DJdzKiW z4ki8=T1hEjRGg%9*WiH3oYzfc>;#2$8A`p8Lb{BN-z%X`#tcXlVwBZtChEQFk+y3} z*L&|wU=+znXkNNO6o}ZZ+LydR}Lz$IG_T)C1#CSYKFPR1wSo0OP|4dL;jz4F67f8Pb4{&-$rp9r)s z4GI`nvrG?lXSDf$>!1(=5xtSP-ydCYfB&md{eSTxlkw0AiKNb+nWf^}b~nuPi;6_% zIQ1&UB8rvY?LXeyBVp!jj1`cv?iN-47N?`#Jw0=rSl2Rp@({BZuP67pHZLD{q}nM#GO-4r8j-^;a;MWJ})?lEhXU-ED^Hcy1zng%q~%B zuOeQ2evUHBftsrVAw?PPg`Oy1MSl6O`J)dxyAxE919FNgL}D!q q3GiM({tX-?d zT))leX4^R(oXJLnHcSU{CmvMVz6EkmIfgS4;73qE0Q{4WAmz;!zc-~PQ>OJ!7ZW{| z{ITDx?}&c-Q--e*_Vfw;9i;1}^0>Pwr_#>MRM6#|#!1-1TeF23rpQ=75+2#t*Ed*X z#Buz%=R{NR=OD_`*zou`txuKAs288|J_1Ht+T(m`Ta6IJPcm7IUM^>O@E|m5y&!4L zVWPG;r(bU@1Nv-%>sUID{mE3Y20hea5pruBh_1>hDV^3*0>U`VcY)qgKtO~nvvpSHyjJk-gcM>a+XyVmg5)hMo?#rHpuTz zj=>Hm7v#zWz^>(mKeHC~J*`F`QW{$D!`>4P(>JZ-fS8p5gvE2LK2BQL=)K8Uz2|*5 zw@%m~xYZIT>r5J2sDsxFt?KQ~y5FO;tKxXZGOifqzIr&-z(qd=Rk}M0of62i!t{>6 zI0h*`(A(R)w6uiSTx1dS7)RA1k-^wOFzxjUM+V#=k);66P8>fW6~Vcq)OjuvE2GE@ zxnpuzHaOLhJz4r{WlHD=PZp6ChXGL(3#GOg-ZT zU}*4U0a-m_EsJ1V>uQXhHp8&;Ncjf_va_?-*VP&9xSe?L@Dbz+a5(-dw7nfNgD3I$ z@nb()=M&?Tl6Fm70Bx|Vx~Cl$M$4XHeWUUvqRhiPu(S)Xnu17pWstf8&_9VpD(JR4 zfog07s{PiSy{!uYs0PLilp)(W_Ulf^-RvY00Fd8)W97K;8`$ zb%KAgb8v{z1`nD=Zh5C%@+;M`woDIOid>5#^ zg@uJdy}Gy#J@bC}aH}T+3c3x@6Tr{BuN_qnzE;4I@f`s;mZf|@X8`Ac1F$&3nV+Aq zy7XoL)yGuGP5)5sXqYlfCKG^|O-qX=^Dp2H@J+#f@SOIuYi}zmyw-@l3^Ee)-8*;g z3|GKuG#b?PE7u`WJq4kJ_;_d8jKxy2GJGc|M@&F_U}VHnCC9L6Fj2Xs_BX~nwWs6= z=wnV!4tQ+G1i|*7;T?1>Y9~EF!9CE?6O0DIKtN#NDOFz*%Yl>k{r%U0fgta9-)v;D zbv}mU4O<`3$o zzt$%p01Zlpe^)9~4ly}PC}#AxrBk=!7JJ!G*k?C%ffz?~y5z$Lc)f>J;L<(0C!7;f zi2QQVSfCx9i8vH#wJM$xJN(c5H5233Qu6(C!@|M>3=36!SY+Q1^C|lZMZeN}U+*=3 zmd^DBL6ww7CMNiyso;jZ=hQY1R6t;#KxCfpPZF_yAP5^pma<1T zfe}?zRe>unXCz+(jKhN*YBF+iwE#pfQ3)M*r;W4^c?81MLk}jzTy%+MxgbTyqaoP% zdZf0S`NatI)dh=zjpOtFIjZ literal 0 HcmV?d00001 diff --git a/docs/demo/sum8_sim.png b/docs/demo/sum8_sim.png new file mode 100644 index 0000000000000000000000000000000000000000..8ffd7f7a196e2b53b1361eade738ac346d3ac15d GIT binary patch literal 13434 zcmdUVWmsHI(7c?v~*0?oM!bcNvDk2WA-9 zA@BR{x7U8V*Z$t~g;CVXo6y9YiDD^>}2FZb4uaF{>DXBU+eiX>JT3B{~dz*#NX`YFP zr!^H;Dl|LS9##yLe^h;f|ZQY1hodOL@Ngk(mhqsjZ$V2a%&!@4i-@bKY8pCenoA(GZ7=%IN(Wc~U{ zAeEa~V&sLU`JC<2$A_Adf#u61YeRtri=GI#0FyA83!x^*y~ZbM0(>bN%i*qzjv!rO z)!7|?y>t7w7PF%(3%$iqg@Ri%k$`2xXqohKBGaj}`zH=G`hL$4xA}AUvP%JIFf&|S z#WT!@Uxq$TpTI|M2{TSYZU-D75znT+KyWqZam~5nU>}Vb1>$;)%*txAFIO4It6(;% z+ex~hTMiXzPDMqaS6cb{5>t9pH|7>b{4}N|*p0_8dcqT!~p;wP61goE{ zeTFShWgWNt3GjkAlL6PZ8s}*rHT=4X zI?IwU33#aKn{_z&CjBWaGNT3I{gH~Bc5hp~ro{E2Fv)(+Y4(0tUIhQ*IcZ$^-rm&U z{rv+jDjXh{lJYU;XNtvg<@fJ0jMq?KVYK|cBY;Xzc{Yc6Vckp*NRR;lxZH!ynltlz zVKPvD^*KLfc4=sszHQ|S5cFX_1eb94EfgV5w4mB|HVJRlHp%i$7o?;7kQ^+j)g(J^ zVB`5ROr_NanHLrSnYHBJzNqq?= zcU5Ea^Fz}lYx(f%5~!Gg3qy!!mF67;bn<1$xa;?*Z2eoo+Pjthm3-z8funkL?%^>a z%h%*M;N|ysd(ZsZk3Xvx8FI&Qb8_dGJ$b@QF?}cG>dY2Llg(wCKZO45Sy;;rx-o-h zG6~*nYYF`#)*(~P&d{jwfWuKmxn9&{6}jnqF+hB5tjJxkst-Sqw^~a_MaBH=BgtQD zwG<2LKWty}(ohs1(dD|>kfU3AdWnhSsvb+!ad0v)^EL$+*3#_K(G)z_kesYx;#P)L zta91K8xDR?zAH9Murq47k#FfkEy5kQqgcIMj@4HQw;M00+^9|!#(O?BsJb+onwAD4 zK;Yku2r)MX99l9{QbvXpNzDm96l6R^Y$lJgC1fwT687C+BaDglno>TOgAz(Ujs}%; z@4mu~DK2J|f;#ZGjWl=X4DN8I;<_>-&7-F3g)ncD<6z(`mMWPWO0Rav5)oCFY@7Nm zuXHd|Cp$UF-|kV5*a;3k_pyWTDdr6pt3<~szso5;zoorz4QlXqvPxA|E3>J9tY$#6 zbdViMWb71MX9!RETp|j^^^)iAU9kn`^$eLn))24=_?y^TM4EGW=7cUeMds z6ZqrTE#Sw3-(a1_)h*e4 zo=f@?ghN}d>tjATLiM7|Gg5bZ&aoY&O(Q1EXz|fwde7}dy8ve)u3)Bkzc7G|&N{=T z;rvDTDCb-KMQ{^bIX}Kw54|J{%9>fq`e*C6@WjUk^D&%ID_h%qRj!el5q~FGW_*#w zVG2~sjqtX;2R5wVkve0UuY2ppTXg9lOfE@9!;ElUg-3ylWqP~*?kBWz z?gyX>wAKC9;#)a_A7@mq5mf>Pu1CMUpq{Llq={Nk%1N*(a!E~8VmNxMysnyW&>cB8 zpOn*PVcI)f=ZE^c-Fb*|<5oOFzJo%FqX^A$tWFu1FXe^l8`A1aRrp<1cqNT;?92#~ zJ-*?c16Yl+TyCVOav(kvc?2!LCh-msGLQeEUkZguy`gw(7e|3fm#hKNpx2*oY(^t4 zz+cl{FSfYO9jyKj2Y6l|h)0x_8J9t@?Yri5lk^(5;<;2^#>2a?aj45AGucmfv2Wq( z?;pZu1fB^+eQC{}oN?c}PU||;^jMU_jcQo1ihr57;XWDF%`Gb~_MZQAjy z+STP@R%&|kLd*PusCR*~8PV%1W&NJHN!#4ShqZuhbewww@U*LRD=YJf2K&>q(4QPM zLIRaD7O&mD=PaAlk?gl6xiFLba2E@j2979IiwbFlNWu!N_fY|q= zkvTv0bVh(074d@yEU;pI)Q=@BDo+!OtW?_HU5xsEXphqu;j?`oH{jN))=cp*;qtu> z4R?$1eUYov%Q37J$Qj$iFk3GZ`)yYDQ|UJEBu#d#vrzx`i)twhkOW^jzsocPcO1Sk z7{mae-aN~uKrIAJuB^~soNZ5e)pSz`$yu7&mMaa*R0pNMfBG0jd}1 zT}`a~>9ciXAI1i>X6Ni5XT+wFP#n3r+sa?X67Rp$i-`sqtqPp${RFT7fNZU!3h}Uy zSCimMdA1%%JYk%inab|%1tff=6ZHPfEye%wV@z!=hgAy0?MmWmMNQ~MxBMNVF(5!} zu+J2RhDLC|q4nhwp1grxFi!zjgJ8vTrPh1{bgz}|KdKiy#@c|1d7&gCcjdEXT(e{F z@x7knW^I;}yO-#D>u}^8!$Jp28H|En+9$hRDtC+u(iI%yzt_W^oSTlDOR2Uu zpD0!oeKU{dde++RR!aIWMT@DasFag&Dai1XQdyapq`d_@5=qwj`V(bhV`79yQxopq zTnV+YR?e3<+$Z7KXu^y-AUm&Fv_y(<7JywDH3lPFUW-}i@AW1n&tZczt^1u)9UT;R z16j&TzChkjTV)MgEJ2AorRh$LRiO^ZFDjGb;`1dAWU@z_PGErVA;FU0DpvULb+5J^ z5)I_OX}0T6l^%ckHX{`R)H;HPxaQ$X+O~>Z=HPrTZBgxUTm+vh-^1Y>wp^eGLNOnd z50ZD6Av2tuPPQWr#~q@PFqvSXkO`q7i*naX>&T(e}dA6W+@>knqISYF`7nKCwxLfo*lx z_rx)2$jfWI4pkF@n*kC~B|Kw)Cq#dMU1z-*TL}%7R8qnt3y(_Cd^Gg=nPJ){Eobcf^_Dl8`Q>*~D`CC|QzC3g4*cPH!7 zI@3f4hnJPkbXUL%<{b{t+gbQ;G`$)8T@35BW16<*O(|t zgoPEA5KFILiQ&eCx3{whv7AsTW&#G707Au+F;>d3+Qi0%9zeR9fVDMNNosY@g}zxj zNS*k*JAK{3ikx)6LJI~%?SZ*vaSB3^=TiB;gbMzaS*yw>0n#cRP~Xu)Dg?K&R>&Y) z_t~4fXCST+3>#4Z@s?MJpB{3r59tR30BFkNu+nKh@D5S-;;c$s@VQU`TE{qTFVhP? zqXug>PcY&D9Q4M7s-@2gZNQ8FGYuuup^-S)t@kGY)udT+({D~2AXCrJLIcn3$I0_? zi4h`rH!vSxJ)xS#SxvfoDv?%7Jo~#p!?zc1%vjDX=?ncHSMJSh+v0Df+#lD}(;K(8 z(UA)a03eso69P6NGBLuFlOu1|cS^VEE@OINxOUdO^<9!a#EYaR&B+8;m22?A;V&|FPCKe^XB&)o>%eo8de5vJv~{6^NmH=JVq zZX;hgD$#N4?b}Q?S82&rqO6!Q>z2El*z2Wgl8@soBXGOvw2kCu}>4RN49p^m$oJ-UA!YTE{ksmp|_VS?n6S;vz3=^tR#N!Vm}@X5rrY7z8;Pa0WWov2u5B4k2d2k0rr+U>B`D{$EN$%~zrwwYF-@zKIS~YK*iIMxW$yr zxYTh!elRW5JTK@XT-kVMkpJEQIa&GdH^s%%B`65v<9Pt=UqfXjH8n$m2@(hxn3%$X z*KTg}Vh2ZX%Z5lbeWZu?eDyrZg{emRG$<V{Hjkd_vggJ3?nk*-!e2g}$^>?;Oc+a&pFkst^3b#QHX0q*fmj{PPHkw%)%- z6gpJs6`N&tNKM?YDg6LzJ=T8-2P{VI70^+e65%N-seL@FiQC%R3YHX?Qr6C^S3Z%2 zjilRw_cyti-L`I?kY5p;$8A&kdE4zSzSXk`o4$IK5s^#}pN#gK27bQZyl4Ooi|f!) zPG#C39Q|aO9asICW7ct42%Bt^CukW-2R%;Qci968VfNDnmd9F+pTI}z2W7$ke=BF)VUzMW_gW1nE6biAexI(&j)(YQ zxy;VGENMsR`!LskG4A_o22N5%AulsdYcYEMp_6~>YQK4J9? zMP94(9q*fYq^jZ(_tXY+8E()$#M8X495jYR@1*_6dS#}|76*Q1=VkQAo)V;1&L(e+ zrVBW0G^@egk$Y1VhzE>pO3Lh&Wy~P?4r4Z>)$;YF661j&)Rk89+mJusgA0@Pr@u8A zzF6mU>@A;L{@H*{OG)VwVM>^&9i5V%slIC^zZ=gPp9%=@Cr}`x61B)~4aZVaO0=?D z$P5)(6MvP$*4*{j`8rn!Na8^n}z1)t-u{Mr#Xmrf0G>mKpgkq zsc=asUnQ2!gjB1T1QT#**IBCWI(mfh^Sl`>wj4>`)|3#>%gx6lDJ~=u&@(h`X|WH5 zhFujG0}P6avR6Mpc2y|31yclXM$(L$qoUE$7Wd6_k1eEf|IW(OEZ|C&H#}(? zjto$Zm^{?Ej_KL_Q&h;vNW>YJL@SsT+=J^X@F?aT0a9b_T64WVh20omz2%y-hMpjz z2;G#}bwCT~4=TS~qq8!Rche9vpUZ6Np0@yQQBg5oUS8hU6lO1ihVWqe6Dje-Z;ztB zMN+Sh0{{SacGZSI#k6tU>8*(K)qz5@eRYj|1eoiv!8bsY#m*rJQhW^}q_kZ9?e{?} z(4WXBGn0Z8Pkc(8d}+?k=~2=zQ#?2CS}sQ|a+`f-3b)hqxrK)pe?;o7{X;_;6~#?y zW0X`cW*ytx8Qh}l!l9#>f|{a%^mvLdA$N5Ihimm*sw`NKasYWhE_0x(O=;7|Z(uGq zB{|W!K$GQr$=M&nWyZtu*=Cl-vO&-afq7dcI&5AB)Qoyq@sz%J37IC8yVwAGN$3OI z10Jo*vVAo_QXTDCWjDLo%k?QzuDeI#@l#2j{Q{eWcwSB}I5`XpX$$4XRm+iuRkg5G zysl6-z_S3+1gZD43VpWQ$;>Sk*|L3r49SyVEOVI z4Xu1~GW%wEBIk!q<3jKUgF-YsQ-UoMQasbtA3sWx(||uq zZ=f}78u}S0|7X74D`jHD~R;#kT6{Lqiw(pD!UpR9F42%pjac zUDpZzL&vX-{}cN|qSxe6Wr>i3&y$vv?dFLp{E>}n)GsKdHPWNma$d1cN3%_ns&xl7 zgxpe?yrDpSwI)CrNq-+5oTv=S^7?>I%b`f~pR{)KwJ~&*0lBSK6eHO`qoq zU*|S7_y*vsnczBHUgJu01J2G=}XTOF7*Annzm7Dbb z#>vUe3wb-z;og4!QR7k4H-7**#VB@5qwCNYy$kxp_~X4P;y z@+kUOmVy=*hkT{jk8O^`93!KM+7}Ned<8dXtU8AO0*Y$~vX$$sMZwn=OO|WTb|HVaoCzX^DN+rS$~`q@ovI&rPH}$wS1Xw#h&xtvnO8L`KVZP^cKeVcP~VF>`GA#8=E&YDvXKt z;z(QRWkDbuv^*y0Wb1eKtWS^XGi?PJ@y*5U_C=0E`(p;?3#HUoA;wj&cj{}PqseKh z9@_YfYF2vsLi-^-QBl8GeEhHy?+@QY^8-IH;M{;GR)U^2$Y?G=&dQ%K?uu`FKRUnf zfY^9od@66bu7iDNwSLpK$bJ;)D#P1yr^fdsb);9T(L$01-y+t;8qi?-{N9lYdnZo? zYlP2Sy}47Ry=7oB0jE@54jusCY0Pn5w0EHb-HUUoMU%Ti`b&(nxnphtXZK00^h1i% z^@!u<;xJpL$NAY{!kdnYl__XSI%!zhx!rG4t*JM$pV4yJjnp+(GQdMkbD^6zVObGy z+ljn{JDydU2Fu6O&ESV5y3Bhl{kz zh<3~1`?lyqq3<7+Mwy|2DL$6p@K4O1hICOK4Y*?er1!F7?pO=cVh#=95TulOUF`oK z+Dt8xEh?BP-v!B}NOc$a;3b|7`LwG;9ux&gyJ^EnDpvMkbXW<9R>I6In{;vWlf zDK#V5(~=MyOj}O@O)qxF#ZL39?s8q@VcFC7&Rwxqao2!?SsSmfyMi|@IstlB7*|@P z&;8WT`DLboh+R5^vqRoRsgL*j0znP2rcLFk5oe4$zA?>a@0L+H*_&C~??TU8-`Fcj z#5>!pT(5hQq{U_=yuLafd9h3soP?odvoG{#>%vFZd9gef*V6K{1AKJjrnL1qH+Vq% zn27@VGw^rhfP`rIS{AS_@a*pR^7tnAT=YCguPurZ+7=;7ceN!y@YV#Qny)UipQ;Yi z+f|V7E<2ijOsMW~^42EZvqQHRzJfVJB1~3g=dYU@w_&q3=IcA6;DijGn56l%+%2cTUs?KJkX; zw{g@l?C);-(tKxD_oceqBILd)Cy!4~rz(i5#Pop8Bv>!r z_sfgrx*3`AMSdFYPl7X$)0NC4cXxcFcyS*7sdb5pP#7`2_xqgu{P?VR|49A#+@xY-##1AYtT`?YsqYEq;M_(7VbHok@7Y_l=v-*6DD2qTJ zZTkENH-SRQ&cg)4;4RGRTn zr_X2(W4%F&y$rpvbotncec1iay_+@hEPYW_+FtaYiC4>aum~xuMGh~fIQ4NIe^9@a zGY@$GO?p!0%5j!Tca3w6=}8L z<;AaG8XY_(&&JBqVeKBCy1$rog#BY%f$Ue)Q-{_amr$Ym^mFfpd$y1^&#l{!%k@h#}n7hRF-|A<74V-Dk%*jWXwefxdu*R?lqfj`6K$dW{* z9o4kbzn1za72;c1SSY<*!~}T4t2>p`FP!Ty^x#q^umSO;Np8~6_=-MhwE+?H#6<3 zpVGe*c69F)ste28Wohg-vUl2o-!RpKZb_rC@|)E>{ltI@6J(Z))ih*;oLmWbT&YLa zgpS7tP9X?`sR{3d%Glkb5;OEuS}bjNt6o9-uikxklMnE#x$0YefGzSm5tt`3zLIb* zhpMR7gRE|bTsLxasTp5lhS8Jgyu!Z_F7|Nx-23ak_}(m1(@;ooX!7-vL;%I@RzG^z z{vZq@`q4$jmO;#cCP;#3X#G&Z0RZ#rN>T*f!YV*J_Q9dIH_#~AHw+9)3JTv^u)6*@ zpI8GvHW)6H=iqK7%cohwytAlIV5WfSu?rU6OuSoZiX;$EIGt92`rd0dM^=Pkb@IMR zwcSQ<8|xA2`%N;bbYxpd>DREMeJZk zW_wWBkPp2)4~v33nwHaVs2awk*shPU%j*%~#pnbP2@u?}>h)tfScx+4gLv85@4CBL zpVcvIyKbJY1D*q45g!Ff_fnB^yAGq}%&$eQ0skm+Rcp7J+P60JDA!AuB>ta>&fT|7 zn3R+~8GAFZ&E{?QWFma5{LCxO0+*#hW3r{b+VF%qc`!UCllfhuakdb*jSfFs$ET;o|z z0_WhuMmAm={mNx5<1%=?%GiTDLX#7YDdCeF*F@;Ea?|K7^pzp%C+pHRnLv|z_wDJc z_N7zBvROefPeFpc5hYXci8NAR0%L^!OpDV>%lC!Scy9|Z7jqzVE=Zi^p;rxOgHeC-#Uie6!^B*|4?NXPbMvLHk=MC#zRBGW_Qo;OmUHZ*@!yL}T zEK>?N^_Q(bNMd=>$qkEz-)G5ju|E+2DB5%)LdCcYl$%Yw*3J8r34mjGMJNeRwKL;5 z^}CRsi;kbA-z9UuFKJzC9U*pn&pC+Wkzr|YmXRZdPs2MTHR|4XA>_)yNFY?x`vK8q zw+%z|yApD4;yQ$2eSLWVE8k8nGiu1}4^kI2ptL>78$6QLC@ZYmOpsp~{;}O>%Nv0W zDIvePI32*ea^U|ddD{M!XY2A!+O(4fb5YEuY7NdOnMUB{=%SV1*qo7#Ma+en_#B7u z6?C4M#`p7iN0h`-)j8>|zy(LR?_Ni`n zh*Hm3}s8PaB+pCyVv)h&2Cofey=?8y&e@Mz_jRn^%5Dn{yTte+|o|?f+!qshoqE0 zBYiS<-#l*hZG*8{q*qu4mAerMYpHwwL-4Kqc|H?mYPNky(OG(MU}K&1?w@DR)Nu)q zCo8#htN}@ED#%#=UlG0R9as<(V)mCnr1$$b)kl2|4S1>&Bry{OCjCdz71aj;0reuT zRPhYD6=?oLBGy*>d&I)-6j4m2?nh%=9kU>_a9@?Ez{)|xekN!Wa@;1!%9zSOj{vw; zW+MR}?w`_WWLC$c|2K-a77=>!4(nupJ@WG%iy0a*#wR4?P3aYD#oDGc2y|GKO8x=7 z+}xTArCDP2(c+r%EvhmkM1$N@FDPNIuU@7v3@E7U>K3%k-ptM$VlsvUtD2<`@vin( z%CuL-9H4F^q=p7FBFZ%$Uem&3X+DN8EVKU7tVaRAw{yN4;h>?TU#!Rs1=gn2BHU5Q z#1HWXx^06K-whA@?ASsY&#IPknI)oZ;EDsj7mdHAeVm45C%Uf0?d?y`21#AYcp&=Y zn^cKfqO6D)vvuqQk7l;&oM#ATSa%rw^Z#^Qj2H6*x@{-e%u0w<9wUHSp% z?1*~NWtd9TuAp{an;l_|;(w*~)1I!MVf!vLPQ#UcXf{N2scc7LcNfwc9CuX zI^e77C(Y*{_!26nh71o%IYDNcT=<@KVnFn$fIm2TJZc47_Q1euxs(p-&m-Aw)^IdEqcS;HqY870a|dV2bIN=ji1malBQ85ALxn(? zS6+txH*Uw}WlDqjR3}8VdiwcuI`o7JaRPy50jIr@6#gugM#oQ#)Vbf6UXy&q-!(Db zISZLys}vv%XpMN~oq(D$D5W|)LPuE*o9xrsTpP>t?YN0fg`Ld?i|uKr6xb(={h=@I^|c^u=p7jN>Reu>;dT!Yd2!KGhmgT zY6ATSPSsPFb0Rl;9;MycUq+E;XiL2Qmn+|%&qj$0_@qi^=vZrezx`#!Jrn=-vk$3UJ^4TSBXE3l zA4e>m^irk@o&GcDL?g}`2c9>)gsNhF*{0`Hz5DnMJR)!KtCGD=s*Ma(jhy-LaS8q3 zWb(N#mPB4$TOUHn_Yr^3Ew5DJrKr61$onpz(a`d9q;aKCBh)q za}zNA7V};!*TvOvoyu^qovg_jJCxjkvrl_5gK1;Ys4mdF1{Vp?fBc*(*X zNRs{gw=h8*-q@ahAwzgoQer?o}`@-FrZI&~&AtEqRYj15Y)+TBi=$-w`Bg|92k$>FbOvrch>69mCm zqoJX}^JxduF))NkiiricSKbVE<#Z_}lF^c22+D(Ak{ch& zNt)x9lj-BdeI)PH8vmg59+Q$i(JNzAdbycT^KImO~;G(B0@t%e-9)) zcUMKnB$%BszBQo>xfK)Zd*k8pMxK~EWh^6teoqZ+*@Z*o&4q=sY!<``%d{mLt<+-Q zBZ);mXWSc1d$I1yXCqK%>r5uIag+~7XC z;cgdHP&Yc1Di5`7Q_wwVnlu~h`qn-fkFCt1XWe#{2`(lj$s@{GwitYE$^AZnh+I~d zvt}JV2pCIt($vGTm8~!NRKEi<4l?6v;RE&hTB|Q9sHWHp;>KXPr7DAhK#|)9S}vw+ zSEb{8Wz%xD?^AVUIYa0ll+91!*2N62uf(q&m!~;$dFC~;U^Zvy)H}|EKW%_u^KKGz zmw9v^Hd~Ip(-cmMb~xK;A_#ad7diVGwd3G6Q{T5uM)YMk>v~k|HO??_P0%=L*d4)H z^C4I7SlflCYBW42?y^`CEOjQO_J|CG)wBj`g%e7~#WEan=IW%w3FiQCP{TyCzyddHgr zYwuB4*$CN&yw;YE#MXVo&4}*-myqnaRW4td|9*U7)9s5ca#}cWIqTdqe*w)7835X5 z>;mM0heL70i)Ji&qHA`LJP0h=GML<7QM7yE2N~&RrVyhE2Xw10e^?!1cTxJu!aG5Y zh>BZJQ>dk;6Z7`K<-pUmrb@0Sz{k>jS}#+5jFCmp$9Zk1EO+fk%f@BCi4VZ@?feE^ z1w3{6vs*eGG4I1LBePyO&~0>bA%W>2h7$Y*=C|H|1&;tTT6R-y;gQ6@onYSZWFHFDQcKqW;Vztbt>08=&NbV0N`8Tr{R>AiqX>TCFg>5$uvD9-q|&M)*K=CzQHc0qeeqv zdJ^773MYFr`@h)|1q@LLrmPUV__B2KE$jSKfe*==J?eUP$CJKRDh@!d!7vk_&hS7N zeB%yJ;@0NhHr2_qLI#B-|IT&U0$v|TjIO$~A`cJX4sw*h%4yJQvu>eO1KyOB7PEU> zS`5KNNl5lu^}+3_N3h}hh}Yc)$Q0SX5@n?7-X(a26oe-+{4ZYgA2EY8m2bS+cLf z)$LZ`{0~s)IBS3_8R}6yGP_?qkVor~Setup
 $ git clone https://github.com/project-oak/silveroak.git
 $ cd silveroak
-$ git submodule update --init --recursive # initialize submodules
+$ make update-third_party
 $ make -j4 cava-coq
 

You can now make the Cava libraries visible to your project by adding the @@ -251,7 +251,8 @@

Example 1 : Inverter

input:list bool

simulate inverter input = map negb input
input:list bool

simulate inverter input = map negb input
-
(* inline the circuit definition *) + + (* inline the circuit definition *)
input:list bool

simulate (Comb inv) input = map negb input
(* simplify simulate to create an expression in terms of Coq lists *) @@ -446,7 +447,7 @@

Example 3: Bit-vector xor

Circuit (signal (Vec Bit n) * signal (Vec Bit n)) (signal (Vec Bit n)) := Comb (Vec.map2 xor2).

We can define an interface for this circuit that also takes n as an -argument, and then compute a netlist for any number of gates we want.

+argument, and then compute a netlist for any number of bits we want.

Definition xor_bitvec_interface {n : nat}
   := sequentialInterface "xor_bitvec_interface"
      "clk" PositiveEdge "rst" PositiveEdge
@@ -1281,7 +1282,7 @@ 

Example 4: Tree of xors

(* The tree lemma produces the same side conditions as before, but we solve them here in a more concise way *) -

Here's the netlist for sum. You can see that no "loop" appears in the final version, just a delay connecting the loop's output to its own input.

Definition sum_interface {n : nat}
-  := sequentialInterface "sum_interface"
+  := sequentialInterface "sum8"
      "clk" PositiveEdge "rst" PositiveEdge
      [mkPort "i" (Vec Bit n)]
      [mkPort "o" (Vec Bit n)].
 
 
= {| - moduleName := "sum_interface"; + moduleName := "sum8"; netlist := [AssignSignal (NamedVector Bit 8 "o") (LocalVec Bit 8 1); @@ -1633,12 +1634,44 @@

Example 6 : Sum the Input Stream

port_name := "o"; port_type := Vec Bit 8 |}] |} -: Module

The netlist for sum_init can use the same interface, but needs an extra +: Module + +Local Open Scope N_scope. + +Definition sum8Netlist := makeCircuitNetlist (sum_interface (n := 8)) sum. +Definition sum8_tb_inputs := map (N2Bv_sized 8) [3; 5; 7; 2; 4; 6]. +Definition sum8_tb_expected_outputs := (simulate sum sum8_tb_inputs). + +Definition sum8_tb := + testBench "sum8_tb" (sum_interface (n := 8)) sum8_tb_inputs sum8_tb_expected_outputs.

The circuit netlist and testbench can be converted in SystemVerilog and +simulated using a SystemVerilog simulator like Verilator:

+
+clang++ -L/usr/local/opt/sqlite/lib    sum8_tb.o verilated.o verilated_vcd_c.o Vsum8_tb__ALL.a    -o Vsum8_tb -lm -lstdc++ obj_dir/Vsum8_tb
+                10: tick = 0,  i = 3,  o = 3
+                20: tick = 1,  i = 5,  o = 8
+                30: tick = 2,  i = 7,  o = 15
+                40: tick = 3,  i = 2,  o = 17
+                50: tick = 4,  i = 4,  o = 21
+                60: tick = 5,  i = 6,  o = 27
+
+

which produces the expected results that were predicted by the model in Coq. +The testbench generates a VCD waveform that we can use to observe graphically +using a VCD waveform viewer like gtkwave:

+Simulation waveform for the sum8 circuit. +

We can also synthesize a version of this testbench and the sum8 circuit +into gates using the Xilinx Vivado FPGA tools to produce a bitstream +that can be usd to program an FPGA chip. We can hook up this circuit +with another circuit that acts as a logic analyzer (ILA) then then +run and observe this actually running on an FPGA and capture its output:

+Logic analyzer trace capture for the sum8 circuit. +

Reassuring the actual circuit behaves as predicted by the Cava model +in Coq and the SystemVerilog simulation.

+
Local Close Scope N_scope.

The netlist for sum_init can use the same interface, but needs an extra argument for the initial value:

= {| - moduleName := "sum_interface"; + moduleName := "sum8"; netlist := [AssignSignal (NamedVector Bit 8 "o") (LocalVec Bit 8 1);