Skip to content

Commit 6ac40f4

Browse files
osmanyasar05osmanyasar05
committed
conclusion
1 parent b6717a8 commit 6ac40f4

2 files changed

Lines changed: 111 additions & 3 deletions

File tree

‎images/.$diagrams.drawio.dtmp‎

Lines changed: 90 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
<mxfile host="Electron" agent="Mozilla/5.0 (Macintosh; Intel Mac OS X 10_15_7) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/25.0.2 Chrome/128.0.6613.186 Electron/32.2.5 Safari/537.36" version="25.0.2">
22
<diagram name="Page-1" id="eKA-p9QtjuDZeN396SeN">
3-
<mxGraphModel dx="445" dy="1425" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="850" pageHeight="1100" math="1" shadow="0">
3+
<mxGraphModel dx="907" dy="1763" grid="1" gridSize="10" guides="1" tooltips="1" connect="1" arrows="1" fold="1" page="1" pageScale="1" pageWidth="850" pageHeight="1100" math="1" shadow="0">
44
<root>
55
<mxCell id="0" />
66
<mxCell id="1" parent="0" />
@@ -2071,6 +2071,95 @@
20712071
<mxCell id="uIBb9Ui2RikNsex4B_yB-105" value="4" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
20722072
<mxGeometry x="2190" y="1615" width="60" height="30" as="geometry" />
20732073
</mxCell>
2074+
<mxCell id="uIBb9Ui2RikNsex4B_yB-111" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;entryX=0.5;entryY=0;entryDx=0;entryDy=0;" edge="1" parent="1" target="uIBb9Ui2RikNsex4B_yB-109">
2075+
<mxGeometry relative="1" as="geometry">
2076+
<mxPoint x="3745" y="1590" as="sourcePoint" />
2077+
</mxGeometry>
2078+
</mxCell>
2079+
<mxCell id="uIBb9Ui2RikNsex4B_yB-108" value="Arbitrary Sum-of-Products" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
2080+
<mxGeometry x="3672.5" y="1561" width="145" height="30" as="geometry" />
2081+
</mxCell>
2082+
<mxCell id="uIBb9Ui2RikNsex4B_yB-109" value="Partial Product Generation" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;gradientColor=none;" vertex="1" parent="1">
2083+
<mxGeometry x="3640" y="1620" width="210" height="60" as="geometry" />
2084+
</mxCell>
2085+
<mxCell id="uIBb9Ui2RikNsex4B_yB-112" value="Compression of Partial Products" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;gradientColor=none;" vertex="1" parent="1">
2086+
<mxGeometry x="3640" y="1710" width="210" height="60" as="geometry" />
2087+
</mxCell>
2088+
<mxCell id="uIBb9Ui2RikNsex4B_yB-115" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2089+
<mxGeometry relative="1" as="geometry">
2090+
<mxPoint x="3729.87" y="1680" as="sourcePoint" />
2091+
<mxPoint x="3729.87" y="1710" as="targetPoint" />
2092+
</mxGeometry>
2093+
</mxCell>
2094+
<mxCell id="uIBb9Ui2RikNsex4B_yB-116" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2095+
<mxGeometry relative="1" as="geometry">
2096+
<mxPoint x="3789.87" y="1680" as="sourcePoint" />
2097+
<mxPoint x="3789.87" y="1710" as="targetPoint" />
2098+
</mxGeometry>
2099+
</mxCell>
2100+
<mxCell id="uIBb9Ui2RikNsex4B_yB-117" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2101+
<mxGeometry relative="1" as="geometry">
2102+
<mxPoint x="3669.87" y="1680" as="sourcePoint" />
2103+
<mxPoint x="3669.87" y="1710" as="targetPoint" />
2104+
</mxGeometry>
2105+
</mxCell>
2106+
<mxCell id="uIBb9Ui2RikNsex4B_yB-118" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2107+
<mxGeometry relative="1" as="geometry">
2108+
<mxPoint x="3699.87" y="1680" as="sourcePoint" />
2109+
<mxPoint x="3699.87" y="1710" as="targetPoint" />
2110+
</mxGeometry>
2111+
</mxCell>
2112+
<mxCell id="uIBb9Ui2RikNsex4B_yB-119" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2113+
<mxGeometry relative="1" as="geometry">
2114+
<mxPoint x="3819.87" y="1680" as="sourcePoint" />
2115+
<mxPoint x="3819.87" y="1710" as="targetPoint" />
2116+
</mxGeometry>
2117+
</mxCell>
2118+
<mxCell id="uIBb9Ui2RikNsex4B_yB-120" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2119+
<mxGeometry relative="1" as="geometry">
2120+
<mxPoint x="3759.87" y="1680" as="sourcePoint" />
2121+
<mxPoint x="3759.87" y="1710" as="targetPoint" />
2122+
</mxGeometry>
2123+
</mxCell>
2124+
<mxCell id="uIBb9Ui2RikNsex4B_yB-121" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2125+
<mxGeometry relative="1" as="geometry">
2126+
<mxPoint x="3789.87" y="1680" as="sourcePoint" />
2127+
<mxPoint x="3789.87" y="1710" as="targetPoint" />
2128+
</mxGeometry>
2129+
</mxCell>
2130+
<mxCell id="uIBb9Ui2RikNsex4B_yB-122" value="" style="endArrow=none;html=1;rounded=0;" edge="1" parent="1">
2131+
<mxGeometry width="50" height="50" relative="1" as="geometry">
2132+
<mxPoint x="3650" y="1700" as="sourcePoint" />
2133+
<mxPoint x="3840" y="1690" as="targetPoint" />
2134+
</mxGeometry>
2135+
</mxCell>
2136+
<mxCell id="uIBb9Ui2RikNsex4B_yB-123" value="&lt;font style=&quot;font-size: 8px;&quot;&gt;N-partial products&lt;/font&gt;" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
2137+
<mxGeometry x="3817.5" y="1673.5" width="115" height="30" as="geometry" />
2138+
</mxCell>
2139+
<mxCell id="uIBb9Ui2RikNsex4B_yB-124" value="Final Stage Carry-Propagate Adder" style="rounded=0;whiteSpace=wrap;html=1;fillColor=#d5e8d4;strokeColor=#82b366;gradientColor=none;" vertex="1" parent="1">
2140+
<mxGeometry x="3640" y="1799.87" width="210" height="60" as="geometry" />
2141+
</mxCell>
2142+
<mxCell id="uIBb9Ui2RikNsex4B_yB-125" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2143+
<mxGeometry relative="1" as="geometry">
2144+
<mxPoint x="3729.85" y="1770" as="sourcePoint" />
2145+
<mxPoint x="3729.85" y="1800" as="targetPoint" />
2146+
</mxGeometry>
2147+
</mxCell>
2148+
<mxCell id="uIBb9Ui2RikNsex4B_yB-126" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2149+
<mxGeometry relative="1" as="geometry">
2150+
<mxPoint x="3759.85" y="1770.13" as="sourcePoint" />
2151+
<mxPoint x="3759.85" y="1800.13" as="targetPoint" />
2152+
</mxGeometry>
2153+
</mxCell>
2154+
<mxCell id="uIBb9Ui2RikNsex4B_yB-127" value="" style="edgeStyle=orthogonalEdgeStyle;rounded=0;orthogonalLoop=1;jettySize=auto;html=1;" edge="1" parent="1">
2155+
<mxGeometry relative="1" as="geometry">
2156+
<mxPoint x="3744.88" y="1859.8700000000001" as="sourcePoint" />
2157+
<mxPoint x="3744.88" y="1889.8700000000001" as="targetPoint" />
2158+
</mxGeometry>
2159+
</mxCell>
2160+
<mxCell id="uIBb9Ui2RikNsex4B_yB-130" value="Z" style="text;html=1;align=center;verticalAlign=middle;whiteSpace=wrap;rounded=0;" vertex="1" parent="1">
2161+
<mxGeometry x="3715" y="1888.87" width="60" height="30" as="geometry" />
2162+
</mxCell>
20742163
</root>
20752164
</mxGraphModel>
20762165
</diagram>

