CLP modeling

[address@hidden]

Hi,

 

I have written a Gnu Prolog program to modeling the behavior of a program and to generate test data for the program, there only one solution for the CLP constraint program, which is [0,0,1,0,0,0,1,0,0,0,1,0,0,0,1,0], but I got more than 4,000 solutions. Can someone help me investigating the Gnu Prolog program and give me some advice on modeling the program behavior in GNU Prolog? Thank you!

 

The program segment is as following:

if ((fifo_clr_n)==(1'b0))
             begin
               cnt <= 4'b0000;
             end
          else
             if ((fifo_reset_n)==(1'b0))
                begin
                  cnt <=  4'b0000;
                end
             else
                begin
                  case ({put, get})
                    2'b10:
                        if ((cnt)<(8))
                           begin
                             cnt =  (cnt)+2;
                           end
                    2'b01:
                        if ((cnt)>(0))
                           begin
                             cnt =  (cnt)-1;
                           end
                    2'b11:
                        begin
                        end
                  endcase
                end
        end

 

The GNU Prolog program is as following:

q(OUTPUTS):-
 get_fd_labeling(Lab),
 statistics(runtime, _),
 
 findall(INPUTS, temp(Lab,INPUTS,OUTPUTS) , INLIST),
 temp(Lab,INPUTS,OUTPUTS),
 statistics(runtime, [_,Y]),
 /*write(OUTPUTS), nl,
 write(INPUTS), nl,*/
 output_results(INLIST),
 write('time: '), write(Y), nl.

 

 output_results([]).
 output_results([IN | REST]) :-
 write('input: '), write(IN), nl,
 output_results(REST).
/*----------- Model definition -----------*/

 

temp(Lab, INPUTS, OUTPUTS):-

 

INPUTS = [Fifo_clr_n_0, Fifo_reset_n_0, Put_0, Get_0, Fifo_clr_n_1, Fifo_reset_n_1, Put_1, Get_1, Fifo_clr_n_2, Fifo_reset_n_2, Put_2, Get_2, Fifo_clr_n_3, Fifo_reset_n_3, Put_3, Get_3],
OUTPUTS = [Cnt_3_1_0,Cnt_3_1_1,Cnt_3_1_2,Cnt_3_1_3],

 

fd_domain(Fifo_clr_n_0, 0, 1),
fd_domain(Fifo_clr_n_1, 0, 1),
fd_domain(Fifo_clr_n_2, 0, 1),
fd_domain(Fifo_clr_n_3, 0, 1),
fd_domain(Fifo_reset_n_0, 0, 1),
fd_domain(Fifo_reset_n_1, 0, 1),
fd_domain(Fifo_reset_n_2, 0, 1),
fd_domain(Fifo_reset_n_3, 0, 1),
fd_domain(Cnt_0_0, 0, 7),
fd_domain(Cnt_0_1, 0, 7),
fd_domain(Cnt_1_1, 0, 7),
fd_domain(Cnt_2_1, 0, 7),
fd_domain(Cnt_3_1, 0, 7),
fd_domain(Cnt_3_1_0, 0, 1),
fd_domain(Cnt_3_1_1, 0, 1),
fd_domain(Cnt_3_1_2, 0, 1),
fd_domain(Cnt_3_1_3, 0, 1),
fd_domain(Get_0, 0, 1),
fd_domain(Get_1, 0, 1),
fd_domain(Get_2, 0, 1),
fd_domain(Get_3, 0, 1),
fd_domain(Put_0, 0, 1),
fd_domain(Put_1, 0, 1),
fd_domain(Put_2, 0, 1),
fd_domain(Put_3, 0, 1),

 

Cnt_0_0 #= 0,
(Fifo_clr_n_0 #= 1) #==> Cnt_0_1 #= Cnt_0_0,
(#\(Fifo_clr_n_0 #= 1) #/\ (Fifo_reset_n_0 #= 1)) #==> Cnt_0_1 #= Cnt_0_0,
((#\(Fifo_clr_n_0 #= 1)) #/\ (#\(Fifo_reset_n_0 #= 1)) #/\ (Put_0 #= 1) #/\ (Get_0 #= 0) #/\ (Cnt_0_0 #< 8)) #==> Cnt_0_1 #= Cnt_0_0 + 2,
((#\(Fifo_clr_n_0 #= 1)) #/\ (#\(Fifo_reset_n_0 #= 1)) #/\ (Put_0 #= 0) #/\ (Get_0 #= 1) #/\ (Cnt_0_0 #> 0)) #==> Cnt_0_1 #= Cnt_0_0 - 1,
((#\(Fifo_clr_n_0 #= 1)) #/\ (#\(Fifo_reset_n_0 #= 1)) #/\ (Put_0 #= 1) #/\ (Get_0 #= 1)) #==> Cnt_0_1 #= Cnt_0_0,
((#\(Fifo_clr_n_0 #= 1)) #/\ (#\(Fifo_reset_n_0 #= 1)) #/\ (Put_0 #= 0) #/\ (Get_0 #= 0)) #==> Cnt_0_1 #= Cnt_0_0,

 

(Fifo_clr_n_1 #= 1) #==> Cnt_1_1 #= 0,
(#\(Fifo_clr_n_1 #= 1) #/\ (Fifo_reset_n_1 #= 1)) #==> Cnt_1_1 #= 0,
((#\(Fifo_clr_n_1 #= 1)) #/\ (#\(Fifo_reset_n_1 #= 1)) #/\ (Put_1 #= 1) #/\ (Get_1 #= 0) #/\ (Cnt_0_1 #< 8)) #==> Cnt_1_1 #= Cnt_0_1 + 2,
((#\(Fifo_clr_n_1 #= 1)) #/\ (#\(Fifo_reset_n_1 #= 1)) #/\ (Put_1 #= 0) #/\ (Get_1 #= 1) #/\ (Cnt_0_1 #> 0)) #==> Cnt_1_1 #= Cnt_0_1 - 1,
((#\(Fifo_clr_n_1 #= 1)) #/\ (#\(Fifo_reset_n_1 #= 1)) #/\ (Put_1 #= 1) #/\ (Get_1 #= 1)) #==> Cnt_1_1 #= Cnt_0_1,
((#\(Fifo_clr_n_1 #= 1)) #/\ (#\(Fifo_reset_n_1 #= 1)) #/\ (Put_1 #= 0) #/\ (Get_1 #= 0)) #==> Cnt_1_1 #= Cnt_0_1,

 

(Fifo_clr_n_2 #= 1) #==> Cnt_2_1 #= 0,
(#\(Fifo_clr_n_2 #= 1) #/\ (Fifo_reset_n_2 #= 1)) #==> Cnt_2_1 #= 0,
((#\(Fifo_clr_n_2 #= 1)) #/\ (#\(Fifo_reset_n_2 #= 1)) #/\ (Put_2 #= 1) #/\ (Get_2 #= 0) #/\ (Cnt_1_1 #< 8)) #==> Cnt_2_1 #= Cnt_1_1 + 2,
((#\(Fifo_clr_n_2 #= 1)) #/\ (#\(Fifo_reset_n_2 #= 1)) #/\ (Put_2 #= 0) #/\ (Get_2 #= 1) #/\ (Cnt_1_1 #> 0)) #==> Cnt_2_1 #= Cnt_1_1 - 1,
((#\(Fifo_clr_n_2 #= 1)) #/\ (#\(Fifo_reset_n_2 #= 1)) #/\ (Put_2 #= 1) #/\ (Get_2 #= 1)) #==> Cnt_2_1 #= Cnt_1_1,
((#\(Fifo_clr_n_2 #= 1)) #/\ (#\(Fifo_reset_n_2 #= 1)) #/\ (Put_2 #= 0) #/\ (Get_2 #= 0)) #==> Cnt_2_1 #= Cnt_1_1,

 

(Fifo_clr_n_3 #= 1) #==> Cnt_3_1 #= 0,
(#\(Fifo_clr_n_3 #= 1) #/\ (Fifo_reset_n_3 #= 1)) #==> Cnt_3_1 #= 0,
((#\(Fifo_clr_n_3 #= 1)) #/\ (#\(Fifo_reset_n_3 #= 1)) #/\ (Put_3 #= 1) #/\ (Get_3 #= 0) #/\ (Cnt_2_1 #< 8)) #==> Cnt_3_1 #= Cnt_2_1 + 2,
((#\(Fifo_clr_n_3 #= 1)) #/\ (#\(Fifo_reset_n_3 #= 1)) #/\ (Put_3 #= 0) #/\ (Get_3 #= 1) #/\ (Cnt_2_1 #> 0)) #==> Cnt_3_1 #= Cnt_2_1 - 1,
((#\(Fifo_clr_n_3 #= 1)) #/\ (#\(Fifo_reset_n_3 #= 1)) #/\ (Put_3 #= 1) #/\ (Get_3 #= 1)) #==> Cnt_3_1 #= Cnt_2_1,
((#\(Fifo_clr_n_3 #= 1)) #/\ (#\(Fifo_reset_n_3 #= 1)) #/\ (Put_3 #= 0) #/\ (Get_3 #= 0)) #==> Cnt_3_1 #= Cnt_2_1,

 

Cnt_3_1 - Cnt_3_1_0 * 8 + Cnt_3_1_1 * 4 + Cnt_3_1_2 * 2 + Cnt_3_1_3 #= 0,

 

 lab(Lab, INPUTS).

 

/*----------- End of model definition -----------*/

 

lab(normal,L):-
        fd_labeling(L).

 

lab(ff,L):-
        fd_labelingff(L).

 

get_fd_labeling(Lab):-
        argument_counter(C),
        get_labeling1(C,Lab).

 

get_labeling1(1,normal).

 

get_labeling1(2,Lab):-
        argument_value(1,Lab).
:-initialization(q([1,0,0,0])).