acw1251/bluecheck

A generic test bench written in Bluespec

bluecheck's Issues

RNGs produce different values during shrinking

First seen in this example. It may be due to the fact that these are functions and not actions.

import StmtFSM::*;
import Clocks::*;
import BlueCheck::*;

typedef 8 InputSz;
typedef TAdd#(InputSz, InputSz) OutputSz;
typedef TAdd#(OutputSz, 1) TempSz;

typedef Bit#(InputSz) Input;
typedef Bit#(OutputSz) Output;
typedef Bit#(TempSz) Temp;

typedef Int#(InputSz) Input_signed;
typedef Int#(OutputSz) Output_signed;
typedef Int#(TempSz) Temp_signed;

typedef UInt#(InputSz) Input_unsigned;
typedef UInt#(OutputSz) Output_unsigned;
typedef UInt#(TempSz) Temp_unsigned;

module [BlueCheck] checkMultiplier#(Reset soft_rst)(Empty);
    function Output mul_unsigned_ref( Input a, Input b );
        Output_unsigned a_tmp = unpack(zeroExtend(a));
        Output_unsigned b_tmp = unpack(zeroExtend(b));
        Output_unsigned out_tmp = a_tmp * b_tmp;
        return pack(out_tmp);
    endfunction
    function Output mul_signed_ref( Input a, Input b );
        Output_signed a_tmp = unpack(signExtend(a));
        Output_signed b_tmp = unpack(signExtend(b));
        Output_signed out_tmp = a_tmp * b_tmp;
        return pack(out_tmp);
    endfunction

    function Output mul_unsigned_impl( Input a, Input b );
        Temp a_tmp = zeroExtend(a);
        Temp b_tmp = zeroExtend(b) + 1;
        return truncate(a_tmp*b_tmp);
    endfunction
    function Output mul_signed_impl( Input a, Input b );
        Temp a_tmp = signExtend(a);
        Temp b_tmp = signExtend(b);
        return truncate(a_tmp*b_tmp);
    endfunction

    equiv("mul_unsigned", mul_unsigned_ref, mul_unsigned_impl);
    equiv("mul_signed", mul_signed_ref, mul_signed_impl);
endmodule

(* synthesize *)
module [Module] mkTestMultiplier();
    Clock clk <- exposeCurrentClock;
    MakeResetIfc my_rst <- mkReset(0, True, clk);
    Reset soft_rst = my_rst.new_rst;

    // Iterative Deepening
    BlueCheck_Params my_params = bcParams;
    ID_Params my_id_params = ID_Params {rst: my_rst, initialDepth: 10, testsPerDepth: 100, incDepth: ( ( \+ )(10) )};
    my_params.verbose = True;
    my_params.wedgeDetect = True;
    my_params.wedgeThreshold = 32'h100000;
    my_params.useIterativeDeepening = True;
    my_params.id = my_id_params;
    my_params.useShrinking = True;

    Stmt s <- mkModelChecker(checkMultiplier(soft_rst), my_params);
    mkAutoFSM(s);
endmodule

prop(_, Bool x) causes problems when x has a guard

In the following example, the compiler gives an error as a result of the prop check_output having a guard:

import Clocks::*;
import StmtFSM::*;
import BlueCheck::*;

// Only lets even numbers pass through
interface EvenFilter;
    method Action enq(Bit#(4) x);
    method Bit#(4) first;
    method Action deq;
endinterface

module mkEvenFilter(EvenFilter);
    Reg#(Bit#(4)) data <- mkReg(0);
    Reg#(Bool) valid <- mkReg(False);

    method Action enq(Bit#(4) x) if (!valid);
        // only enqueue if even
        if (x[0] == 0) begin
            data <= x;
            valid <= True;
        end
    endmethod

    method Bit#(4) first if (valid);
        return data;
    endmethod

    method Action deq if (valid);
        valid <= False;
    endmethod
endmodule

module [BlueCheck] checkBoolProp#(Reset soft_rst)(Empty);
    EvenFilter dut <- mkEvenFilter;

    function Bool check_output();
        return ((dut.first)[0] == 0);
    endfunction

    function Action enq(Bit#(4) x);
        return (action
                dut.enq(x);
            endaction);
    endfunction

    function Action deq;
        return (action
                dut.deq;
            endaction);
    endfunction

    prop("check_output", check_output);
    prop("enq", enq);
    prop("deq", deq);
endmodule

(* synthesize *)
module [Module] mkBoolPropExample(Empty);
    Clock clk <- exposeCurrentClock;
    MakeResetIfc my_rst <- mkReset(0, True, clk);
    Reset soft_rst = my_rst.new_rst;

    // Iterative Deepening
    BlueCheck_Params my_params = bcParams;
    ID_Params my_id_params = ID_Params {rst: my_rst, initialDepth: 10, testsPerDepth: 100, incDepth: ( ( \+ )(10) )};
    my_params.verbose = True;
    my_params.showTime = True;
    // my_params.showNoOp = True;
    my_params.wedgeDetect = True;
    my_params.useIterativeDeepening = True;
    my_params.id = my_id_params;
    my_params.useShrinking = True;

    Stmt s <- mkModelChecker(checkBoolProp(soft_rst), my_params);
    mkAutoFSM(s);
endmodule

equiv between functions doesn't get messages printed showing the operands