‎paper.tex‎

Lines changed: 21 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -888,7 +888,7 @@ \section{Results}
888888
\toprule
889889
& \multicolumn{2}{c}{Verified\,/\,Datapath} & \multicolumn{2}{c}{Time to verify (s)} \\
890890
\cmidrule(lr){2-3} \cmidrule(lr){4-5}
891-
Benchmark & Area & Delay & \textsc{Standard} & \textsc{Verified} \\
891+
Benchmark (16-bit) & Area & Delay & \textsc{Standard} & \textsc{Verified} \\
892892
\midrule
893893
AddMop & 1.00 & 1.06 & 0.44 & 0.24 \\
894894
AddMulSgn$^{\dagger}$ & 1.19 & 1.45 & $\times$ & $\times$ \\
@@ -912,6 +912,11 @@ \section{Results}
912912
MulThreeSgn$^{\dagger}$ & 1.01 & 1.14 & $\times$ & 22.72 \\
913913
SqrSgn$^{\dagger}$ & 1.87 & 1.19 & 14.65 & 26.24 \\
914914
SqrUns & 1.48 & 1.13 & 11.78 & 19.95 \\
915+
\midrule
916+
Geometric mean (32-bit) & 1.17 & 1.14 \\
917+
Geometric mean (16-bit) & 1.21 & 1.12 \\
918+
Geometric mean (8-bit) & 1.21 & 1.10 \\
919+
\bottomrule
915920
\bottomrule
916921
\end{tabular}
917922
\end{table}
@@ -1086,7 +1091,21 @@ \section{Related Work}
10861091
Integrated into an existing HLS tool, Graphiti provides a verified rewriting engine that ensures the composition of verified rewrites refines the original behaviour.
10871092

10881093

1089-
\section{Conclusion}
1094+
\section{Conclusion and Future Work}
1095+
This paper has presents a verified datapath synthesis engine integrated into CIRCT.
1096+
By formalizing datapath synthesis steps with using bit heaps as the core data structure in Lean 4,
1097+
we provide machine-checked correctness guarantees on the arithmetic circuits we generate.
1098+
Our insight is that the most challenging verification task in datapath synthesis is the verification of the multipliers due to complex compressor trees.
1099+
We therefore formally verify this stage of datapath synthesis, and leave the remaining proof obligations to an SMT-solver, which discharges them easily.
1100+
At 16-bits, our approach can verify 16 of 22 designs within the timeout
1101+
while only being 1.21 times larger and 1.12 times slower than unverified method,
1102+
whereas the SMT-based baseline can only verify 5 of the designs.
1103+
We make all our contributions open-source on (this link).\osman{should we put a link here? if so how to appropriately anonymize it?}
1104+
1105+
Future work will address the missing optimizations on bit heaps and datapath synthesis.
1106+
Namely Booth encoding, sign-extension related optimizations opportunities, and extend our formalization
1107+
with timing-aware compression, in which the arrival of each bit is accounted for during the compression.
1108+
10901109

10911110
%% Acknowledgments. IEEEtran has no \begin{acks} or \grantsponsor/\grantnum;
10921111
%% IEEE uses an unnumbered section. Suppressed for anonymous review.

0 commit comments

Comments
 (0)