Add new tests for Efinix architecture.

Problems/questions:
	- fsm.ys. equiv_opt -assert failed because of unproven cells;
	- latches.ys,tribuf.ys - internal cells present;
	- memory.ys - sat called with -verify and proof did fail.

1 files changed, 37 insertions, 0 deletions

diff --git a/tests/efinix/dffs.v b/tests/efinix/dffs.v
new file mode 100644
index 000000000..d97840c43
--- /dev/null
+++ b/tests/efinix/dffs.v
@@ -0,0 +1,37 @@
+module dff
+    ( input d, clk, output reg q );
+	always @( posedge clk )
+            q <= d;
+endmodule
+
+module dffe
+    ( input d, clk, en, output reg q );
+    initial begin
+      q = 0;
+    end
+	always @( posedge clk )
+		if ( en )
+			q <= d;
+endmodule
+
+module top (
+input clk,
+input en,
+input a,
+output b,b1,
+);
+
+dff u_dff (
+        .clk (clk ),
+        .d (a ),
+        .q (b )
+    );
+
+dffe u_ndffe (
+        .clk (clk ),
+        .en (en),
+        .d (a ),
+        .q (b1 )
+    );
+
+endmodule