Minor fixes

backends_reviewed/write_smv/top_fulladder.v

@@ -7,21 +7,17 @@ module top
  output reg A,
  output reg cout
  );
- 
+
  initial begin
     A = 0;
     cout = 0;
  end
 
-`ifndef BUG
 always @(posedge x) begin
     A <=  y + cin;
 end
 always @(negedge x) begin
     cout <=  y + A;
 end
-`else
-assign {cout,A} =  cin - y * x;
-`endif
 
 endmodule

backends_reviewed/write_xaiger/top.v

@@ -7,13 +7,13 @@ module top
  output reg A,
  output reg cout
  );
- 
+
  reg ASSERT = 1;
  (* anyconst *) reg foo;
  (* anyseq *) reg too;
- 
 
- 
+
+
  initial begin
     begin
         A = 0;
@@ -21,23 +21,19 @@ module top
     end
  end
 
-`ifndef BUG
 always @(posedge x) begin
-    if ($initstate) 
+    if ($initstate)
         A <= 0;
     A <=  y + cin + too;
-    assume(too);    
+    assume(too);
     assume(s_eventually too);
 end
 always @(negedge x) begin
-    if ($initstate) 
+    if ($initstate)
         cout <= 0;
         cout <=  y + A + foo;
     assert(ASSERT);
     assert(s_eventually ASSERT);
 end
-`else
-assign {cout,A} =  cin - y * x;
-`endif
 
 endmodule

backends_reviewed/write_xaiger/top_cant_find_top.v

@@ -21,7 +21,7 @@ module top
     end
  end
 
-`ifndef BUG
+
 always @(posedge x) begin
     if ($initstate)
         A <= 0;
@@ -36,9 +36,6 @@ always @(negedge x) begin
     assert(ASSERT);
     assert(s_eventually ASSERT);
 end
-`else
-assign {cout,A} =  cin - y * x;
-`endif
 
 endmodule
 

backends_reviewed/write_xaiger/top_fulladder.v

@@ -7,21 +7,18 @@ module top
  output reg A,
  output reg cout
  );
- 
+
  initial begin
     A = 0;
     cout = 0;
  end
 
-`ifndef BUG
+
 always @(posedge x) begin
     A <=  y + cin;
 end
 always @(negedge x) begin
     cout <=  y + A;
 end
-`else
-assign {cout,A} =  cin - y * x;
-`endif
 
 endmodule

backends_reviewed/write_xaiger/top_mem.v

@@ -7,38 +7,30 @@ module top
 );
 	// Declare the RAM variable
 	reg [7:0] ram[63:0];
-	
+
 	initial begin
-        q_a <= 8'h00;        
+        q_a <= 8'h00;
         q_b <= 8'd0;
 	end
-	
+
 	// Port A
 	always @ (posedge clka)
 	begin
-`ifndef BUG        
-		if (we_a) 
-`else        
-		if (we_b) 
-`endif
+		if (we_a)
 		begin
 			ram[addr_a] <= data_a;
 			q_a <= data_a;
 		end
-		if (re_b) 
+		if (re_b)
 		begin
 			q_a <= ram[addr_a];
 		end
 	end
-	
+
 	// Port B
 	always @ (posedge clkb)
 	begin
-`ifndef BUG        
-		if (we_b) 
-`else        
-		if (we_a) 
-`endif
+		if (we_b)
 		begin
 			ram[addr_b] <= data_b;
 			q_b <= data_b;
@@ -48,5 +40,5 @@ module top
 			q_b <= ram[addr_b];
 		end
 	end
-	
-endmodule								 
+
+endmodule