Merge branch 'master' of github.com:cliffordwolf/yosys

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
 

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);
 		}
 	};
 

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)

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 a = ez.frozen_literal("a");
-	int b = ez.literal("b");
+	int b = ez.frozen_literal("b");
-	int c = ez.literal("c");
+	int c = ez.frozen_literal("c");
-	int d = ez.literal("d");
+	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 a = ez.frozen_literal("a");
-	int b = ez.literal("b");
+	int b = ez.frozen_literal("b");
-	int c = ez.literal("c");
+	int c = ez.frozen_literal("c");
-	int d = ez.literal("d");
+	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 a = ez.frozen_literal("a");
-	int b = ez.literal("b");
+	int b = ez.frozen_literal("b");
-	int c = ez.literal("c");
+	int c = ez.frozen_literal("c");
 
-	int x = ez.literal("x");
+	int x = ez.frozen_literal("x");
-	int y = ez.literal("y");
+	int y = ez.frozen_literal("y");
-	int z = ez.literal("z");
+	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();

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 A lot can be achived in Yosys just with the standard set of commands.
-\item TBD
+\item The commands {\tt techmap} and {\tt extract} can be used to prototype many complex synthesis tasks.
-\item TBD
-\item TBD
 \end{itemize}
 
 \bigskip