diff options
Diffstat (limited to 'tests/sat')
| -rw-r--r-- | tests/sat/clk2fflogic.ys | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/tests/sat/clk2fflogic.ys b/tests/sat/clk2fflogic.ys new file mode 100644 index 000000000..cdbeb022b --- /dev/null +++ b/tests/sat/clk2fflogic.ys @@ -0,0 +1,39 @@ +read_verilog <<EOT +module top(input clk, d, s, r, output reg [17:0] q); +always @(posedge clk or posedge s) if ( s) q[ 0] <= 1'b1; else q[ 0] <= d; +always @(posedge clk or negedge s) if (!s) q[ 1] <= 1'b1; else q[ 1] <= d; +always @(posedge clk or posedge r) if ( r) q[ 2] <= 1'b0; else q[ 2] <= d; +always @(posedge clk or negedge r) if (!r) q[ 3] <= 1'b0; else q[ 3] <= d; +always @(negedge clk or posedge s) if ( s) q[ 4] <= 1'b1; else q[ 4] <= d; +always @(negedge clk or negedge s) if (!s) q[ 5] <= 1'b1; else q[ 5] <= d; +always @(negedge clk or posedge r) if ( r) q[ 6] <= 1'b0; else q[ 6] <= d; +always @(negedge clk or negedge r) if (!r) q[ 7] <= 1'b0; else q[ 7] <= d; + +always @(posedge clk or posedge s or posedge r) if ( r) q[ 8] <= 1'b0; else if ( s) q[ 8] <= 1'b1; else q[ 8] <= d; +always @(posedge clk or posedge s or negedge r) if (!r) q[ 9] <= 1'b0; else if ( s) q[ 9] <= 1'b1; else q[ 9] <= d; +always @(posedge clk or negedge s or posedge r) if ( r) q[10] <= 1'b0; else if (!s) q[10] <= 1'b1; else q[10] <= d; +always @(posedge clk or negedge s or negedge r) if (!r) q[11] <= 1'b0; else if (!s) q[11] <= 1'b1; else q[11] <= d; +always @(negedge clk or posedge s or posedge r) if ( r) q[12] <= 1'b0; else if ( s) q[12] <= 1'b1; else q[12] <= d; +always @(negedge clk or posedge s or negedge r) if (!r) q[13] <= 1'b0; else if ( s) q[13] <= 1'b1; else q[13] <= d; +always @(negedge clk or negedge s or posedge r) if ( r) q[14] <= 1'b0; else if (!s) q[14] <= 1'b1; else q[14] <= d; +always @(negedge clk or negedge s or negedge r) if (!r) q[15] <= 1'b0; else if (!s) q[15] <= 1'b1; else q[15] <= d; + +always @(posedge clk) q[16] <= d; +always @(negedge clk) q[17] <= d; +endmodule +EOT +proc +select -assert-count 8 t:$adff +select -assert-count 8 t:$dffsr +select -assert-count 2 t:$dff +design -save gold + +simplemap +design -stash gate + +design -import gold -as gold +design -import gate -as gate +clk2fflogic + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports -set-init-undef -seq 10 miter |