D flip-flop with asynchronous reset

dff.sby

[tasks]
proof
cover

[options]
proof: mode prove
proof: depth 50

cover: mode cover
cover: depth 30
cover: append 10

multiclock on

[engines]
smtbmc yices
# smtbmc boolector
# abc pdr
# aiger avy
# aiger suprove

[script]
read_verilog -formal dff.v
read_verilog -formal -sv synchronizer.sv

prep -top dff

[files]
dff.v
synchronizer.sv

dff.v

// Design
// D flip-flop
// https://www.edaplayground.com/x/5dzJ

// If (asynchronous 'reset_sync' & enable') are true on the same clock, 
// and then 'reset_sync' is low on the next clock,
// then the asynchronous 'reset_sync' gets ignored and the 'enable' applied

module dff (clk, reset, enable, d, q);
	  
	input      clk;
	input      reset;
	input 	 enable;
	input      d;
	output reg q;


  	always @(posedge clk or posedge reset_sync)
  	begin
    	if (reset_sync) begin
      		// Asynchronous reset when reset goes high
	      	q <= 1'b0;      
	    end 

		else if(enable) 
		begin
      		// Assign D to Q on positive clock edge
      		q <= d;
    	end
  	end

	wire reset_sync;

    synchronizer #(.RESET_STATE(1)) reset_synchronizer(
        .clk(clk),
        .reset(reset),
        .data_i(0),
        .data_o(reset_sync));


`ifdef FORMAL

	(* gclk *) reg gbl_clk; 

	always @(posedge gbl_clk) assume(clk != $past(clk));

	reg first_clock_had_passed;
	initial first_clock_had_passed = 0;

	always @(posedge clk) first_clock_had_passed <= 1;

	localparam MAX_CNT = 16;

	reg[$clog2(MAX_CNT)-1:0] counter;
	initial counter = 0;

	always @(posedge clk) counter <= counter + 1;

	initial assume(reset);
	initial assume(enable);

	always @(posedge clk) if(counter == (MAX_CNT >> 1)) assume(reset != $past(reset));

	always @(posedge gbl_clk) if (!$rose(clk)) assume($stable(enable) && $stable(d)); 

	always @(posedge clk)
	begin
		if(first_clock_had_passed) 
		begin
			if(reset_sync || $past(reset_sync)) assert(q == 0);
		
			else if($past(enable)) assert(q == $past(d));

			else assert(q == $past(q));
		end
	end

	always @(posedge clk) cover(reset && enable && d && !clk);

`endif

endmodule

dff.ys

# read design
read_verilog dff.v
read_verilog -sv synchronizer.sv
hierarchy -check

# high-level synthesis
proc; opt; fsm; opt; memory; opt

# schematics
show -pause dff
show -pause synchronizer

dff_bmc.gtkw

[*]
[*] GTKWave Analyzer v3.3.94 (w)1999-2018 BSI
[*] Mon Sep  2 04:20:38 2019
[*]
[dumpfile] "/home/phung/Downloads/dff/dff_proof/engine_0/trace.vcd"
[dumpfile_mtime] "Mon Sep  2 04:20:22 2019"
[dumpfile_size] 2177
[savefile] "/home/phung/Downloads/dff/dff_bmc.gtkw"
[timestart] 0
[size] 960 995
[pos] -1 -1
*-5.216685 100 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 51
[signals_width] 257
[sst_expanded] 0
[sst_vpaned_height] 278
@28
smt_clock
@420
smt_step
@28
dff.clk
@22
dff.counter[3:0]
@29
dff.d
dff.enable
dff.q
@28
dff.reset
@29
dff.reset_sync
@28
dff.reset_synchronizer.clk
dff.reset_synchronizer.data_i
dff.reset_synchronizer.data_o
dff.reset_synchronizer.reset
dff.reset_synchronizer.sync0
dff.reset_synchronizer.sync1
dff.first_clock_had_passed
[pattern_trace] 1
[pattern_trace] 0

dff_cover.gtkw

[*]
[*] GTKWave Analyzer v3.3.94 (w)1999-2018 BSI
[*] Mon Aug 26 02:16:53 2019
[*]
[dumpfile] "/home/phung/Downloads/dff/dff_cover/engine_0/trace0.vcd"
[dumpfile_mtime] "Mon Aug 26 02:06:35 2019"
[dumpfile_size] 2189
[savefile] "/home/phung/Downloads/dff/dff_cover.gtkw"
[timestart] 0
[size] 960 995
[pos] -1 -1
*-5.415514 90 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[treeopen] dff.
[sst_width] 51
[signals_width] 287
[sst_expanded] 0
[sst_vpaned_height] 141
@28
smt_clock
@420
smt_step
@28
dff.clk
@29
dff.d
dff.enable
dff.q
@28
dff.reset
dff.reset_synchronizer.sync0
dff.reset_synchronizer.sync1
@29
dff.reset_sync
[pattern_trace] 1
[pattern_trace] 0

dff_induction.gtkw

[*]
[*] GTKWave Analyzer v3.3.94 (w)1999-2018 BSI
[*] Wed Jul  3 01:12:24 2019
[*]
[dumpfile] "/home/phung/Downloads/afifo/dff_proof/engine_0/trace_induct.vcd"
[dumpfile_mtime] "Wed Jul  3 01:05:57 2019"
[dumpfile_size] 7316
[savefile] "/home/phung/Downloads/afifo/dff_induction.gtkw"
[timestart] 0
[size] 960 995
[pos] -51 -1
*-7.270348 490 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1 -1
[sst_width] 51
[signals_width] 185
[sst_expanded] 0
[sst_vpaned_height] 141
@28
smt_clock
@420
smt_step
@28
dff.clk
@22
dff.counter[3:0]
@28
dff.d
dff.enable
dff.q
dff.reset
dff.reset_sync
dff.reset_synchronizer.clk
dff.reset_synchronizer.data_i
dff.reset_synchronizer.data_o
dff.reset_synchronizer.reset
dff.reset_synchronizer.sync0
dff.reset_synchronizer.sync1
[pattern_trace] 1
[pattern_trace] 0

synchronizer.sv

// https://github.com/jbush001/NyuziProcessor/blob/master/hardware/core/synchronizer.sv
//
// Copyright 2011-2015 Jeff Bush
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//

//
// Transfer a signal into a clock domain, avoiding metastability and
// race conditions due to propagation delay.
//

module synchronizer
    #(parameter WIDTH = 1,
    parameter RESET_STATE = 0)

    (input                      clk,
    input                       reset,
    output logic[WIDTH - 1:0]   data_o,
    input [WIDTH - 1:0]         data_i);

    logic[WIDTH - 1:0] sync0;
    logic[WIDTH - 1:0] sync1;

    always_ff @(posedge clk, posedge reset)
    begin
        if (reset)
        begin
            sync0 <= {WIDTH{RESET_STATE}};
            sync1 <= {WIDTH{RESET_STATE}};
            data_o <= {WIDTH{RESET_STATE}};
        end
        else
        begin
            sync0 <= data_i;
            sync1 <= sync0;
            data_o <= sync1;
        end
    end
endmodule