Finite state machine equivalence; checking designs with different number of ports

Hi. I've just tried to use Yosys to compare the following two different state machines written in Verilog:

old.v

module top ( 
    // ------------------------------------------------------------
    // Inputs
    // ------------------------------------------------------------
    input wire Clock ,
    input wire Reset ,
    input wire A,
    input wire B,
    // ------------------------------------------------------------
    // ------------------------------------------------------------
    // Outputs
    // ------------------------------------------------------------
    output wire Output1 ,
    output wire Output2 ,
    output reg [2:0]   Status
// ------------------------------------------------------------
);

// --------------------------------------------------------------------
// State Encoding
// --------------------------------------------------------------------
localparam STATE_Initial = 3'b000,
        STATE_1 = 3'b001,
        STATE_2 = 3'b010,
        STATE_3 = 3'b100;
// --------------------------------------------------------------------

// --------------------------------------------------------------------
// State reg Declarations
// --------------------------------------------------------------------
reg [2:0]  CurrentState;
reg [2:0]  NextState;
// --------------------------------------------------------------------
// --------------------------------------------------------------------
// Outputs
// --------------------------------------------------------------------
// 1-bit outputs
assign Output1 = (CurrentState  ==  STATE_1) | (CurrentState  ==  STATE_2);
assign Output2 = (CurrentState  ==  STATE_2);

// multi-bit outputs
always@( * ) begin
    Status = 3'b000;
    case (CurrentState)
    STATE_2: begin
        Status = 3'b010;
    end
    STATE_3: begin
        Status = 3'b011;
    end
    endcase
end
// --------------------------------------------------------------------

// Synchronous State-Transition
// --------------------------------------------------------------------
always@( posedge Clock) begin
    if (Reset)
        CurrentState  <= STATE_Initial;
    else
        CurrentState  <= NextState;
end
// --------------------------------------------------------------------
// --------------------------------------------------------------------
// Conditional State-Transition
// --------------------------------------------------------------------
always@( * ) begin
    NextState = CurrentState;
    case (CurrentState)
    STATE_Initial: begin
        NextState = STATE_1;
    end
    STATE_1: begin
        if (A & B) NextState = STATE_2;
    end
    STATE_2: begin
        if (A) NextState = STATE_3;
    end
    STATE_3: begin
        if (!A & B) NextState = STATE_Initial;
        else if (A & !B) NextState = STATE_3;
    end
    endcase
end
// --------------------------------------------------------------------
endmodule

new.v

module top ( 
    // ------------------------------------------------------------
    // Inputs
    // ------------------------------------------------------------
    input wire Clock ,
    input wire Reset ,
    input wire A,
    input wire B,
    // ------------------------------------------------------------
    // ------------------------------------------------------------
    // Outputs
    // ------------------------------------------------------------
    output wire Output1 ,
    output wire Output2 ,
    //////////////////////////////////
        // ECO begin
        // old specification
    //output reg [2:0]   Status
        // new specification
    output reg [3:0]   Status
// ------------------------------------------------------------
);

// --------------------------------------------------------------------
// State Encoding
// --------------------------------------------------------------------
    //////////////////////////////////
        // ECO begin
        // old specification
//localparam STATE_Initial = 3'b000,
//        STATE_1 = 3'b001,
//        STATE_2 = 3'b010,
//        STATE_3 = 3'b100;
        // new specification
localparam STATE_Initial = 8'b00000000,
        STATE_1 = 8'b00000001,
        STATE_2 = 8'b00000010,
        STATE_3 = 8'b00000100,
        STATE_4 = 8'b00001000,
        STATE_5 = 8'b00010000,
        STATE_6 = 8'b00100000,
        STATE_7 = 8'b01000000,
        STATE_8 = 8'b10000000;
        // ECO end
        // //////////////////////////////
// --------------------------------------------------------------------

// --------------------------------------------------------------------
// State reg Declarations
// --------------------------------------------------------------------
reg [7:0]  CurrentState;
reg [7:0]  NextState;
// --------------------------------------------------------------------
// --------------------------------------------------------------------
// Outputs
// --------------------------------------------------------------------
// 1-bit outputs
    //////////////////////////////////
        // ECO begin
        // old specification
//assign Output1 = (CurrentState  ==  STATE_1) | (CurrentState  ==  STATE_2);
//assign Output2 = (CurrentState  ==  STATE_2);
        // new specification
assign Output1 = (CurrentState  ==  STATE_1) 
                | (CurrentState  ==  STATE_2)
                | (CurrentState  ==  STATE_4)
                | (CurrentState  ==  STATE_8);
assign Output2 = (CurrentState  ==  STATE_3)
                | (CurrentState  ==  STATE_5);
        // ECO end
        // //////////////////////////////

