From 2c849e7415ba0227754d6ab3500f7185bfa385f8 Mon Sep 17 00:00:00 2001
From: Iztok Jeras <iztok.jeras@gmail.com>
Date: Tue, 23 Jun 2026 23:18:12 +0200
Subject: [PATCH] dfflibmap: updated dlatchlibmap tests so they pass

---
 tests/techmap/dlatchlibmap.ys        | 23 ++++++++++++++---------
 tests/techmap/dlatchlibmap_formal.ys |  8 ++------
 2 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys
index fa0ce65be..dd1a943e1 100644
--- a/tests/techmap/dlatchlibmap.ys
+++ b/tests/techmap/dlatchlibmap.ys
@@ -29,7 +29,7 @@ design -load orig
 dfflibmap -liberty dlatchlibmap.lib
 clean
 
-select -assert-count 5 t:$_NOT_
+select -assert-count 4 t:$_NOT_
 select -assert-count 1 t:dlatchn
 select -assert-count 4 t:dlatchsr
 select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
@@ -37,7 +37,7 @@ select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
 design -load orig
 dfflibmap -prepare -liberty dlatchlibmap.lib
 
-select -assert-count 11 t:$_NOT_
+select -assert-count 9 t:$_NOT_
 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
@@ -45,16 +45,20 @@ select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i
 design -load orig
 dfflibmap -map-only -liberty dlatchlibmap.lib
 
-select -assert-count 6 t:$_NOT_
+select -assert-count 5 t:$_NOT_
 select -assert-count 0 t:dlatchn
 select -assert-count 1 t:dlatchsr
+select -assert-count 1 t:$_DLATCH_P_
+select -assert-count 1 t:$_DLATCH_PP0_
+select -assert-count 1 t:$_DLATCH_PP1_
+select -assert-count 1 t:$_DLATCHSR_NNN_
 
 design -load orig
 dfflibmap -prepare -liberty dlatchlibmap.lib
 dfflibmap -map-only -liberty dlatchlibmap.lib
 clean
 
-select -assert-count 5 t:$_NOT_
+select -assert-count 4 t:$_NOT_
 select -assert-count 1 t:dlatchn
 select -assert-count 4 t:dlatchsr
 select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
@@ -64,7 +68,7 @@ dfflibmap -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatc
 dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
 clean
 
-select -assert-count 5 t:$_NOT_
+select -assert-count 4 t:$_NOT_
 select -assert-count 1 t:dlatchn
 select -assert-count 4 t:dlatchsr
 select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i
@@ -79,14 +83,15 @@ select -assert-count 5 t:dlatchsr
 design -load orig
 dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
 clean
+
 # We have one more _NOT_ than with the regular dlatchsr
-select -assert-count 6 t:$_NOT_
+select -assert-count 5 t:$_NOT_
 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",
+# Originally, latch2.R is an active high "preset".
+# dlatchsr_mixedpol has functionally swapped labels due to the data_in inversion,
+# so we use its CLEAR port for the "preset",
 # but we have to invert it because the CLEAR pin is active low.
 # latch2.CLEAR = !R
 select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i
diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys
index 8a6410156..135bfdc1a 100644
--- a/tests/techmap/dlatchlibmap_formal.ys
+++ b/tests/techmap/dlatchlibmap_formal.ys
@@ -122,10 +122,6 @@ $_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]));
 
-// 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
 $_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]));
@@ -199,7 +195,7 @@ read_verilog <<EOT
 
 module top(input E, D, S, R, output Q);
   // DLATCHSR with priority R over S
-  always_latch
+  always @*
     if      (R)  Q <= 1'b0;
     else if (S)  Q <= 1'b1;
     else if (E)  Q <= D;
@@ -230,7 +226,7 @@ read_verilog <<EOT
 
 module top(input E, D, R, output Q);
   // DLATCH with preset
-  always_latch
+  always @*
     if     (~R)  Q <= 1'b1;
     else if (E)  Q <= D;
 endmodule