From f111bbdf4006be9f108374c8591c682f02033a6f Mon Sep 17 00:00:00 2001
From: gatecat <gatecat@ds0.me>
Date: Thu, 10 Nov 2022 09:53:07 +0100
Subject: fabulous: improvements to the pass

Signed-off-by: gatecat <gatecat@ds0.me>
---
 tests/arch/fabulous/.gitignore     |  4 ++++
 tests/arch/fabulous/complexflop.ys | 37 +++++++++++++++++++++++++++++++++++++
 tests/arch/fabulous/counter.ys     | 26 ++++++++++++++++++++++++++
 tests/arch/fabulous/fsm.ys         | 19 +++++++++++++++++++
 tests/arch/fabulous/logic.ys       | 10 ++++++++++
 tests/arch/fabulous/regfile.ys     | 33 +++++++++++++++++++++++++++++++++
 tests/arch/fabulous/tribuf.ys      | 12 ++++++++++++
 7 files changed, 141 insertions(+)
 create mode 100644 tests/arch/fabulous/.gitignore
 create mode 100644 tests/arch/fabulous/complexflop.ys
 create mode 100644 tests/arch/fabulous/counter.ys
 create mode 100644 tests/arch/fabulous/fsm.ys
 create mode 100644 tests/arch/fabulous/logic.ys
 create mode 100644 tests/arch/fabulous/regfile.ys
 create mode 100644 tests/arch/fabulous/tribuf.ys

(limited to 'tests')

diff --git a/tests/arch/fabulous/.gitignore b/tests/arch/fabulous/.gitignore
new file mode 100644
index 000000000..9a71dca69
--- /dev/null
+++ b/tests/arch/fabulous/.gitignore
@@ -0,0 +1,4 @@
+*.log
+/run-test.mk
++*_synth.v
++*_testbench
diff --git a/tests/arch/fabulous/complexflop.ys b/tests/arch/fabulous/complexflop.ys
new file mode 100644
index 000000000..13f4522b9
--- /dev/null
+++ b/tests/arch/fabulous/complexflop.ys
@@ -0,0 +1,37 @@
+read_verilog <<EOT
+module top ( input d0, d1, d2, d3, ce, sr, clk, output reg q0, q1, q2, q3 );
+    always @(posedge clk)
+      begin
+        if (sr) begin
+            q0 <= 1'b0;
+            q1 <= 1'b1;
+        end else begin
+            q0 <= d0;
+            q1 <= d1;
+        end
+        if (ce) begin
+          if (sr) begin
+              q2 <= 1'b0;
+              q3 <= 1'b1;
+          end else begin
+              q2 <= d2;
+              q3 <= d3;
+          end
+        end
+      end
+endmodule
+EOT
+
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous -complex-dff # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:LUTFF_SR
+select -assert-count 1 t:LUTFF_SS
+select -assert-count 1 t:LUTFF_ESR
+select -assert-count 1 t:LUTFF_ESS
+
+select -assert-none t:LUTFF_SR t:LUTFF_SS t:LUTFF_ESR t:LUTFF_ESS %% t:* %D
diff --git a/tests/arch/fabulous/counter.ys b/tests/arch/fabulous/counter.ys
new file mode 100644
index 000000000..d79b378a6
--- /dev/null
+++ b/tests/arch/fabulous/counter.ys
@@ -0,0 +1,26 @@
+read_verilog <<EOT
+module top ( out, clk, reset );
+    output [7:0] out;
+    input clk, reset;
+    reg [7:0] out;
+
+    always @(posedge clk)
+      if (reset)
+          out <= 8'b0;
+      else
+          out <= out + 1;
+endmodule
+EOT
+
+hierarchy -top top
+proc
+flatten
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+
+select -assert-count 1 t:LUT2
+select -assert-count 7 t:LUT3
+select -assert-count 4 t:LUT4
+select -assert-count 8 t:LUTFF
+select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D
diff --git a/tests/arch/fabulous/fsm.ys b/tests/arch/fabulous/fsm.ys
new file mode 100644
index 000000000..9c3831682
--- /dev/null
+++ b/tests/arch/fabulous/fsm.ys
@@ -0,0 +1,19 @@
+read_verilog ../common/fsm.v
+hierarchy -top fsm
+proc
+flatten
+
+equiv_opt -run :prove -map +/fabulous/prims.v synth_fabulous
+async2sync
+miter -equiv -make_assert -flatten gold gate miter
+stat
+sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter
+
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd fsm # Constrain all select calls below inside the top module
+
+select -assert-count 6 t:LUTFF
+select -assert-max 4 t:LUT2
+select -assert-max 2 t:LUT3
+select -assert-max 9 t:LUT4
+select -assert-none t:LUT2 t:LUT3 t:LUT4 t:LUTFF %% t:* %D
diff --git a/tests/arch/fabulous/logic.ys b/tests/arch/fabulous/logic.ys
new file mode 100644
index 000000000..730d9ab54
--- /dev/null
+++ b/tests/arch/fabulous/logic.ys
@@ -0,0 +1,10 @@
+read_verilog ../common/logic.v
+hierarchy -top top
+proc
+equiv_opt -assert -map +/fabulous/prims.v synth_fabulous # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd top # Constrain all select calls below inside the top module
+select -assert-max 1 t:LUT1
+select -assert-max 6 t:LUT2
+select -assert-max 2 t:LUT4
+select -assert-none t:LUT1 t:LUT2 t:LUT4 %% t:* %D
diff --git a/tests/arch/fabulous/regfile.ys b/tests/arch/fabulous/regfile.ys
new file mode 100644
index 000000000..8d1eedef0
--- /dev/null
+++ b/tests/arch/fabulous/regfile.ys
@@ -0,0 +1,33 @@
+read_verilog <<EOT
+module sync_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
+	reg [3:0] mem[0:31];
+	always @(posedge clk)
+		if (we) mem[aw] <= wd;
+	always @(posedge clk)
+		ra <= mem[aa];
+	always @(posedge clk)
+		rb <= mem[ab];
+endmodule
+EOT
+
+synth_fabulous -top sync_sync
+cd sync_sync
+select -assert-count 1 t:RegFile_32x4
+
+design -reset
+
+read_verilog <<EOT
+module async_sync(input clk, we, input [4:0] aw, aa, ab, input [3:0] wd, output reg [3:0] ra, rb);
+	reg [3:0] mem[0:31];
+	always @(posedge clk)
+		if (we) mem[aw] <= wd;
+	always @(posedge clk)
+		ra <= mem[aa];
+	always @(*)
+		rb <= mem[ab];
+endmodule
+EOT
+
+synth_fabulous -top async_sync
+cd async_sync
+select -assert-count 1 t:RegFile_32x4
diff --git a/tests/arch/fabulous/tribuf.ys b/tests/arch/fabulous/tribuf.ys
new file mode 100644
index 000000000..0dcf1cbab
--- /dev/null
+++ b/tests/arch/fabulous/tribuf.ys
@@ -0,0 +1,12 @@
+read_verilog ../common/tribuf.v
+hierarchy -top tristate
+proc
+tribuf
+flatten
+synth
+equiv_opt -assert -map +/fabulous/prims.v -map +/simcells.v synth_fabulous -iopad # equivalency check
+design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
+cd tristate # Constrain all select calls below inside the top module
+select -assert-count 3 t:IO_1_bidirectional_frame_config_pass
+select -assert-max 1 t:LUT1
+select -assert-none t:IO_1_bidirectional_frame_config_pass t:LUT1 %% t:* %D
-- 
cgit v1.2.3