formal_tristate.sby

[options]
mode bmc
depth 20
expect pass

[engines]
smtbmc boolector

[script]
read -formal test.v
prep -top test
flatten
tribuf -formal

[file test.v]
module test(
    input clk,
    input data_a, data_b,
    input en_a, en_b,
    output data_bus
);
    reg [7:0] counter_a = 1;
    reg [7:0] counter_b = 1;
    wire bus;

    always @(posedge clk) begin
        counter_a <= counter_a == 3 ? 0 : counter_a + 1;
        counter_b <= counter_b == 5 ? 0 : counter_b + 1;
    end

    tristate_driver driver_a(
        .bus(bus),
        .to_bus(data_a),
        .en(en_a && counter_a == 0),
        .from_bus(data_bus)
    );

    tristate_driver driver_b(
        .bus(bus),
        .to_bus(data_b),
        .en(en_b && counter_b == 0)
    );

endmodule

module tristate_driver(
    input to_bus,
    output from_bus,
    input en,
    inout bus
);
    assign bus = en ? to_bus : 1'bz;

    assign from_bus = bus;

endmodule