diff options
| -rw-r--r-- | libs/ezsat/Makefile | 4 | ||||
| -rw-r--r-- | libs/ezsat/ezsat.h | 2 | ||||
| -rw-r--r-- | libs/ezsat/puzzle3d.cc | 4 | ||||
| -rw-r--r-- | libs/ezsat/testbench.cc | 120 | ||||
| -rw-r--r-- | manual/PRESENTATION_ExAdv.tex | 71 |
5 files changed, 87 insertions, 114 deletions
diff --git a/libs/ezsat/Makefile b/libs/ezsat/Makefile index da2355a9b..e831cc6f0 100644 --- a/libs/ezsat/Makefile +++ b/libs/ezsat/Makefile @@ -3,7 +3,7 @@ CC = clang CXX = clang CXXFLAGS = -MD -Wall -Wextra -ggdb CXXFLAGS += -std=c++11 -O0 -LDLIBS = -lminisat -lstdc++ +LDLIBS = -lminisat -lm -lstdc++ all: demo_vec demo_bit demo_cmp testbench puzzle3d @@ -20,7 +20,7 @@ test: all ./demo_cmp clean: - rm -f demo_bit demo_vec testbench puzzle3d *.o *.d + rm -f demo_bit demo_vec demo_cmp testbench puzzle3d *.o *.d .PHONY: all test clean diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index b0b731d0a..852405566 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -168,7 +168,7 @@ public: int get(ezSAT *that) { if (name.empty()) return id; - return that->literal(name); + return that->frozen_literal(name); } }; diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc index 56d293260..aee0044b4 100644 --- a/libs/ezsat/puzzle3d.cc +++ b/libs/ezsat/puzzle3d.cc @@ -260,8 +260,10 @@ int main() std::vector<int> modelExpressions; std::vector<bool> modelValues; - for (auto &it : blockinfo) + for (auto &it : blockinfo) { + ez.freeze(it.first); modelExpressions.push_back(it.first); + } int solution_counter = 0; while (1) diff --git a/libs/ezsat/testbench.cc b/libs/ezsat/testbench.cc index 8283686e3..8332ad919 100644 --- a/libs/ezsat/testbench.cc +++ b/libs/ezsat/testbench.cc @@ -63,7 +63,7 @@ void test_simple() { printf("==== %s ====\n\n", __PRETTY_FUNCTION__); - ezSAT sat; + ezMiniSAT sat; sat.assume(sat.OR("A", "B")); sat.assume(sat.NOT(sat.AND("A", "B"))); test(sat); @@ -71,89 +71,6 @@ void test_simple() // ------------------------------------------------------------------------------------------------------------ -void test_basic_operators(ezSAT &sat, xorshift128 &rng, int iter, bool buildTrees, bool buildClusters, std::vector<bool> &log) -{ - int vars[6] = { - sat.VAR("A"), sat.VAR("B"), sat.VAR("C"), - sat.NOT("A"), sat.NOT("B"), sat.NOT("C") - }; - for (int i = 0; i < iter; i++) { - int assumption = 0, op = rng() % 6, to = rng() % 6; - int a = vars[rng() % 6], b = vars[rng() % 6], c = vars[rng() % 6]; - // printf("--> %d %d:%s %d:%s %d:%s\n", op, a, sat.to_string(a).c_str(), b, sat.to_string(b).c_str(), c, sat.to_string(c).c_str()); - switch (op) - { - case 0: - assumption = sat.NOT(a); - break; - case 1: - assumption = sat.AND(a, b); - break; - case 2: - assumption = sat.OR(a, b); - break; - case 3: - assumption = sat.XOR(a, b); - break; - case 4: - assumption = sat.IFF(a, b); - break; - case 5: - assumption = sat.ITE(a, b, c); - break; - } - // printf(" --> %d:%s\n", to, sat.to_string(assumption).c_str()); - if (buildTrees) - vars[to] = assumption; - if (!buildClusters) - sat.clear(); - sat.assume(assumption); - if (sat.numCnfVariables() < 15) { - printf("%d:\n", int(log.size())); - log.push_back(test(sat)); - } else { - // printf("** skipping large problem **\n"); - } - } -} - -void test_basic_operators(ezSAT &sat, std::vector<bool> &log) -{ - printf("-- %s --\n\n", __PRETTY_FUNCTION__); - - xorshift128 rng; - test_basic_operators(sat, rng, 1000, false, false, log); - for (int i = 0; i < 100; i++) - test_basic_operators(sat, rng, 10, true, false, log); - for (int i = 0; i < 100; i++) - test_basic_operators(sat, rng, 10, false, true, log); -} - -void test_basic_operators() -{ - printf("==== %s ====\n\n", __PRETTY_FUNCTION__); - - ezSAT sat; - ezMiniSAT miniSat; - std::vector<bool> logSat, logMiniSat; - - test_basic_operators(sat, logSat); - test_basic_operators(miniSat, logMiniSat); - - if (logSat != logMiniSat) { - printf("Differences between logSat and logMiniSat:"); - for (int i = 0; i < int(std::max(logSat.size(), logMiniSat.size())); i++) - if (i >= int(logSat.size()) || i >= int(logMiniSat.size()) || logSat[i] != logMiniSat[i]) - printf(" %d", i); - printf("\n"); - abort(); - } else { - printf("Completed %d tests with identical results with ezSAT and ezMiniSAT.\n\n", int(logSat.size())); - } -} - -// ------------------------------------------------------------------------------------------------------------ - void test_xorshift32_try(ezSAT &sat, uint32_t input_pattern) { uint32_t output_pattern = input_pattern; @@ -238,7 +155,7 @@ void check(const char *expr1_str, bool expr1, const char *expr2_str, bool expr2) void test_signed(int8_t a, int8_t b, int8_t c) { - ezSAT sat; + ezMiniSAT sat; std::vector<int> av = sat.vec_const_signed(a, 8); std::vector<int> bv = sat.vec_const_signed(b, 8); @@ -257,7 +174,7 @@ void test_signed(int8_t a, int8_t b, int8_t c) void test_unsigned(uint8_t a, uint8_t b, uint8_t c) { - ezSAT sat; + ezMiniSAT sat; if (b < c) b ^= c, c ^= b, b ^= c; @@ -279,7 +196,7 @@ void test_unsigned(uint8_t a, uint8_t b, uint8_t c) void test_count(uint32_t x) { - ezSAT sat; + ezMiniSAT sat; int count = 0; for (int i = 0; i < 32; i++) @@ -333,10 +250,10 @@ void test_onehot() printf("==== %s ====\n\n", __PRETTY_FUNCTION__); ezMiniSAT ez; - int a = ez.literal("a"); - int b = ez.literal("b"); - int c = ez.literal("c"); - int d = ez.literal("d"); + int a = ez.frozen_literal("a"); + int b = ez.frozen_literal("b"); + int c = ez.frozen_literal("c"); + int d = ez.frozen_literal("d"); std::vector<int> abcd; abcd.push_back(a); @@ -387,10 +304,10 @@ void test_manyhot() printf("==== %s ====\n\n", __PRETTY_FUNCTION__); ezMiniSAT ez; - int a = ez.literal("a"); - int b = ez.literal("b"); - int c = ez.literal("c"); - int d = ez.literal("d"); + int a = ez.frozen_literal("a"); + int b = ez.frozen_literal("b"); + int c = ez.frozen_literal("c"); + int d = ez.frozen_literal("d"); std::vector<int> abcd; abcd.push_back(a); @@ -441,13 +358,13 @@ void test_ordered() printf("==== %s ====\n\n", __PRETTY_FUNCTION__); ezMiniSAT ez; - int a = ez.literal("a"); - int b = ez.literal("b"); - int c = ez.literal("c"); + int a = ez.frozen_literal("a"); + int b = ez.frozen_literal("b"); + int c = ez.frozen_literal("c"); - int x = ez.literal("x"); - int y = ez.literal("y"); - int z = ez.literal("z"); + int x = ez.frozen_literal("x"); + int y = ez.frozen_literal("y"); + int z = ez.frozen_literal("z"); std::vector<int> abc; abc.push_back(a); @@ -507,7 +424,6 @@ void test_ordered() int main() { test_simple(); - test_basic_operators(); test_xorshift32(); test_arith(); test_onehot(); diff --git a/manual/PRESENTATION_ExAdv.tex b/manual/PRESENTATION_ExAdv.tex index bf9b350ff..7aa014242 100644 --- a/manual/PRESENTATION_ExAdv.tex +++ b/manual/PRESENTATION_ExAdv.tex @@ -789,11 +789,11 @@ extract -constports -ignore_parameters \ Unwrap in {\tt test2}: \hfil\begin{tikzpicture} +\node at (0,0) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf}}; +\node at (0,-4) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}}; \node at (1,-1.7) {\begin{lstlisting}[linewidth=5.5cm, frame=single, basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=ys] techmap -map macc_xilinx_unwrap_map.v ;; \end{lstlisting}}; -\node at (0,0) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2d.pdf}}; -\node at (0,-4) {\includegraphics[width=11cm,trim=1.5cm 1.5cm 1.5cm 1.5cm]{PRESENTATION_ExAdv/macc_xilinx_test2e.pdf}}; \draw[-latex] (4,-0.7) .. controls (5,-1.7) .. (4,-2.7); \end{tikzpicture} \end{frame} @@ -808,10 +808,67 @@ techmap -map macc_xilinx_unwrap_map.v ;; \subsectionpagesuffix \end{frame} -\subsubsection{TBD} +\subsubsection{Changing the design from Yosys} \begin{frame}{\subsubsecname} -TBD +Yosys commands can be used to change the design in memory. Examples of this are: + +\begin{itemize} +\item {\bf Changes in design hierarchy} \\ +Commands such as {\tt flatten} and {\tt submod} can be used to change the design hierarchy, i.e. +flatten the hierarchy or moving parts of a module to a submodule. This has applications in synthesis +scripts as well as in reverse engineering and analysis. + +\item {\bf Behavioral changes} \\ +Commands such as {\tt techmap} can be used to make behavioral changes to the design, for example +changing asynchonous resets to synchronous resets. This has applications in design space exploration +(evaluation of various architectures for one circuit). +\end{itemize} +\end{frame} + +\subsubsection{Example: Async reset to sync reset} + +\begin{frame}[t, fragile]{\subsubsecname} +The following techmap map file replaces all positive-edge async reset flip-flops with +positive-edge sync reset flip-flops. The code is taken from the example Yosys script +for ASIC synthesis of the Amber ARMv2 CPU. + +\begin{columns} +\column[t]{6cm} +\vbox to 0cm{ +\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=Verilog] +(* techmap_celltype = "$adff" *) +module adff2dff (CLK, ARST, D, Q); + + parameter WIDTH = 1; + parameter CLK_POLARITY = 1; + parameter ARST_POLARITY = 1; + parameter ARST_VALUE = 0; + + input CLK, ARST; + input [WIDTH-1:0] D; + output reg [WIDTH-1:0] Q; + + wire [1023:0] _TECHMAP_DO_ = "proc"; + + wire _TECHMAP_FAIL_ = !CLK_POLARITY || !ARST_POLARITY; +\end{lstlisting} +\vss} +\column[t]{4cm} +\begin{lstlisting}[basicstyle=\ttfamily\fontsize{8pt}{10pt}\selectfont, language=Verilog] +// ..continued.. + + + always @(posedge CLK) + if (ARST) + Q <= ARST_VALUE; + else + <= D; + +endmodule +\end{lstlisting} +\end{columns} + \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -820,10 +877,8 @@ TBD \begin{frame}{\subsecname} \begin{itemize} -\item TBD -\item TBD -\item TBD -\item TBD +\item A lot can be achived in Yosys just with the standard set of commands. +\item The commands {\tt techmap} and {\tt extract} can be used to prototype many complex synthesis tasks. \end{itemize} \bigskip |