// multi-bit outputs
always@( * ) begin
    Status = 4'b0000;
    case (CurrentState)
    STATE_2: begin
        Status = 4'b0010;
    end
    STATE_3: begin
        Status = 4'b0011;
    end
    //////////////////////////////////
        // ECO begin
        // old specification
        // new specification
    STATE_4: begin
        Status = 4'b0011;
    end
    STATE_5: begin
        Status = 4'b0101;
    end
    STATE_6: begin
        Status = 4'b0110;
    end
    STATE_7: begin
        Status = 4'b0111;
    end
    STATE_7: begin
        Status = 4'b1101;
    end
        // ECO end
        // //////////////////////////////
    endcase
end
// --------------------------------------------------------------------

// Synchronous State-Transition
// --------------------------------------------------------------------
always@( posedge Clock) begin
    if (Reset)
        CurrentState  <= STATE_Initial;
    else
        CurrentState  <= NextState;
end
// --------------------------------------------------------------------
// --------------------------------------------------------------------
// Conditional State-Transition
// --------------------------------------------------------------------
always@( * ) begin
    NextState = CurrentState;
    case (CurrentState)
    STATE_Initial: begin
        NextState = STATE_1;
    end
    STATE_1: begin
        if (A & B) NextState = STATE_2;
    end
    STATE_2: begin
        if (A) NextState = STATE_3;
    end
    STATE_3: begin
        if (!A & B) NextState = STATE_Initial;
        else if (A & !B) NextState = STATE_4;
    end
    //////////////////////////////////
        // ECO begin
        // old specification
        // new specification
    STATE_4: begin
        if (A) NextState = STATE_5;
        else NextState = STATE_6;
    end
    STATE_5: begin
        if (!A|!B) NextState = STATE_4;
        else NextState = STATE_6;
    end
    STATE_6: begin
        if (A^B) NextState = STATE_7;
    end
    STATE_7: begin
        if (!A^B) NextState = STATE_Initial;
        else NextState = STATE_8;
    end
    STATE_7: begin
        if (!A&!B) NextState = STATE_8;
        else NextState = STATE_2;
    end
        // ECO end
        // //////////////////////////////
    endcase
end
// --------------------------------------------------------------------
endmodule

And my Yosys script is listed below:

read_verilog old.v
hierarchy -top top
rename top top_v1
prep -top top_v1 -flatten
splitnets -ports
design -stash top_v1

read_verilog new.v
hierarchy -top top
rename top top_v2
prep -top top_v2 -flatten
splitnets -ports
design -stash top_v2

design -copy-from top_v1 -as top_old top_v1
design -copy-from top_v2 -as top_new top_v2

# formal verification with equiv_*
equiv_make -blacklist dont-match-signals.txt top_old top_new miter_1

opt -full

equiv_simple -undef -seq 10
equiv_induct -undef -seq 1000
equiv_status 
equiv_purge
equiv_miter -trigger miter_2 miter_1

# format verification with sat
#sat -verify -show-all -tempinduct -prove trigger 0 -set-init-undef -set-def-inputs -ignore_unknown_cells -set-at 0 a 1 -seq 10 miter_2

The signal State[3] is included in the ignore list (dont-match-signals.txt). The state machine described in new.v should be different from that described in old.v. But I found that the above Yosys script reports that they are equivalent.

If the line "equiv_induct -undef -seq 1000" is removed, the system will report:

Executing EQUIV_STATUS pass. Found 11 $equiv cells in miter_1: Of those cells 3 are proven and 8 are unproven. Unproven $equiv $auto$equiv_make.cc:241:find_same_wires$193: 1'0 \Status[2]_gate Unproven $equiv $auto$equiv_make.cc:241:find_same_wires$194: \Status[1]_gold \Status[1]_gate Unproven $equiv $auto$equiv_make.cc:241:find_same_wires$195: \Status[0]_gold \Status[0]_gate Unproven $equiv $auto$equiv_make.cc:241:find_same_wires$196: \Output1_gold \Output1_gate Unproven $equiv $auto$equiv_make.cc:241:find_same_wires$197: \Output2_gold \Output2_gate Unproven $equiv $auto$equiv_make.cc:270:find_same_wires$187: \NextState[2]_gold \NextState[2]_gate Unproven $equiv $auto$equiv_make.cc:270:find_same_wires$188: \NextState[1]_gold \NextState[1]_gate Unproven $equiv $auto$equiv_make.cc:270:find_same_wires$189: \NextState[0]_gold \NextState[0]_gate No $equiv cells found in top_new. No $equiv cells found in top_old. Found a total of 8 unproven $equiv cells.

I understand that equiv_induct will only perform a weak equivalence check. May I know whether my results are expected? I would also like to know the correct procedures of performing equivalent check of netlists having different ports or ports with different bus width. Many thanks.

YosysHQ / yosys