diff options
| author | Marcelina Kościelnicka <mwk@0x04.net> | 2020-07-20 22:49:30 +0200 |
|---|---|---|
| committer | Marcelina Kościelnicka <mwk@0x04.net> | 2020-07-24 03:19:21 +0200 |
| commit | 0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9 (patch) | |
| tree | fe9e286ed179c54348beeac052b06fd957454dac /tests/sat | |
| parent | dafe04d5590412cc8a95bee31810d96a358af3dd (diff) | |
| download | yosys-0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9.tar.gz yosys-0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9.tar.bz2 yosys-0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9.zip | |
satgen: Add support for dffe, sdff, sdffe, sdffce cells.
Diffstat (limited to 'tests/sat')
| -rw-r--r-- | tests/sat/dff.ys | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/tests/sat/dff.ys b/tests/sat/dff.ys new file mode 100644 index 000000000..ba3625871 --- /dev/null +++ b/tests/sat/dff.ys @@ -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 |