Index: vis_dev/vis-2.3/models/debug/2_faulty.v =================================================================== --- vis_dev/vis-2.3/models/debug/2_faulty.v (revision 33) +++ vis_dev/vis-2.3/models/debug/2_faulty.v (revision 33) @@ -0,0 +1,108 @@ +typedef enum {UN,DEUX,TROIS,QUATRE,CINQ,SIX,SEPT,HUIT,NEUF,DIX} state_t; + +module concret(clk); +input clk; + +reg p; +reg q; +input i,j; +state_t reg state; + +initial +begin +p = 1; +q = 1; +state = UN; +end + +always @(posedge clk) +begin +case(state) + UN : + if(j == 1) + begin + state = QUATRE; + p = 0; + q = 1; + end + else + if(i == 1) + begin + state = SIX; + p = 1; + q = 0; + end + else + begin + state = DEUX; + p = 1; + q = 1; + end + DEUX: + begin + state = TROIS; + p = 1; + q = 0; + end + // The faulty transition + TROIS: + begin + state = NEUF; + p = 1; + q = 1; + end + QUATRE: + begin + state = CINQ; + p = 1; + q = 0; + end + CINQ: + begin + state = CINQ; + p = 1; + q = 0; + end + SIX: + if (j == 0) + begin + state = SEPT; + p = 1; + q = 1; + end + else + begin + state = TROIS; + p = 1; + q = 0; + end + SEPT: + begin + state = HUIT; + p = 0; + q = 1; + end + HUIT: + begin + state = NEUF; + p = 1; + q = 1; + end + NEUF: + begin + state = DIX; + p = 0; + q = 0; + end + DIX: + begin + state = DIX; + p = 0; + q = 0; + end +endcase + +end + + +endmodule Index: vis_dev/vis-2.3/models/debug/2_golden.v =================================================================== --- vis_dev/vis-2.3/models/debug/2_golden.v (revision 33) +++ vis_dev/vis-2.3/models/debug/2_golden.v (revision 33) @@ -0,0 +1,107 @@ +typedef enum {UN,DEUX,TROIS,QUATRE,CINQ,SIX,SEPT,HUIT,NEUF,DIX} state_t; + +module concret(clk); +input clk; + +reg p; +reg q; +input i,j; +state_t reg state; + +initial +begin +p = 1; +q = 1; +state = UN; +end + +always @(posedge clk) +begin +case(state) + UN : + if(j == 1) + begin + state = QUATRE; + p = 0; + q = 1; + end + else + if(i == 1) + begin + state = SIX; + p = 1; + q = 0; + end + else + begin + state = DEUX; + p = 1; + q = 1; + end + DEUX: + begin + state = TROIS; + p = 1; + q = 0; + end + TROIS: + begin + state = QUATRE; + p = 0; + q = 1; + end + QUATRE: + begin + state = CINQ; + p = 1; + q = 0; + end + CINQ: + begin + state = CINQ; + p = 1; + q = 0; + end + SIX: + if (j == 0) + begin + state = SEPT; + p = 1; + q = 1; + end + else + begin + state = TROIS; + p = 1; + q = 0; + end + SEPT: + begin + state = HUIT; + p = 0; + q = 1; + end + HUIT: + begin + state = NEUF; + p = 1; + q = 1; + end + NEUF: + begin + state = DIX; + p = 0; + q = 0; + end + DIX: + begin + state = DIX; + p = 0; + q = 0; + end +endcase + +end + + +endmodule Index: vis_dev/vis-2.3/models/debug/and.v =================================================================== --- vis_dev/vis-2.3/models/debug/and.v (revision 33) +++ vis_dev/vis-2.3/models/debug/and.v (revision 33) @@ -0,0 +1,44 @@ +module andgate(clk,a); +input clk; +input a; +//output c; + +parameter ZERO = 2'b00; +parameter UN = 2'b01; +parameter DEUX = 2'b10; +parameter TROIS = 2'b11; +reg [1:0]c; +reg o; + +initial c[1:0] = ZERO; +initial o = 0; + +always @(posedge clk) +begin +case(c[1:0]) + ZERO: + if (a == 0) + begin + c[1:0] = UN; + o =0; + end + else + begin + c[1:0] = DEUX; + o=1; + end + UN : + begin + c = DEUX; + o=1; + end + + + + +endcase +end + +endmodule + + Index: vis_dev/vis-2.3/models/debug/and2.cnf =================================================================== --- vis_dev/vis-2.3/models/debug/and2.cnf (revision 33) +++ vis_dev/vis-2.3/models/debug/and2.cnf (revision 33) @@ -0,0 +1,31 @@ +c Nd37_48_0 9 +c a_0_0 7 +c Nd12_24_0 6 +c Nd36_49_0 5 +c b_0_0 8 +c Nd85_97_0 4 +c c_0_1 3 +c c_0_0 1 +p cnf 11 22 +1 2 0 +-1 -2 0 +2 0 +-7 -8 6 0 +7 -6 0 +8 -6 0 +-1 6 5 0 +1 -5 0 +-6 -5 0 +1 -6 9 0 +-1 -9 0 +6 -9 0 +5 9 4 0 +-5 -4 0 +-9 -4 0 +3 4 10 0 +-3 -10 0 +-4 -10 0 +-3 -4 11 0 +3 -11 0 +4 -11 0 +10 11 0 Index: vis_dev/vis-2.3/models/debug/and2.mv =================================================================== --- vis_dev/vis-2.3/models/debug/and2.mv (revision 33) +++ vis_dev/vis-2.3/models/debug/and2.mv (revision 33) @@ -0,0 +1,71 @@ +# vl2mv and2.v +# version: 2.1 +# date: 16:50:59 12/22/2011 (CET) +.model andgate +# I/O ports +.inputs a +.inputs b +# c = 0 +.names c$raw_n0 +0 +# non-blocking assignments for initial +# assign x = a & b +# a & b +.names a b _n2 +.def 0 +1 1 1 +.names _n2 x$raw_n1 +- =_n2 +# assign y = (a ) ? b : x +# (a ) ? b : x +.names a b x _n4 +.def 0 +1 1 - 1 +0 - 1 1 +.names _n4 y$raw_n3 +- =_n4 +# c = ~x + c +.names x _n7 +0 1 +1 0 +# ~x + c +.names _n9 +0 +.names _n7 c _n9 _n8 +.def 0 +0 0 1 1 +0 1 0 1 +1 0 0 1 +1 1 1 1 +# carry/borrow +.names _nb +0 +.names _n7 c _nb _na +.def 0 +- 1 1 1 +1 - 1 1 +1 1 - 1 +.names _n8 c$raw_n6 +- =_n8 +# conflict arbitrators +.names y$raw_n3 y +0 0 +1 1 +.names _nc +.def 0 + 1 +.names _nc c$raw_n6 _nd +.def 0 +1 0 0 +1 1 1 +.names x$raw_n1 x +0 0 +1 1 +# non-blocking assignments +# latches +.r c$raw_n0 c +0 0 +1 1 +.latch _nd c +# quasi-continuous assignment +.end Index: vis_dev/vis-2.3/models/debug/and2.v =================================================================== --- vis_dev/vis-2.3/models/debug/and2.v (revision 33) +++ vis_dev/vis-2.3/models/debug/and2.v (revision 33) @@ -0,0 +1,21 @@ +module andgate(clk,a,b); +input clk; +input a; +input b; + +reg c; +wire x; +wire y; + +initial c = 0; + +assign x = a & b; +assign y = (a)?b:x; + +always @(posedge clk) +begin + c = ~x + c; +end +endmodule + + Index: vis_dev/vis-2.3/models/debug/andé.cnf =================================================================== --- vis_dev/vis-2.3/models/debug/andé.cnf (revision 33) +++ vis_dev/vis-2.3/models/debug/andé.cnf (revision 33) @@ -0,0 +1,26 @@ +c Nd73_85_0 4 +c a_0_0 6 +c Nd13_36_0 7 +c Nd12_37_0 5 +c c_0_1 3 +c c_0_0 1 +p cnf 9 19 +1 2 0 +-1 -2 0 +2 0 +-6 1 5 0 +6 -5 0 +-1 -5 0 +6 -1 7 0 +-6 -7 0 +1 -7 0 +5 7 4 0 +-5 -4 0 +-7 -4 0 +3 4 8 0 +-3 -8 0 +-4 -8 0 +-3 -4 9 0 +3 -9 0 +4 -9 0 +8 9 0 Index: vis_dev/vis-2.3/models/debug/test.script =================================================================== --- vis_dev/vis-2.3/models/debug/test.script (revision 33) +++ vis_dev/vis-2.3/models/debug/test.script (revision 33) @@ -0,0 +1,6 @@ +rlmv %:2.mv +init +_createAbn +#aig +#_sat_debug -v 1 -k 1 -o %:2.cnf +