From 0df2169f8189b7c63a970311f1f43021529c0950 Mon Sep 17 00:00:00 2001
From: Iztok Jeras <iztok.jeras@gmail.com>
Date: Mon, 22 Jun 2026 01:12:09 +0200
Subject: [PATCH] dlatchlibmap: modified copies of dfflibmap* test files for
 dlatchlibmap tests

---
 tests/techmap/dlatchlibmap-sim.v              |  28 +---
 tests/techmap/dlatchlibmap.lib                |  52 ++-----
 tests/techmap/dlatchlibmap.ys                 |  97 ++++++------
 .../techmap/dlatchlibmap_dlatch_not_data.lib  |  12 +-
 tests/techmap/dlatchlibmap_dlatchn.lib        |  35 +----
 .../dlatchlibmap_dlatchsr_mixedpol.lib        |  17 +-
 .../dlatchlibmap_dlatchsr_not_data.lib        |  12 +-
 .../dlatchlibmap_dlatchsr_not_data_l.lib      |  15 +-
 tests/techmap/dlatchlibmap_dlatchsr_r.lib     |  15 +-
 tests/techmap/dlatchlibmap_dlatchsr_s.lib     |  15 +-
 tests/techmap/dlatchlibmap_dlatchsr_x.lib     |  15 +-
 tests/techmap/dlatchlibmap_formal.ys          | 146 ++++++++----------
 tests/techmap/dlatchlibmap_proc_formal.ys     |  52 ++-----
 13 files changed, 207 insertions(+), 304 deletions(-)

diff --git a/tests/techmap/dlatchlibmap-sim.v b/tests/techmap/dlatchlibmap-sim.v
index 42006a211..03a2e4817 100644
--- a/tests/techmap/dlatchlibmap-sim.v
+++ b/tests/techmap/dlatchlibmap-sim.v
@@ -1,30 +1,18 @@
-module dffn(input CLK, D, output reg Q, output QN);
+module dlatchn(input ENA, D, output reg Q, output QN);
 
-always @(negedge CLK)
-	Q <= D;
+always @*
+	if (~ENA)  Q <= D;
 
 assign QN = ~Q;
 
 endmodule
 
