luke
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

dfflibmap: updated dlatchlibmap tests so they pass

This commit is contained in:
Iztok Jeras 2026-06-23 23:18:12 +02:00
parent 0df2169f81
commit 2c849e7415
2 changed files with 16 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
tests/techmap/dlatchlibmap.ys
View File

@ -29,7 +29,7 @@ design -load orig
dfflibmap -liberty dlatchlibmap.lib dfflibmap -liberty dlatchlibmap.lib
clean clean
select -assert-count 5 t:$_NOT_ select -assert-count 4 t:$_NOT_
select -assert-count 1 t:dlatchn select -assert-count 1 t:dlatchn
select -assert-count 4 t:dlatchsr select -assert-count 4 t:dlatchsr
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i 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 design -load orig
dfflibmap -prepare -liberty dlatchlibmap.lib 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 1 t:$_DLATCH_N_
select -assert-count 4 t:$_DLATCHSR_PPP_ select -assert-count 4 t:$_DLATCHSR_PPP_
select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i 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 design -load orig
dfflibmap -map-only -liberty dlatchlibmap.lib 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 0 t:dlatchn
select -assert-count 1 t:dlatchsr 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 design -load orig
dfflibmap -prepare -liberty dlatchlibmap.lib dfflibmap -prepare -liberty dlatchlibmap.lib
dfflibmap -map-only -liberty dlatchlibmap.lib dfflibmap -map-only -liberty dlatchlibmap.lib
clean clean
select -assert-count 5 t:$_NOT_ select -assert-count 4 t:$_NOT_
select -assert-count 1 t:dlatchn select -assert-count 1 t:dlatchn
select -assert-count 4 t:dlatchsr select -assert-count 4 t:dlatchsr
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i 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 dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib
clean clean
select -assert-count 5 t:$_NOT_ select -assert-count 4 t:$_NOT_
select -assert-count 1 t:dlatchn select -assert-count 1 t:dlatchn
select -assert-count 4 t:dlatchsr select -assert-count 4 t:dlatchsr
select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i 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 design -load orig
dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr
clean clean
# We have one more _NOT_ than with the regular dlatchsr # 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 1 t:dlatchn
select -assert-count 4 t:dlatchsr_mixedpol select -assert-count 4 t:dlatchsr_mixedpol
# The additional NOT is on latch2. # The additional NOT is on latch2.
# Originally, latch2.R is an active high "set". # Originally, latch2.R is an active high "preset".
# dlatchsr_mixedpol has functionally swapped labels due to the next_state inversion, # dlatchsr_mixedpol has functionally swapped labels due to the data_in inversion,
# so we use its CLEAR port for the "set", # so we use its CLEAR port for the "preset",
# but we have to invert it because the CLEAR pin is active low. # but we have to invert it because the CLEAR pin is active low.
# latch2.CLEAR = !R # latch2.CLEAR = !R
select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i

8
tests/techmap/dlatchlibmap_formal.ys
View File

@ -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_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1]));
$_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2])); $_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 // no assume when mapping to unset clear_preset_var
$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3])); $_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])); $_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); module top(input E, D, S, R, output Q);
// DLATCHSR with priority R over S // DLATCHSR with priority R over S
always_latch always @*
if (R) Q <= 1'b0; if (R) Q <= 1'b0;
else if (S) Q <= 1'b1; else if (S) Q <= 1'b1;
else if (E) Q <= D; else if (E) Q <= D;
@ -230,7 +226,7 @@ read_verilog <<EOT
module top(input E, D, R, output Q); module top(input E, D, R, output Q);
// DLATCH with preset // DLATCH with preset
always_latch always @*
if (~R) Q <= 1'b1; if (~R) Q <= 1'b1;
else if (E) Q <= D; else if (E) Q <= D;
endmodule endmodule