data/full_repos/permissive/176378198/src/instruction_register.v
1: b'%Warning-WIDTH: data/full_repos/permissive/176378198/src/instruction_register.v:27: Operator COND expects 8 bits on the Conditional False, but Conditional False\'s CONST \'4\'bzzzz\' generates 4 bits.\n                                                                                  : ... In instance instruction_register\n    assign bus[3:0] = IO ? instruction : 4\'bzzzz;\n                         ^\n                ... Use "/* verilator lint_off WIDTH */" and lint_on around source to disable this message.\n%Warning-WIDTH: data/full_repos/permissive/176378198/src/instruction_register.v:27: Operator ASSIGNW expects 4 bits on the Assign RHS, but Assign RHS\'s COND generates 8 bits.\n                                                                                  : ... In instance instruction_register\n    assign bus[3:0] = IO ? instruction : 4\'bzzzz;\n                    ^\n%Error: Exiting due to 2 warning(s)\n'
module instruction_register (
    inout [7:0] bus,
    input clk,
    input rst,


    output [3:0] MSB4,

    input IO,
    input II
);

    reg [7:0] instruction;
    initial instruction = 0;
    always @(posedge clk) begin
        if (rst)
            instruction = 0;
        else if (II)
            instruction = bus;
    end

    assign bus[3:0] = IO ? instruction : 4'bzzzz;
    assign MSB4 = instruction[7:4];

`ifdef FORMAL
    always @* begin

        if (IO)
            assume(!II);

        assert(MSB4 == instruction[7:4]);
        if (IO)
            assert(bus[3:0] == instruction[3:0]);
    end

    reg past_valid;
    initial past_valid = 0;
    always @(posedge clk) begin
        past_valid <= 1;

        if ($past(rst))
            assert(instruction == 0);
        else if ($past(II) && past_valid)
            assert(instruction == $past(bus));
    end
`endif
endmodule
module instruction_register (
    inout [7:0] bus,
    input clk,
    input rst,


    output [3:0] MSB4,

    input IO,
    input II
);


    reg [7:0] instruction;
    initial instruction = 0;
    always @(posedge clk) begin
        if (rst)
            instruction = 0;
        else if (II)
            instruction = bus;
    end

    assign bus[3:0] = IO ? instruction : 4'bzzzz;
    assign MSB4 = instruction[7:4];

`ifdef FORMAL
    always @* begin

        if (IO)
            assume(!II);

        assert(MSB4 == instruction[7:4]);
        if (IO)
            assert(bus[3:0] == instruction[3:0]);
    end

    reg past_valid;
    initial past_valid = 0;
    always @(posedge clk) begin
        past_valid <= 1;

        if ($past(rst))
            assert(instruction == 0);
        else if ($past(II) && past_valid)
            assert(instruction == $past(bus));
    end
`endif
endmodule