From 69df81756ca692971e9b2b75ffe25859fe215207 Mon Sep 17 00:00:00 2001
From: Iztok Jeras <iztok.jeras@gmail.com>
Date: Mon, 22 Jun 2026 01:08:39 +0200
Subject: [PATCH] dlatchlibmap: making a copy of test files dfflibmap* to
 dlatchlibmap*

---
 tests/techmap/dlatchlibmap-sim.v              |  31 ++
 tests/techmap/dlatchlibmap.lib                |  79 ++++++
 tests/techmap/dlatchlibmap.ys                 |  99 +++++++
 .../techmap/dlatchlibmap_dlatch_not_data.lib  |  24 ++
 tests/techmap/dlatchlibmap_dlatchn.lib        |  47 +++
 .../dlatchlibmap_dlatchsr_mixedpol.lib        |  35 +++
 .../dlatchlibmap_dlatchsr_not_data.lib        |  28 ++
 .../dlatchlibmap_dlatchsr_not_data_l.lib      |  33 +++
 tests/techmap/dlatchlibmap_dlatchsr_r.lib     |  33 +++
 tests/techmap/dlatchlibmap_dlatchsr_s.lib     |  33 +++
 tests/techmap/dlatchlibmap_dlatchsr_x.lib     |  33 +++
 tests/techmap/dlatchlibmap_formal.ys          | 268 ++++++++++++++++++
 tests/techmap/dlatchlibmap_proc_formal.ys     | 100 +++++++
 13 files changed, 843 insertions(+)
 create mode 100644 tests/techmap/dlatchlibmap-sim.v
 create mode 100644 tests/techmap/dlatchlibmap.lib
 create mode 100644 tests/techmap/dlatchlibmap.ys
 create mode 100644 tests/techmap/dlatchlibmap_dlatch_not_data.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchn.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_r.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_s.lib
 create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_x.lib
 create mode 100644 tests/techmap/dlatchlibmap_formal.ys
 create mode 100644 tests/techmap/dlatchlibmap_proc_formal.ys

