From 1f429eeba125e65ba4649045196d043a4acac31d Mon Sep 17 00:00:00 2001 From: Cesar Strauss Date: Tue, 13 Feb 2024 10:43:27 -0300 Subject: [PATCH] bug 1220: add a few more slides with examples I did a practice run of the talk, and turns out I still had time to show some more examples. Added: verification of memories, streams and partitioned SIMD --- .../fosdem2024/fosdem2024_formal/.gitignore | 3 ++ .../fosdem2024/fosdem2024_formal/Makefile | 4 +-- .../fosdem2024/fosdem2024_formal/formal.md | 30 ++++++++++++++++-- .../fosdem2024/fosdem2024_formal/memory.dia | Bin 0 -> 1850 bytes .../fosdem2024_formal/states_input.dia | Bin 2106 -> 2210 bytes .../fosdem2024/fosdem2024_formal/stream.dia | Bin 0 -> 1701 bytes .../fosdem2024/fosdem2024_formal/sum.dia | Bin 0 -> 1232 bytes 7 files changed, 33 insertions(+), 4 deletions(-) create mode 100644 conferences/fosdem2024/fosdem2024_formal/memory.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/stream.dia create mode 100644 conferences/fosdem2024/fosdem2024_formal/sum.dia diff --git a/conferences/fosdem2024/fosdem2024_formal/.gitignore b/conferences/fosdem2024/fosdem2024_formal/.gitignore index b43b63175..e45fb553a 100644 --- a/conferences/fosdem2024/fosdem2024_formal/.gitignore +++ b/conferences/fosdem2024/fosdem2024_formal/.gitignore @@ -1,2 +1,5 @@ formal.pdf states_*.png +memory.png +stream.png +sum.png diff --git a/conferences/fosdem2024/fosdem2024_formal/Makefile b/conferences/fosdem2024/fosdem2024_formal/Makefile index f99d01114..9012dc9f0 100644 --- a/conferences/fosdem2024/fosdem2024_formal/Makefile +++ b/conferences/fosdem2024/fosdem2024_formal/Makefile @@ -1,8 +1,8 @@ all: formal.pdf formal.pdf: formal.md states_enable.png states_one.png states_output.png \ - states_input.png states_verification.png states_complete.png \ - test_enable.png + states_input.png states_verification.png states_complete.png \ + test_enable.png memory.png stream.png sum.png %.pdf: %.md pandoc -t beamer $< -o $@ diff --git a/conferences/fosdem2024/fosdem2024_formal/formal.md b/conferences/fosdem2024/fosdem2024_formal/formal.md index bf26aa07e..f9b32deef 100644 --- a/conferences/fosdem2024/fosdem2024_formal/formal.md +++ b/conferences/fosdem2024/fosdem2024_formal/formal.md @@ -44,14 +44,16 @@ date: FOSDEM 2024 * bad trace: -$I(s_0) P(s_0) \wedge T(s_0,s_1)\overline{I(s_1)}P(s_1) -\wedge\dots\wedge T(s_{k-1},s_k)\overline{I(s_k)} +$I(s_0) P(s_0) \wedge T(s_0,s_1)P(s_1) +\wedge\dots\wedge T(s_{k-1},s_k) \overline{P(s_k)}$ * k $\leftarrow$ 0 * base case: no path from initial state leads to a bad state in k steps +* if base case fails, report the bad trace * inductive case: no path ending in a bad state can be reached in k+1 steps * if inductive case fails, $k \leftarrow k + 1$ and repeat +* otherwise, proof is complete, circuit is safe. # Single register with feedback @@ -159,6 +161,8 @@ class Formal(FHDLTestCase): self.assertFormal(m, mode="prove", depth=5) + + if __name__ == '__main__': unittest.main() ``` @@ -173,6 +177,27 @@ DONE (UNKNOWN, rc=4) ![](test_enable.png) +# Verifying memories with a "victim address" + +![](memory.png) + +# Verifying streams with transaction counters + +![](stream.png) + +# Dynamic SIMD + +``` +exp-a : ....0....0....0.... 1x 32-bit +exp-a : ....0....0....1.... 1x 24-bit plus 1x 8-bit +exp-a : ....0....1....0.... 2x 16-bit +... +... +exp-a : ....1....1....0.... 2x 8-bit, 1x 16-bit +exp-a : ....1....1....1.... 4x 8-bit +``` +![](sum.png) + # \centering {\Huge @@ -188,6 +213,7 @@ Questions? * Discussion: http://lists.libre-soc.org * Libera IRC \#libre-soc * http://libre-soc.org/ +* https://libre-soc.org/resources/ * http://nlnet.nl/entrust * https://libre-soc.org/nlnet_2022_ongoing/ * https://libre-soc.org/nlnet/\#faq diff --git a/conferences/fosdem2024/fosdem2024_formal/memory.dia b/conferences/fosdem2024/fosdem2024_formal/memory.dia new file mode 100644 index 0000000000000000000000000000000000000000..6f030afc72269ad6be02d1b8f9a12607fba1a647 GIT binary patch literal 1850 zcmV-A2gUdwiwFP!000021MOT(liD~CzR$04k;`rs5!TDHGMP#39#VVQtvw`r$%PVF z1Kt>$vdu7D_P4KOn;Gx}28;+~OyyDbG-|i3@B6yt_I&*GGz+Xp87F=e-t{1`dzK8x zk>`h#yWT%vKfiZ-pYCrydcOFe{!U^sv(z`jL?7MtrfE9=Fc>VCOAxFQkw!5H`~^tl z;6D)rVxWu$z55%>+8n?WsnF+&vm#Anf3!%Y6^fa>>y5M6vZK zg1g?khwRfE6vGU*#@R9UTukIBmg0N!(6;(;e$3Ew8JCBh&7;IuCh2NkF=-e_|GQyR zSS89RoZP?rjl9b*sW|a6R^5d*I!R|Dp7>$akD8kxp9ln8gpisH%3W?V!r*#N4tF;? zue;#9?&9;h^ONB`iqly5Y1QQ@iUKLZ+-n*y+Z9%eC?5PYjrLssg9wt> z1dyM8M%$stoy5Mk8@O8*4Wlf5FP#pb3{6))`pVGgkAC8h0$F$UewdzY_|<8KFW;Sv zyiP*E=Tfaw7y_YmZB_Y0d z*ZbSvp09F*YA{8Gl?j_i&#TG-1Tu#E5YX~GR9U3S#b{La5UUtOI0@w13+5>ELKwZ} zz$N+!0f*B~qCdp14CHJ$j^ePIFq|^H%uU8E)ezUbf&sC&KBR@Osq`n)wAmR1kl75{ zHp1AUoI6K48%41v<9(soz^2==+4wkr$uwFHYckjUvRqFggBP$gq33fDEyq(4r;YG| z?cqcF*f4a6c0n|3IPEiaL(BrEML-t^mZKwiEjnNk1SH&s(1GY8z|mNMdER!uT8Zb# z=}P5Ow%nw%Tl0=yFtR!7& z@m9={fAtR;Jj&D`i_J9S@GGdS;M&{bW+gXg>JNbqCcK@~ZBDDB0T-Y?1r!t5($#jd zxMN4bw%a*UrPw5#$@=>#!^Ny7i{6z-*QJ6jv}hxf`_m6)jTWJ{TBMk@PYfy%23TtY z!!EjYfCHi1CjdFnJe5>ZFjfcLWfWb0#;SLShRZjZv^K0{ zGf8V@4gL%Xt8E}*ZQ2jbE~%Mt@mZ*do`Q-fK!&M^DA~-Zh%%(b9bX3-3D1jVl5}iz z4mR3ah8-JSG8;7%7fyRNqJ0Mt>~L(9k%)E!8HIRVoU8v-f<%m07&YHj?Yfr&s~V`QVcoX-+ZA)(7CO*2yknR-usN}vTL=M%1S{y+7{V*r zGK@PVH?8F5HQ0&xC5w1N6PJC8E-q@6iX7eesC=-j{gES`KO$tjlk4c9F0PYHsT|+> z5Z3iQ9OGUQU-UlvP=u>r-<*h3>NqaO zHX^PfIzpLg5wEPpPQ|bAxgSKQ;3Q=9!Jqa30V_Dkv6ZGHfUkp;vXWvf=IJ7qUPnsj zASKj2{<{`Z`sPo*iAiaf@R^!gw-{2xy}1-%#YOq+RjSs=Uaum+KDNS$;&eLPyG2O% zHRfsqMVGsu3$9<#dZk&Lh@#lvUgEo&!*?zH=Iz`Otg)zMvfc4->WHL*3Dq1}j8NfILm8+D-mQJ_94&S-m_=?)gN7-M<`b^AaF9+*sRoxxSe1gR8n9OxY-X3Q zFgZD-UJ09B-|HZCz?Ks`#j9hs;n!ZY2mKVAGOlzAa*lLfcpcBN*Sp}|lWgtiLz>%1MjO(yjiz-&8q*DF=sXQ+?(SkzU5#^W=v_nF^*5wJeu`#JXjIK} z4@FNJ0SI&bYp|}UC+*EXKsvjiR~BO@=vVku8?|muW7&3)Nl9mbF&9Do_$VW$+#|UP oQtEifG!IqQU&li~l!x-;>=%vR-)#LR()*kL0kDUha;;nd0C{YfhyVZp literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/states_input.dia b/conferences/fosdem2024/fosdem2024_formal/states_input.dia index dab3127fafb7528e06ee5e95a36bf42abb8a2c78..43dfac0ee9f33f221f08867cdf78048d0a8f07e5 100644 GIT binary patch literal 2210 zcmV;T2wnFdiwFP!000021MOX1lcTm0ecxZ<^1eD)pCHAVNhOt}@{p=~Ym@uz!bW40 zU~mDR+1ZEu_A3FNu`ys95If$HYu7G3Lamn7-RHC#_~FOTn_%=P;>3@_yD_xDcqGDQ z7%m1s`-HhZJVWN)i#_KfQem|W)Jv~{$bK<5^Yz6+# zO2qVEHwfIRY&0F;e;ADpJMi4pRo@lgx@j8wi(M*4p}P@xQEiigwE= zh~m+s8{CaQK4h=)wCHAf)K5d-TX!WEv2g#X?;6M#=WV*)in!eEW*a5GY?3~2Pny*9 zquvkN6s;23C|uot{E2+bhg5v=+E>*;YlWm6H(vSSsT?^sK|T@4VhABQ8I&^)9OA(J zoLnz%F|4>?SaI>N;{0U3jp8(R{q$7iB8mdxhPl)<-ih{dlBFBSCDx=?2Q41_G>y)T z|G^ECOBBezezCS|Eq4|BUbEpIwW#Uk$@kLr{IjO%%6os-)cd2K_=`YPjouH_-nxJ8 zr~C4+lX>sg(>tz)ytmr$;4wi3y*@mwcD^T)Gt2C_O-)bhqS^G^te4weIx+cIrC^xy=Tm@q9)wx3_ zSiR4XgieS~pshaI$rORu%$HFdo`QrvRLZ)~{K%Fh6Qn!tgZ+z9H<@VW=of zs|2aR(1omoDqO-f+W~pg&R@*i;8f!DQ5FRDV4$gI-7XRhE%qS*P-A+yb|i{mC)W> zX!c5l98h?r7qP}G8L!l^5RF&5L9c{+z)Fr<3|K!_a`I5P$4Z4*w&3vjebc=0hts)XHYHs3^~aUow<|Fs$G&p zAsSOC=uM;>YIndq@7SH6csEQjr5JNSIYth4_}h;_0GJr0I|i{l1OW?Rj=rrJ1U1B< zD0kcv|s4-8knNv`bl!<8W#ge)sD2W*)P!@F?3l6U9Q2etRJGBr`z>1Q*(Qa}jzMW(!YLtZk?Oz1rdg^ zj43($48CKlOgR`NgI}#=eX5_E{QWybLbwYOBD!6`Pw}$K12{KR`f4+3+tReMPlbaR zB3KDlpTiV?;R|#39qfO(iyy_@^AoB3QZ%h?La_3I)aDF8M%rFX8pzOa-jHBnK#*_% zp$(C7MBnH}BK}H_i1kFs_&4o{s+H8?m5n1Zj_9i*BK_5{)i({Gs)wpupLZ{xM+yV#G5X^t`YIz2f+m*-q0gmn&v8l zn%C4i=Ipnc%7Y zUQI=g%{Gy9pd1_S9uORhXpRYp6Gw`XZh|;7DGuVSoD48TG^g3h+Ev{j7Zc!cb<1Sl z`Z7|JZ~L10ww_F>hv(2h3@FZ?px65P#|v+-3+zk`l;%VUp-5FlK!~_*d#Y2h%CLw7 kaW*g@V}dcP+c&KIID4k{{fDE6Zr^|SKL_`V)tG|-0DW~zU-sgGs8h-fk^EQ|~h&b`1@OBCuiw6-(;x3X{NVZgd-;DI^X)`l5hm*FcDhN^-S_kPUUrak<*2%`+RwhIqq z(%#&1Tyw#==HhY9`N?7z#c9m_^xWh!iUPsI+-e%{MRz;NiU)FvHFc{;FYf&`jV`qR zo(IV_9mqd^UTtkx?mG6p=7oDwqNbKd-%B@(&zgoSul-3=?GJw9F9T84dOu7DtNv-2 z>dW6whTboi_nZxRZME*fqk;(1-aV}Mz9*6k)9kcNO--Ak*!+i>>i-mL>7t{_F5qD_ofO}30Xh@DO8tk!+0n2>%fH1cE&BUs%0rLG-sHQ<&(Y`U z3k{JZ#P@Ee{{g4tRqmmzOhVz=fbF8^S%qhIx&PFeE}3EV zeuE@+LSzOVb?9bO1Y)~bMR9me5{BqfR(*ye=iPe75Za^ejqul-w4rj;t@33Qdm_Hn zbYKAj@|SB9Kqzo}nLEXSiyX9_jbsx&E-HxbWiMWhIP;gab;V-)OMFg`RvRo<8|=H< zAhr;ZYXGT(#&vhF11;hLdh=q|w!5yqR1L`mKT|4G_tj>^{G?oo!`CqQ2Dewop`tLY zGNeAA-1Ds;JjwR(Fqux0^htrU1lIi0-$n2sQh&vd-AMZuoGtmvg-OBb%kF3NbP~3h zh+T}8VW3ts0?^NpB-`t7E2_Uy5$?CeXkKZh(%H9L6AxLF%B$j~DR>lALcLK59neBE zDiwA>flAM24JsK_YM6)ymEIsK;Q_dkt0n{1&z0QV6&|=!Vb-9ML8XR?Xi(|Zq0(q>7Cerl$9k&>^{jdkh;ZG!8G!0BteeS;+YcQr zuA(rMb6qaVyXPe{FM$Pl=E=AUZtFyQ4IFx`HY$E9)lgVv(PZuQ5kF>>F=J(cjyeQ-)jPe zY#{toa~@Nz0BB3Lqzt(Pt5_j`4plUkcFk^8Bf1cwcV)Ejtc$e;6`^-Jl2kd_R=aXr zs?zD-VDJu)9=yX}FL-yng6l7aT9^NIav6dFa`8qH%(+y4R?N;wig|$U8Oi+qBr`O$ zS9_L|Z8Wn+&0ND7VgH|$NEXK!(=VHqAv-su=%Y&CrU1ESA?!NhBRO?$+txdx7 z3fYQv%htO4p^%|q0FNM8kCHxKPEFQ_;SmiJ(WHI6nY0i6!Mi##xO`z;#Cy_xNj!))uF_3@KPh{s;qG@j1HdYu&97X}8cGn-12GTWLUP!Q5K+t9Y zLI)xPMBnH}BK}H1LQ3rFWdlS8h`uT#(w_}mePe3aI~yK4Gp$;PSd7eU z`E~=TmEAf+^A=*~{#>(lh+f~;;k9?A9tezH%}(VTh$nt}mjOk_m@EI;(7`s-9#C{= zj)kNnXJ%7!oJ~p8|Hl_(Ml8+S5KP%Xm?D+D0wJXG)OED~@T%OkYX4-Jc-uQ;mk5>! zB50*^+3D3}aCZ6MSnPPrRSi|QKJTACj}!;gx#Xe6FmX_zD^h-m zC3yZS)te00eax=mvRLOMR>}#Xqv-6z3-&Ok{QbW1c`IcW(8k2Q9|TvJctwwNX&S4H zYPQL*u6#(?z`9_d$uOo)_{Ah1jBs~xMa^8P6l|juI_4eR2mWrciDLhYoK8GwgqG4X z6I+{+Bt%U{ZAOy)QaxC*Ay^DYyZsyL{fi{MLA;|F9vCBrr!|CUvj4xS?Ehar8Rx0} kUQI=e%`u*{ZHz5H&z@I$_u=G$rgtCy4~v0iRrGuS04qT*>Hq)$ diff --git a/conferences/fosdem2024/fosdem2024_formal/stream.dia b/conferences/fosdem2024/fosdem2024_formal/stream.dia new file mode 100644 index 0000000000000000000000000000000000000000..a99d28a2b51469838191c94c3c52d557b9e22c2b GIT binary patch literal 1701 zcmV;W23q+aiwFP!000021MOT(bDKyIzWY~Duyd(jFNC_(EA>8yw58eHJBierd;dvP-Pdti!5#Fmv(^Z9sbK&}- zcdvf?`suB$et5Wf@A~W={P7~TRN#y-PTt+C3n^FcCX>x(qXjQ9lOoarf33xQ@*fKV zHUXoF`f#Ht`wm$Gow4~3FB0p}RWqxt-CP7BQl40FufBOq zU+QG*W|H%B!1s!Id=_!`qu#X+FUM))dc~un+vQ5cKA6atRmr5rPxAMk&DJUgqtJVJ z^O3yCE@^w<)mPPp)`G|-i#$Ipo_!bQWv z`SElmA{jAXmLX?C1e}E#s*KjWJx)Al0i@WWusTHX=u0V%T>m2r;!^_14*#sSrj_eO zzI(WEa~3sTHohwt)90R+EA#%+llLb-_GbaFx_Up9XLJ8@9{0t&lXmad(>rEE=B<_< zT$@u)o7020_FWzyNwd67ji<%dY;tVXi*~0jOm?V1)+t25UU;;1|Al)%(Lz}TEEKA; zy~o?8qp-R3pLXx|mPO3|<#V}>_fsG?^975f@>cmvJgcud1XPIc-mCxU`2{P62;QI< zmR4*fex{YJ*|&yf7Z;)2Lh9VlW<~E21i(Ts;5!710)$2H5OjHZYiR~;2gd`xoX$lQ zmPNw3B1$3BUQ&)~*GEVP*9-1@3t8{m&|0p|Ohhh^j$OL0Aw7E`;^+vO2)Bca7h*H5 z5TeIfwh79Lxo)0eOYyW^F3F!uccIvA3O02sk?PExT|ttr{1peGz}=gVpTE_p(*rHN zP9KO+R-q=xl}EPpgBQ3s7RIU)%a^3_K+nid{hJ3*T>5ji-y)k|K`ECjZ;+jC7aR+| z2r>=gbOX(Iv#R<>fO$(bVh}{SVda_bz;;O2y8(fY^ui^tzM(u^FDoR#ArVl;V|83S zd1akC8u|k5++~pqEc6-jxPpdIR~n+4c}q02M;f9Ur2t_VHogOjK*)x7wuxF2#ax8p zl!tB_L!-#57|UuOJY>gwRm87Sjg7b}bf+we#HQ%@H5oDP=z1FP&^t_4hMs?su8>FR zu_++c@e}3sy9vFNhiM94&m+j}bF@B7 z>$mwO2x$8e3o>!i3Z3f^WPS+$8`W6fYOIumqZqqnF;+c+=X7mF&MoeF{>}jzhBYgj zz#}-B#-k3kP@hwH9ilpA1`qZz=i${;hVpb+JKX|Zf(^r@j$;zL-yuDn7Fv;U5mS2S z+`ORfldC-s3|V`1<7j$1@Bl2{=jO#eIw=IDiw_w%#|_$dn^SfzC+4sbKPR0cGB7o*9xFFNfh;GEiS7{6NJe>tn#jC-?LCK1E&sq-B}z@x zHVhpT+rgAjt8evPnTw+Wzdi+yaCZrg29V%rUxMQyBsdx+_$a~aC3xpKKP#OOA-#%l z>u2R;BHT>Mr%w@H3aZ)!AJ^GO4A3aVuU&`(_52zoPR^mk@gPbZ(%c|~rb^t#7N8Q_ z-2XAK%U0sEQHc+s#PO)ae*+~>yDM>h041*PD{(Z064ys1J}U8gC4PA0UQ)y1D vRGVWxsiCXV=JBY_htTF|)aDnZ&9nFE@0xnJ$^9~_hnxQaUw?&Puu=d3v3pFy literal 0 HcmV?d00001 diff --git a/conferences/fosdem2024/fosdem2024_formal/sum.dia b/conferences/fosdem2024/fosdem2024_formal/sum.dia new file mode 100644 index 0000000000000000000000000000000000000000..357469b826be84b691767b7cd8bca93e3168933c GIT binary patch literal 1232 zcmV;>1TXs^iwFP!000021MON%Z{s!)zUNm6%GHrYJxpo6&Z0dOJrrnx-8~zW#mMZ^ zq(ISjeCcm5^>A$KVa1Z=B3lbc0*T}K$kBY?jLCfd^17nh28)DnHq(J&>KbMX9ugMK z^zYw(d-C)z&kvtNfb~&hy-7=P|vLjy9K9QXd6Ul`r}J>>Epu9 z_{7f{-!Y1CATavT?Alb9?{{$>V^Mayig`kmiQL5%lLkNO?<1SSDp5u(dVc)HdCaF& zJUIBOn`k45Tpe`Vp?M%I!?P?)1;h0{--HeX`W7LFwIm&a__r=yl+TC0*dQqPnf)#``vZim)}mN-iMF(%!b@sV|fTY>|*!w@(`^_ zh?AByJGE)>v@FcVZBZ}Vy*DuVqf)WXASl{lQMmt#BUPfg7E{Eyt`+aN5FHIIB-!lm zj>5u&zwtsA>-{Pb3y}!5C+%1Msvp`A)r636rvGW4#;d$S_hvJJN! zf~tTtc@KiJbD^e>SVZw2z%VUWfjH2e0x!D(R{EzKD5iKdUvR;yjlz|dl_6wuQeE0x zx$5J4iAl7S&Cb29GY_~3v1psSX_&5=U(j()*E1)*;7;|RwHLh%BU$q8yr$u8ujcj2 zGd^(a9i;n<(_O?_4e>x<;#ng&AnSnP+y2BEO$=Yr&Ns}7X-`IeciP1&67y{O?_N}O z*lig$l)-WCS4}48J^1H`;mAKX>>LkY5**b9;tN=}zwD1li9gg@YxrRG<%5#z(U5h> zHZ0q-MvmdTQ`>+O;Hg{#0C?Rn7o4#2<#N5nJ}RH`X9B$XPtAJLYIKWXm=bWQTCd}xQ! znpahEdL5S9eOU?zW+^;kDZC*|VH-=~ouwa>rPm>j)0a4DZ{rV095*M9mlDU#i37kb zm{VFijg}ZQn{c3Owj`OgNc_p=Fo8 zWYhHRKRebuu`8W`#tjFcXHE^8j-WV`bx7%R?FFp}-Khy7mgrg{cZK}tAN?KE4VGkq zj`im98C14PYYF2u6Q&F3Y38+OUl)w>rfK6zyJ_|VLX<>oh3jABK}p|>QhP*l85cI$ zl$u4|zHUd~pg`~%8&-}n?3Pt}ZUTMBoJ?)iH2~-h7W zb;!HMmfWy91dntG8a{BWkE27uU5AF&A$ZrJpFoHFYwU2U?@I2Vo16;5OqB>sUBk0{ uB}5AHV<=H_SE8YnsG5RzDf&;PD8JACDen2<0rnF8}}w0A?=$ literal 0 HcmV?d00001 -- 2.30.2