data/full_repos/permissive/153960117/hdl/relu.v
data/verilator_xmls/11f61b05-4f0f-4407-a14d-dd102003b800.xml
module relu
  #(parameter
    NUM_WIDTH = 16)
   (input  wire                 clk,
    input  wire                 bypass,

    input  wire [NUM_WIDTH-1:0] up_data,
    output reg  [NUM_WIDTH-1:0] dn_data
);





    function greater_than_zero;
        input [NUM_WIDTH-1:0] arg;

        begin
            greater_than_zero = ~arg[NUM_WIDTH-1];
        end
    endfunction


    reg  [NUM_WIDTH-1:0]    up_data_1p;





    always @(posedge clk) begin
        up_data_1p <= 'b0;

        if (bypass || greater_than_zero(up_data)) begin
            up_data_1p <= up_data;
        end
    end


    always @(posedge clk)
        dn_data <= up_data_1p;


`ifdef FORMAL

    reg  past_exists;
    reg  past_wait;
    initial begin
        restrict property (past_exists == 1'b0);
        restrict property (past_wait   == 1'b0);
    end


    always @(posedge clk)
        {past_exists, past_wait} <= {past_wait, 1'b1};








    always @(posedge clk)
        if (past_exists && $past(bypass, 2)) begin
            assert(dn_data == $past(up_data, 2));
        end



    always @(posedge clk)
        if (past_exists && ($signed($past(up_data, 2)) >= 0)) begin
            assert(dn_data == $past(up_data, 2));
        end



    always @(posedge clk)
        if (past_exists && $past(bypass, 2) && ($signed($past(up_data, 2)) < 0)) begin
            assert(dn_data == $past(up_data, 2));
        end


`endif
endmodule
module relu
  #(parameter
    NUM_WIDTH = 16)
   (input  wire                 clk,
    input  wire                 bypass,

    input  wire [NUM_WIDTH-1:0] up_data,
    output reg  [NUM_WIDTH-1:0] dn_data
);






    function greater_than_zero;
        input [NUM_WIDTH-1:0] arg;

        begin
            greater_than_zero = ~arg[NUM_WIDTH-1];
        end
    endfunction


    reg  [NUM_WIDTH-1:0]    up_data_1p;





    always @(posedge clk) begin
        up_data_1p <= 'b0;

        if (bypass || greater_than_zero(up_data)) begin
            up_data_1p <= up_data;
        end
    end


    always @(posedge clk)
        dn_data <= up_data_1p;


`ifdef FORMAL

    reg  past_exists;
    reg  past_wait;
    initial begin
        restrict property (past_exists == 1'b0);
        restrict property (past_wait   == 1'b0);
    end


    always @(posedge clk)
        {past_exists, past_wait} <= {past_wait, 1'b1};








    always @(posedge clk)
        if (past_exists && $past(bypass, 2)) begin
            assert(dn_data == $past(up_data, 2));
        end



    always @(posedge clk)
        if (past_exists && ($signed($past(up_data, 2)) >= 0)) begin
            assert(dn_data == $past(up_data, 2));
        end



    always @(posedge clk)
        if (past_exists && $past(bypass, 2) && ($signed($past(up_data, 2)) < 0)) begin
            assert(dn_data == $past(up_data, 2));
        end


`endif
endmodule