Dual-modulus ÷15/16 circuit in Figure 15.35 of Razavi's book "Design of CMOS Phase-Locked Loops: From Circuit Level to Architecture Level"

dual_modulus_prescaler_15_16.sby

[tasks]
proof
cover

[options]
multiclock on

proof: mode prove
proof: depth 10

cover: mode cover
cover: depth 1000
cover: append 40

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

[script]
read_verilog -sv /foss/tools/yosys/share/yosys/simcells.v
read_verilog -formal -sv dual_modulus_prescaler_15_16.v

prep -top dual_modulus_prescaler_15_16

# Convert processes and map internal cells to logic
proc
techmap

# Optional: Further optimizations can be added here
opt

# Check for unconnected wires
check

[files]
dual_modulus_prescaler_15_16.v

dual_modulus_prescaler_15_16.v

// Dual-modulus ÷15/÷16 prescaler with asynchronous FF3/FF4
// MF = 0 -> ÷15 ; MF = 1 -> ÷16
module dual_modulus_prescaler_15_16 (
    input  wire clk,      // CK
    input  wire rst_n    // active-low synchronous reset of stage1 & stage2
);

    always @(*) begin
        if ($initstate) assume(!rst_n);
        else assume(rst_n);
    end

    always @($global_clock) begin
	if ($initstate)
	    assume(!clk);
   	else
	    assume(clk == !$past(clk));
    end

    always @(*) begin
	if ($initstate) begin
	    //assume(~Q1);
	    assume(~Q2);
	    assume(~Q4);
	    assume(MF);
	end
    end

    always @($global_clock) cover($fell(Q2));

    // — Stage 1 (FF1, FF2 synchronous) — ÷3/÷4 front end
    reg Q1, Q2;
    wire Q2_bar = ~Q2;

    always @(posedge clk) begin
        if (!rst_n)       Q1 <= 0;
        else              Q1 <= Q2_bar;
    end

    // Synchronous stage2 selector for FF2 input
    wire MF = Q3_bar | Q4_bar; // mode control signal
    wire D2 = Q1 & (MF | Q2_bar);

    always @(posedge clk) begin
        if (!rst_n) Q2 <= 0;
        else Q2 <= D2;
    end


    wire Q3, Q4;

    // Generate asynchronous trigger pulse for FF3 & FF4
    // Q3 toggles on each async trigger when Q2_bar transitions
    wire Q3_bar = ~Q3;
    // Q4 toggles on each async trigger when Q3_bar transitions
    wire Q4_bar = ~Q4;


    // FF3 using Yosys generic primitive — async ripple clock
    $_DFF_PN0_ FF3 (
        .C(Q2_bar),   // ASYNCHRONOUS derived clock
        .D(Q3_bar),
        .Q(Q3),
        .R(rst_n)
    );

    // FF4 asynchronous clocked by ~Q3
    $_DFF_PN0_ FF4 (
        .C(Q3_bar),   // ASYNCHRONOUS derived clock
        .D(Q4_bar),
        .Q(Q4),
        .R(rst_n)
    );


/*
    // — Stage 3 & Stage 4 (FF3 & FF4 asynchronous flip-flops) —
    // Q3 toggles on each async trigger
    reg Q3;
    always @(posedge Q2_bar or negedge rst_n) begin
        if (!rst_n)       Q3 <= 0;
        else              Q3 <= ~Q3;
    end

    // For illustration, we'll toggle Q4 on each trigger as well:
    reg Q4;
    always @(posedge Q3_bar or negedge rst_n) begin
        if (!rst_n)       Q4 <= 0;
        else              Q4 <= ~Q4;
    end
*/

endmodule