-module dffsr(input CLK, D, CLEAR, PRESET, output reg Q, output QN);
+module dlatchsr(input ENA, 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;
+always @*
+	if      (CLEAR)   Q <= 1'b0;
+	else if (PRESET)  Q <= 1'b1;
+	else if (ENA)     Q <= D;
 
 assign QN = ~Q;
 
diff --git a/tests/techmap/dlatchlibmap.lib b/tests/techmap/dlatchlibmap.lib
index 54a44a296..1e4f0bc99 100644
--- a/tests/techmap/dlatchlibmap.lib
+++ b/tests/techmap/dlatchlibmap.lib
@@ -1,16 +1,17 @@
 library(test) {
-  /* D-type flip-flop with asynchronous reset and preset */
-  cell (dffn) {
+  /* D-type latch with reset and preset */
+  cell (dlatchn) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "!CLK";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable  : "!ENA";
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(Q) {
       direction: output;
@@ -21,21 +22,22 @@ library(test) {
       function : "IQN";
     }
   }
-  cell (dffsr) {
+  cell (dlatchsr) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "CLK";
-      clear      : "CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable  : "ENA";
+      clear   : "CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : L;
       clear_preset_var2 : L;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
@@ -52,28 +54,4 @@ library(test) {
       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
index 87ecc8bc7..fa0ce65be 100644
--- a/tests/techmap/dlatchlibmap.ys
+++ b/tests/techmap/dlatchlibmap.ys
@@ -1,15 +1,14 @@
 read_verilog -icells <<EOT
 
-module top(input C, D, E, S, R, output [11:0] Q);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_     latch0 (.E(E), .D(D),               .Q(Q[0]));
+$_DLATCH_PP0_   latch1 (.E(E), .D(D), .R(R),        .Q(Q[1]));
+$_DLATCH_PP1_   latch2 (.E(E), .D(D), .R(R),        .Q(Q[2]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R(R), .S(S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(R), .S(S), .Q(Q[4]));
 
-assign Q[11:6] = ~Q[5:0];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -18,82 +17,76 @@ EOT
 simplemap
 
 design -save orig
-read_liberty -lib dfflibmap.lib
+read_liberty -lib dlatchlibmap.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
+equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib
+equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dlatchlibmap.lib
 
-dfflibmap -prepare -liberty dfflibmap.lib
-equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib
+dfflibmap -prepare -liberty dlatchlibmap.lib
+equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib
 
 design -load orig
-dfflibmap -liberty dfflibmap.lib
+dfflibmap -liberty dlatchlibmap.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
+select -assert-count 1 t:dlatchn
+select -assert-count 4 t:dlatchsr
+select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
 
 design -load orig
-dfflibmap -prepare -liberty dfflibmap.lib
+dfflibmap -prepare -liberty dlatchlibmap.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
+select -assert-count 1 t:$_DLATCH_N_
+select -assert-count 4 t:$_DLATCHSR_PPP_
+select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i
 
 design -load orig
-dfflibmap -map-only -liberty dfflibmap.lib
+dfflibmap -map-only -liberty dlatchlibmap.lib
 
 select -assert-count 6 t:$_NOT_
-select -assert-count 0 t:dffn
-select -assert-count 1 t:dffsr
+select -assert-count 0 t:dlatchn
+select -assert-count 1 t:dlatchsr
 
 design -load orig
-dfflibmap -prepare -liberty dfflibmap.lib
-dfflibmap -map-only -liberty dfflibmap.lib
+dfflibmap -prepare -liberty dlatchlibmap.lib
+dfflibmap -map-only -liberty dlatchlibmap.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
+select -assert-count 1 t:dlatchn
+select -assert-count 4 t:dlatchsr
+select -assert-none t:dlatchn t:dlatchsr 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
+dfflibmap -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
+dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_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
+select -assert-count 1 t:dlatchn
+select -assert-count 4 t:dlatchsr
+select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
 
 design -load orig
-dfflibmap -liberty dfflibmap.lib -dont_use *ffn
+dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn
 clean
 
-select -assert-count 0 t:dffn
-select -assert-count 5 t:dffsr
-select -assert-count 1 t:dffe
+select -assert-count 0 t:dlatchn
+select -assert-count 5 t:dlatchsr
 
 design -load orig
-dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr
+dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
 clean
-# We have one more _NOT_ than with the regular dffsr
+# We have one more _NOT_ than with the regular dlatchsr
 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,
+select -assert-count 1 t:dlatchn
+select -assert-count 4 t:dlatchsr_mixedpol
+# The additional NOT is on latch2.
+# Originally, latch2.R is an active high "set".
+# dlatchsr_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
+# latch2.CLEAR = !R
+select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i
diff --git a/tests/techmap/dlatchlibmap_dlatch_not_data.lib b/tests/techmap/dlatchlibmap_dlatch_not_data.lib
index 0a0b011de..48fd9b62b 100644
--- a/tests/techmap/dlatchlibmap_dlatch_not_data.lib
+++ b/tests/techmap/dlatchlibmap_dlatch_not_data.lib
@@ -1,11 +1,11 @@
-library (test_not_next) {
-  cell (dff_not_next) {
+library (test_not_data) {
+  cell (dff_not_data) {
     area: 1.0;
     pin (QN) {
       direction : output;
       function : "STATE";
     }
-    pin (CLK) {
+    pin (ENA) {
       direction : input;
       clock : true;
     }
@@ -15,9 +15,9 @@ library (test_not_next) {
     pin (RN) {
       direction : input;
     }
-    ff (STATE, STATEN) {
-      clocked_on: "CLK";
-      next_state: "!D";
+    latch (STATE, STATEN) {
+      enable: "ENA";
+      data_in: "!D";
       preset : "!RN";
     }
   }
diff --git a/tests/techmap/dlatchlibmap_dlatchn.lib b/tests/techmap/dlatchlibmap_dlatchn.lib
index 832edee67..85c14dd1b 100644
--- a/tests/techmap/dlatchlibmap_dlatchn.lib
+++ b/tests/techmap/dlatchlibmap_dlatchn.lib
@@ -1,15 +1,16 @@
 library(test) {
-  cell (dffn) {
+  cell (dlatchn) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "!CLK";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable : "!ENA";
     } 
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(Q) {
       direction: output;
@@ -20,28 +21,4 @@ library(test) {
       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
index 8c6a2f509..acb7987a5 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib
@@ -1,21 +1,20 @@
 library(test) {
-  cell (dffsr_mixedpol) {
+  cell (dlatchsr_mixedpol) {
     area : 6;
-    ff("IQ", "IQN") {
-      // look here
-      next_state : "!D";
-      clocked_on : "CLK";
-      // look here
-      clear      : "!CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "!D";
+      enable  : "ENA";
+      clear   : "!CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : L;
       clear_preset_var2 : L;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib b/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
index 579dedb10..181728d85 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_not_data.lib
@@ -1,11 +1,11 @@
-library (test_not_next) {
-  cell (dffsr_not_next) {
+library (test_not_data) {
+  cell (dlatchsr_not_data) {
     area : 1.0;
     pin (Q) {
       direction : output;
       function : "STATE";
     }
-    pin (CLK) {
+    pin (ENA) {
       clock : true;
       direction : input;
     }
@@ -18,10 +18,10 @@ library (test_not_next) {
     pin (SN) {
       direction : input;
     }
-    ff (STATE,STATEN) {
+    latch (STATE,STATEN) {
       clear : "!SN";
-      clocked_on : "CLK";
-      next_state : "!D";
+      enable : "ENA";
+      data_in : "!D";
       preset : "!RN";
     }
   }
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib b/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
index 74004bea1..6c3144c69 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib
@@ -1,19 +1,20 @@
 library(test) {
-  cell (dffr_not_next) {
+  cell (dlatchr_not_data) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "!D";
-      clocked_on : "CLK";
-      clear      : "CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "!D";
+      enable  : "ENA";
+      clear   : "CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : L;
       clear_preset_var2 : L;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_r.lib b/tests/techmap/dlatchlibmap_dlatchsr_r.lib
index f36e200a0..d1cb66efa 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_r.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_r.lib
@@ -1,19 +1,20 @@
 library(test) {
-  cell (dffsr) {
+  cell (dlatchsr) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "CLK";
-      clear      : "CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable  : "ENA";
+      clear   : "CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : L;
       clear_preset_var2 : H;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_s.lib b/tests/techmap/dlatchlibmap_dlatchsr_s.lib
index cf930f3c7..04175bc80 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_s.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_s.lib
@@ -1,19 +1,20 @@
 library(test) {
-  cell (dffsr) {
+  cell (dlatchsr) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "CLK";
-      clear      : "CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable  : "ENA";
+      clear   : "CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : H;
       clear_preset_var2 : L;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
diff --git a/tests/techmap/dlatchlibmap_dlatchsr_x.lib b/tests/techmap/dlatchlibmap_dlatchsr_x.lib
index 91d702412..9637c64e7 100644
--- a/tests/techmap/dlatchlibmap_dlatchsr_x.lib
+++ b/tests/techmap/dlatchlibmap_dlatchsr_x.lib
@@ -1,19 +1,20 @@
 library(test) {
-  cell (dffsr) {
+  cell (dlatchsr) {
     area : 6;
-    ff("IQ", "IQN") {
-      next_state : "D";
-      clocked_on : "CLK";
-      clear      : "CLEAR";
-      preset     : "PRESET";
+    latch("IQ", "IQN") {
+      data_in : "D";
+      enable  : "ENA";
+      clear   : "CLEAR";
+      preset  : "PRESET";
       clear_preset_var1 : X;
       clear_preset_var2 : X;
     }
     pin(D) {
       direction : input;
     }
-    pin(CLK) {
+    pin(ENA) {
       direction : input;
+      clock : true;
     }
     pin(CLEAR) {
       direction : input;
diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys
index e5e61cd62..8a6410156 100644
--- a/tests/techmap/dlatchlibmap_formal.ys
+++ b/tests/techmap/dlatchlibmap_formal.ys
@@ -2,19 +2,17 @@
 
 read_verilog -sv -icells <<EOT
 
-module top(input C, D, E, S, R, output [11:0] Q);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_   latch0 (.E(E), .D(D),        .Q(Q[0]));
+$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
+$_DLATCH_PP1_ latch2 (.E(E), .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]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .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];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -22,10 +20,10 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr_s.lib
+read_liberty dlatchlibmap_dlatchsr_s.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr_s.lib top
+dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
 
 clk2fflogic
 flatten
@@ -42,19 +40,17 @@ 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);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_   latch0 (.E(E), .D(D),        .Q(Q[0]));
+$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
+$_DLATCH_PP1_ latch2 (.E(E), .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]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .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];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -62,10 +58,10 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr_r.lib
+read_liberty dlatchlibmap_dlatchsr_r.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr_r.lib top
+dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
 
 clk2fflogic
 flatten
@@ -82,19 +78,17 @@ 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);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_   latch0 (.E(E), .D(D),        .Q(Q[0]));
+$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
+$_DLATCH_PP1_ latch2 (.E(E), .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]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .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];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -102,11 +96,11 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr_x.lib
+read_liberty dlatchlibmap_dlatchsr_x.lib
 opt
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr_x.lib top
+dfflibmap -liberty dlatchlibmap_dlatchsr_x.lib top
 
 clk2fflogic
 flatten
@@ -122,22 +116,21 @@ 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);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_   latch0 (.E(E), .D(D),        .Q(Q[0]));
+$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
+$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2]));
 
-// Formal checking of directly instantiated DFFSR doesn't work at the moment
+// TODO: this comment is just a copy from 'dfflibmap_formal.ys'
+// Formal checking of directly instantiated DLATCHSR 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]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .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];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -145,11 +138,11 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffn_dffe.lib
-read_liberty dfflibmap_dffsr_not_next.lib
+read_liberty dlatchlibmap_dlatchn.lib
+read_liberty dlatchlibmap_dlatchsr_not_data.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
+dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
 
 clk2fflogic
 flatten
@@ -165,19 +158,17 @@ 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);
+module top(input E, D, S, R, output [9: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]));
+$_DLATCH_P_   latch0 (.E(E), .D(D),        .Q(Q[0]));
+$_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
+$_DLATCH_PP1_ latch2 (.E(E), .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]));
+$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3]));
+$_DLATCHSR_NNN_ latch4 (.E(E), .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];
+assign Q[9:5] = ~Q[4:0];
 
 endmodule
 
@@ -185,10 +176,10 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr_not_next_l.lib
+read_liberty dlatchlibmap_dlatchsr_not_data_l.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr_not_next_l.lib top
+dfflibmap -liberty dlatchlibmap_dlatchsr_not_data_l.lib top
 
 clk2fflogic
 flatten
@@ -206,28 +197,24 @@ 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;
-
+module top(input E, D, S, R, output Q);
+  // DLATCHSR with priority R over S
+  always_latch
+    if      (R)  Q <= 1'b0;
+    else if (S)  Q <= 1'b1;
+    else if (E)  Q <= D;
 endmodule
 
 EOT
 
 proc
 opt
-read_liberty dfflibmap_dffn_dffe.lib
-read_liberty dfflibmap_dffsr_not_next.lib
+read_liberty dlatchlibmap_dlatchn.lib
+read_liberty dlatchlibmap_dlatchsr_not_data.lib
 
 copy top top_unmapped
 simplemap top
-dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_not_next.lib top
+dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_not_data.lib top
 
 clk2fflogic
 flatten
@@ -241,28 +228,27 @@ 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
+module top(input E, D, R, output Q);
+  // DLATCH with preset
+  always_latch
+    if     (~R)  Q <= 1'b1;
+    else if (E)  Q <= D;
 endmodule
 
 EOT
 
 proc
 opt
-read_liberty dfflibmap_dffn_dffe.lib
-read_liberty dfflibmap_dff_not_next.lib
+read_liberty dlatchlibmap_dlatchn.lib
+read_liberty dlatchlibmap_dlatch_not_data.lib
 
 copy top top_unmapped
 simplemap top
-dfflibmap -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dff_not_next.lib top
+dfflibmap -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatch_not_data.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
+equiv_status -assert equiv
diff --git a/tests/techmap/dlatchlibmap_proc_formal.ys b/tests/techmap/dlatchlibmap_proc_formal.ys
index 88cb97cdb..c570f8e2f 100644
--- a/tests/techmap/dlatchlibmap_proc_formal.ys
+++ b/tests/techmap/dlatchlibmap_proc_formal.ys
@@ -2,41 +2,19 @@
 
 read_verilog -sv -icells <<EOT
 
-module top(input C, D, E, S, R, output [7:0] Q);
+module top(input E, D, S, R, output [3: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_latch
+		if      (R)  Q[0] <= 1'b0;
+		else if (S)  Q[0] <= 1'b1;
+		else if (E)  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_latch
+		if      (S)  Q[1] <= 1'b1;
+		else if (R)  Q[1] <= 1'b0;
+		else if (E)  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];
+assign Q[3:2] = ~Q[1:0];
 
 endmodule
 
@@ -44,10 +22,10 @@ EOT
 
 proc
 opt
-read_liberty dfflibmap_dffsr_s.lib
+read_liberty dlatchlibmap_dlatchsr_s.lib
 
 copy top top_unmapped
-dfflibmap -liberty dfflibmap_dffsr_s.lib top
+dfflibmap -liberty dlatchlibmap_dlatchsr_s.lib top
 
 clk2fflogic
 flatten
@@ -62,7 +40,7 @@ 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
+dfflibmap -liberty dlatchlibmap_dlatchsr_r.lib top
 
 clk2fflogic
 flatten
@@ -76,7 +54,7 @@ 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
+dfflibmap -liberty dlatchlibmap_dlatchsr_mixedpol.lib top
 
 clk2fflogic
 flatten
@@ -90,7 +68,7 @@ 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
+dfflibmap -liberty dlatchlibmap_dlatchsr_not_data.lib top
 
 clk2fflogic
 flatten