06/25/14 03:42:18 ./toolflow/build/condset_src_from_analysis_check.v

  1 
module CondSet_Check(comparand_a,out,error);
  2 
    input  [31:0] comparand_a;
  3 
    input  [31:0] out;
  4 
    output error;
  5 
    wire   [31:0] comparand_b;
  6 
    wire   [31:0] thenset;
  7 
    wire   [31:0] elseset;
  8 
 
  9 
    assign comparand_b  = 0;
 10 
    assign thenset      = 0;
 11 
    assign elseset      = 1;
 12 
 
 13 
    CondSet_CheckInt csc0( .comparand_a( comparand_a ), .comparand_b( comparand_b ), .thenset( thenset ), .elseset( elseset ), .out( out ), .error( error ) );
 14 
 
 15 
endmodule
 16 
 
 17 
module CondSet_CheckInt(comparand_a,comparand_b,thenset,elseset,out,error);
 18 
    input  [31:0] comparand_a;
 19 
    input  [31:0] comparand_b;
 20 
    input  [31:0] thenset;
 21 
    input  [31:0] elseset;
 22 
    input  [31:0] out;
 23 
    output error;
 24 
    
 25 
    // Trick ODIN into thinking every port is being used
 26 
    wire   use_all;
 27 
    assign use_all = comparand_a ^ comparand_b ^ thenset ^ elseset ^ out;
 28 
 
 29 
    wire   sign_a;
 30 
    wire   sign_b;
 31 
    assign sign_a  = comparand_a[31];
 32 
    assign sign_b  = comparand_b[31];
 33 
 
 34 
    wire [30:0] a;
 35 
    wire [30:0] b;
 36 
    assign a       = comparand_a[30:0];
 37 
    assign b       = comparand_b[30:0];
 38 
 
 39 
    wire [30:0] result;
 40 
    wire   sign_result;
 41 
    assign result      = out[30:0];
 42 
    assign sign_result = out[31];
 43 
 
 44 
    wire   result_or_reduced;
 45 
    assign result_or_reduced = |result;
 46 
 
 47 
    wire   result_eq_zero;
 48 
    assign result_eq_zero = ~sign_result & ~result_or_reduced;
 49 
 
 50 
    wire   result_gt_zero;
 51 
    assign result_gt_zero = ~sign_result & result_or_reduced;
 52 
 
 53 
    wire   in_gt_zero;
 54 
    assign in_gt_zero = ~sign_a & |a;
 55 
 
 56 
    wire   in_lt_zero;
 57 
    assign in_lt_zero = sign_a;
 58 
 
 59 
    wire   implication1;
 60 
    // a -> b == ~a v b
 61 
    // in <= 0 -> out > 0
 62 
    assign implication1 =  in_gt_zero | result_gt_zero;
 63 
 
 64 
    wire   implication2;
 65 
    // in > 0 -> out = 0
 66 
    assign implication2 = ~in_gt_zero | result_eq_zero;
 67 
 
 68 
    wire   implication3;
 69 
    // in < 0 -> out > 0
 70 
    assign implication3 = ~in_lt_zero | result_gt_zero;
 71 
 
 72 
    wire   all_implications_hold;
 73 
    assign all_implications_hold = implication1 & implication2 & implication3;
 74 
 
 75 
    assign error = ~all_implications_hold;
 76 
 
 77 
endmodule
 78