mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-23 15:42:32 +00:00
Code Activity

dlatchlibmap: making a copy of test files dfflibmap* to dlatchlibmap*

Browse source
This commit is contained in:
Iztok Jeras 2026-06-22 01:08:39 +02:00
parent 6b1d5dedbf
commit 69df81756c
13 changed files with 843 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

100
tests/techmap/dlatchlibmap_proc_formal.ys Normal file
View file

@ -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