mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-23 00:55:32 +00:00
Code Activity

satgen: Add support for dffe, sdff, sdffe, sdffce cells.

Browse source
This commit is contained in:
Marcelina Kościelnicka 2020-07-20 22:49:30 +02:00
parent dafe04d559
commit 0c6d0d4b5d
4 changed files with 88 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tests/arch/xilinx/pmgen_xilinx_srl.ys
View file

@ -35,7 +35,6 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_fixed
design -copy-from gate -as gate pmtest_xilinx_srl_pm_fixed
dff2dffe -unmap # sat does not support flops-with-enable yet
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter
@ -52,6 +51,5 @@ design -stash gate
design -copy-from gold -as gold pmtest_xilinx_srl_pm_variable
design -copy-from gate -as gate pmtest_xilinx_srl_pm_variable
dff2dffe -unmap # sat does not support flops-with-enable yet
miter -equiv -flatten -make_assert gold gate miter
sat -set-init-zero -seq 5 -verify -prove-asserts miter

21
tests/sat/dff.ys Normal file
View file

@ -0,0 +1,21 @@
# Ensure all sync-only DFFs have usable SAT models.
read_verilog -icells <<EOT
module top(...);
input C, D, R, E;
output [4:0] Q;
\$dff #(.WIDTH(1), .CLK_POLARITY(1'b1)) ff0 (.CLK(C), .D(D), .Q(Q[0]));
\$dffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .EN_POLARITY(1'b1)) ff1 (.CLK(C), .D(D), .EN(E), .Q(Q[1]));
\$sdff #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0)) ff2 (.CLK(C), .D(D), .SRST(R), .Q(Q[2]));
\$sdffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff3 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[3]));
\$sdffce #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff4 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[4]));
endmodule
EOT
# This ensures that 1) coarse cells have SAT models, 2) fine cells have SAT models, 3) they're equivalent
equiv_opt -assert simplemap