diff --git a/tests/techmap/dlatchlibmap-sim.v b/tests/techmap/dlatchlibmap-sim.v
new file mode 100644
index 000000000..42006a211
--- /dev/null
+++ b/tests/techmap/dlatchlibmap-sim.v
@@ -0,0 +1,31 @@
+module dffn(input CLK, D, output reg Q, output QN);
+
+always @(negedge CLK)
+	Q <= D;
+
+assign QN = ~Q;
+
+endmodule
+
+module dffsr(input CLK, D, CLEAR, PRESET, output reg Q, output QN);
+
+always @(posedge CLK, posedge CLEAR, posedge PRESET)
+	if (CLEAR)
+		Q <= 0;
+	else if (PRESET)
+		Q <= 1;
+	else
+		Q <= D;
+
+assign QN = ~Q;
+
+endmodule
+
+module dffe(input CLK, EN, D, output reg Q, output QN);
+
+always @(negedge CLK)
+	if (EN) Q <= D;
+
+assign QN = ~Q;
+
+endmodule
diff --git a/tests/techmap/dlatchlibmap.lib b/tests/techmap/dlatchlibmap.lib
new file mode 100644
index 000000000..54a44a296
--- /dev/null
+++ b/tests/techmap/dlatchlibmap.lib
@@ -0,0 +1,79 @@
+library(test) {
+  /* D-type flip-flop with asynchronous reset and preset */
+  cell (dffn) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "!CLK";
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+  cell (dffe) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "(D EN) | (IQ !EN)";
+      clocked_on : "!CLK";
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(EN) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys
new file mode 100644
index 000000000..87ecc8bc7
--- /dev/null
+++ b/tests/techmap/dlatchlibmap.ys
@@ -0,0 +1,99 @@
+read_verilog -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(R), .S(S), .Q(Q[4]));
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+simplemap
+
+design -save orig
+read_liberty -lib dfflibmap.lib
+
+equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib
+equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib
+
+dfflibmap -prepare -liberty dfflibmap.lib
+equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
+
+design -load orig
+dfflibmap -liberty dfflibmap.lib
+clean
+
+select -assert-count 5 t:$_NOT_
+select -assert-count 1 t:dffn
+select -assert-count 4 t:dffsr
+select -assert-count 1 t:dffe
+select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
+
+design -load orig
+dfflibmap -prepare -liberty dfflibmap.lib
+
+select -assert-count 11 t:$_NOT_
+select -assert-count 1 t:$_DFF_N_
+select -assert-count 4 t:$_DFFSR_PPP_
+select -assert-count 1 t:$_DFFE_NP_
+select -assert-none t:$_DFF_N_ t:$_DFFSR_PPP_ t:$_DFFE_NP_ t:$_NOT_ %% %n t:* %i
+
+design -load orig
+dfflibmap -map-only -liberty dfflibmap.lib
+
+select -assert-count 6 t:$_NOT_
+select -assert-count 0 t:dffn
+select -assert-count 1 t:dffsr
+
+design -load orig
+dfflibmap -prepare -liberty dfflibmap.lib
+dfflibmap -map-only -liberty dfflibmap.lib
+clean
+
+select -assert-count 5 t:$_NOT_
+select -assert-count 1 t:dffn
+select -assert-count 4 t:dffsr
+select -assert-count 1 t:dffe
+select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
+
+design -load orig
+dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
+dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib
+clean
+
+select -assert-count 5 t:$_NOT_
+select -assert-count 1 t:dffn
+select -assert-count 1 t:dffe
+select -assert-count 4 t:dffsr
+select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i
+
+design -load orig
+dfflibmap -liberty dfflibmap.lib -dont_use *ffn
+clean
+
+select -assert-count 0 t:dffn
+select -assert-count 5 t:dffsr
+select -assert-count 1 t:dffe
+
+design -load orig
+dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
+clean
+# We have one more _NOT_ than with the regular dffsr
+select -assert-count 6 t:$_NOT_
+select -assert-count 1 t:dffn
+select -assert-count 4 t:dffsr_mixedpol
+select -assert-count 1 t:dffe
+# The additional NOT is on ff2.
+# Originally, ff2.R is an active high "set".
+# dffsr_mixedpol has functionally swapped labels due to the next_state inversion,
+# so we use its CLEAR port for the "set",
+# but we have to invert it because the CLEAR pin is active low.
+# ff2.CLEAR = !R
+select -assert-count 1 c:ff2 %x:+[CLEAR] %ci t:$_NOT_ %i
diff --git a/tests/techmap/dlatchlibmap_dlatch_not_data.lib b/tests/techmap/dlatchlibmap_dlatch_not_data.lib
new file mode 100644
index 000000000..0a0b011de
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatch_not_data.lib
@@ -0,0 +1,24 @@
+library (test_not_next) {
+  cell (dff_not_next) {
+    area: 1.0;
+    pin (QN) {
+      direction : output;
+      function : "STATE";
+    }
+    pin (CLK) {
+      direction : input;
+      clock : true;
+    }
+    pin (D) {
+      direction : input;
+    }
+    pin (RN) {
+      direction : input;
+    }
+    ff (STATE, STATEN) {
+      clocked_on: "CLK";
+      next_state: "!D";
+      preset : "!RN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchn.lib b/tests/techmap/dlatchlibmap_dlatchn.lib
new file mode 100644
index 000000000..832edee67
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchn.lib
@@ -0,0 +1,47 @@
+library(test) {
+  cell (dffn) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "!CLK";
+    } 
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    } 
+  }
+  cell (dffe) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "(D&EN) | (IQ&!EN)";
+      clocked_on : "!CLK";
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(EN) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib
new file mode 100644
index 000000000..8c6a2f509
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib
@@ -0,0 +1,35 @@
+library(test) {
+  cell (dffsr_mixedpol) {
+    area : 6;
+    ff("IQ", "IQN") {
+      // look here
+      next_state : "!D";
+      clocked_on : "CLK";
+      // look here
+      clear      : "!CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib b/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
new file mode 100644
index 000000000..579dedb10
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
@@ -0,0 +1,28 @@
+library (test_not_next) {
+  cell (dffsr_not_next) {
+    area : 1.0;
+    pin (Q) {
+      direction : output;
+      function : "STATE";
+    }
+    pin (CLK) {
+      clock : true;
+      direction : input;
+    }
+    pin (D) {
+      direction : input;
+    }
+    pin (RN) {
+      direction : input;
+    }
+    pin (SN) {
+      direction : input;
+    }
+    ff (STATE,STATEN) {
+      clear : "!SN";
+      clocked_on : "CLK";
+      next_state : "!D";
+      preset : "!RN";
+    }
+  }
+}
\ No newline at end of file
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib b/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
new file mode 100644
index 000000000..74004bea1
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffr_not_next) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "!D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_r.lib b/tests/techmap/dlatchlibmap_dlatchsr_r.lib
new file mode 100644
index 000000000..f36e200a0
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_r.lib
@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : L;
+      clear_preset_var2 : H;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_s.lib b/tests/techmap/dlatchlibmap_dlatchsr_s.lib
new file mode 100644
index 000000000..cf930f3c7
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_s.lib
@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : H;
+      clear_preset_var2 : L;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_x.lib b/tests/techmap/dlatchlibmap_dlatchsr_x.lib
new file mode 100644
index 000000000..91d702412
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_dlatchsr_x.lib
@@ -0,0 +1,33 @@
+library(test) {
+  cell (dffsr) {
+    area : 6;
+    ff("IQ", "IQN") {
+      next_state : "D";
+      clocked_on : "CLK";
+      clear      : "CLEAR";
+      preset     : "PRESET";
+      clear_preset_var1 : X;
+      clear_preset_var2 : X;
+    }
+    pin(D) {
+      direction : input;
+    }
+    pin(CLK) {
+      direction : input;
+    }
+    pin(CLEAR) {
+      direction : input;
+    }
+    pin(PRESET) {
+      direction : input;
+    }
+    pin(Q) {
+      direction: output;
+      function : "IQ";
+    }
+    pin(QN) {
+      direction: output;
+      function : "IQN";
+    }
+  }
+}
diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys
new file mode 100644
index 000000000..e5e61cd62
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_formal.ys
@@ -0,0 +1,268 @@
+##################################################################
+
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+assume property (~R || ~S);
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_s.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_s.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+assume property (~R || ~S);
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_r.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_r.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+// no assume when mapping to X
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_x.lib
+opt
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_x.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+// Formal checking of directly instantiated DFFSR doesn't work at the moment
+// likely due to an equiv_induct -set-assumes assume bug #5196
+
+// no assume when mapping to unset clear_preset_var
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dffsr_not_next.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [11:0] Q);
+
+$_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0]));
+$_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1]));
+$_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2]));
+
+assume property (~R || ~S);
+$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4]));
+
+$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5]));
+
+assign Q[11:6] = ~Q[5:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_not_next_l.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+hierarchy -top miter
+
+# Prove that this is equivalent with the assumption
+sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter
+# Prove that this is NOT equivalent WITHOUT the assumption
+sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter
+
+##################################################################
+
+design -reset
+read_verilog <<EOT
+
+module top(input C, D, E, S, R, output Q);
+// DFFSR with priority R over S
+always @(posedge C, posedge R, posedge S)
+    if (R == 1)
+        Q <= 0;
+    else if (S == 1)
+        Q <= 1;
+    else
+        Q <= D;
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dffsr_not_next.lib
+
+copy top top_unmapped
+simplemap top
+dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+equiv_make top top_unmapped equiv
+equiv_induct -set-assumes equiv
+equiv_status -assert equiv
+
+##################################################################
+
+design -reset
+read_verilog <<EOT
+
+module top(input C, D, R, output Q);
+  // DFF with preset
+  always @(posedge C or negedge R) begin
+    if (!R) Q <= 1'b1;
+    else Q <= D;
+  end
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffn_dffe.lib
+read_liberty dfflibmap_dff_not_next.lib
+
+copy top top_unmapped
+simplemap top
+dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+equiv_make top top_unmapped equiv
+equiv_induct -set-assumes equiv
+equiv_status -assert equiv
\ No newline at end of file
diff --git a/tests/techmap/dlatchlibmap_proc_formal.ys b/tests/techmap/dlatchlibmap_proc_formal.ys
new file mode 100644
index 000000000..88cb97cdb
--- /dev/null
+++ b/tests/techmap/dlatchlibmap_proc_formal.ys
@@ -0,0 +1,100 @@
+##################################################################
+
+read_verilog -sv -icells <<EOT
+
+module top(input C, D, E, S, R, output [7:0] Q);
+
+	always @( posedge C, posedge S, posedge R)
+		if (R)
+			Q[0] <= 0;
+		else if (S)
+			Q[0] <= 1;
+		else
+			Q[0] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (S)
+			Q[1] <= 1;
+		else if (R)
+			Q[1] <= 0;
+		else
+			Q[1] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (R)
+			Q[2] <= 0;
+		else if (S)
+			Q[2] <= 1;
+		else if (E)
+			Q[2] <= D;
+
+	always @( posedge C, posedge S, posedge R)
+		if (S)
+			Q[3] <= 1;
+		else if (R)
+			Q[3] <= 0;
+		else if (E)
+			Q[3] <= D;
+
+assign Q[7:4] = ~Q[3:0];
+
+endmodule
+
+EOT
+
+proc
+opt
+read_liberty dfflibmap_dffsr_s.lib
+
+copy top top_unmapped
+dfflibmap -liberty dfflibmap_dffsr_s.lib top
+
+clk2fflogic
+flatten
+opt_clean -purge
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_r.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter
+
+##################################################################
+
+delete top miter
+
+copy top_unmapped top
+dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
+
+clk2fflogic
+flatten
+miter -equiv -make_assert -flatten top_unmapped top miter
+
+# Prove that this is equivalent
+sat -verify -prove-asserts -set-init-undef -show-public -seq 3 miter