mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-05-03 08:55:15 +00:00
Code Activity

dfflibmap: test dffsr and dffsre from proc with equiv

Browse source
This commit is contained in:
Emil J. Tywoniak 2026-01-28 18:26:26 +01:00
parent 18753c4c9e
commit e51f8024fa
1 changed files with 99 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

99
tests/techmap/dfflibmap_proc_formal.ys Normal file
View file

@ -0,0 +1,99 @@
##################################################################
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
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_r.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_mixedpol.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv
##################################################################
delete top equiv
copy top_unmapped top
dfflibmap -liberty dfflibmap_dffsr_not_next.lib top
async2sync
flatten
opt_clean -purge
equiv_make top top_unmapped equiv
equiv_induct equiv
equiv_status -assert equiv