From f88a2c3bdb5e169f22184413a550ed62c24b1e36 Mon Sep 17 00:00:00 2001
From: Denis Tereshkin <denis@kasan.ws>
Date: Thu, 6 Nov 2025 17:50:04 +0700
Subject: [PATCH] Verify implemented instructions

---
 src/alu.verilog      |   4 +
 src/cpu.verilog      | 250 ++++++++++++++++++++++++++++++-------------
 src/mio.verilog      |  51 +++++++--
 src/parameters.vh    | 180 +++++++++++++++----------------
 src/slon.sby         |  32 ++++++
 src/slon_decoder.sby |  24 +++++
 6 files changed, 367 insertions(+), 174 deletions(-)
 create mode 100644 src/slon.sby
 create mode 100644 src/slon_decoder.sby

diff --git a/src/alu.verilog b/src/alu.verilog
index 76f3d00..5954282 100644
--- a/src/alu.verilog
+++ b/src/alu.verilog
@@ -1,6 +1,7 @@
 `default_nettype none
 module alu (A, B, C, sel, result, r_n, r_z, r_v, r_c);
 
+
 `include "parameters.vh"
 
     input logic [7:0]  A;
@@ -24,6 +25,9 @@ assign diff = A - B - (1 - C);
 
 always_comb
   begin
+      result = 0;
+      r_c = 0;
+      r_v = 0;
       case (sel)
         OP_OR:
           begin
diff --git a/src/cpu.verilog b/src/cpu.verilog
index 12cbdc8..44bc8e0 100644
--- a/src/cpu.verilog
+++ b/src/cpu.verilog
@@ -6,7 +6,8 @@ module cpu
     clk,
     nmi,
     irq,
-   o_led);
+    o_led,
+    o_state);
 
 `include "parameters.vh"
 
@@ -33,6 +34,7 @@ localparam
     input wire nmi;
     input wire irq;
     output wire [5:0] o_led;
+    output wire [31:0] o_state;
 
 
     reg [7:0]  X;
@@ -88,6 +90,10 @@ initial pending_a_read = 0;
 initial pending_x_read = 0;
 initial pending_rel_branch = 0;
 
+assign o_state[3:0] = state;
+assign o_state[31:24] = A;
+assign o_state[23:16] = X;
+
 alu alui(
          .A(alu_op_1),
          .B(alu_op_2),
@@ -128,30 +134,6 @@ initial state = STATE_FETCH;
 initial PC = 0;
 initial mem_sel = 0;
 
-always @(posedge clk)
-  if (state == STATE_START_0)
-    begin
-        mem_sel <= DMUX_AUX;
-        mem_aux_addr <= 16'hfffc;
-        state <= STATE_START_1;
-    end
-  else if (state == STATE_START_1)
-    begin
-        state <= STATE_START_2;
-    end
-  else if (state == STATE_START_2)
-    begin
-        PC[7:0] <= mem_data;
-        mem_aux_addr <= 16'hfffd;
-        state <= STATE_START_3;
-    end
-  else if(state == STATE_START_3)
-    begin
-        PC[15:8] <= mem_data;
-        mem_sel <= DMUX_PC;
-        state <= STATE_FETCH;
-    end
-
 always_comb
   begin
       alu_op_1 = 0;
@@ -210,9 +192,7 @@ always @(posedge clk)
         PC <= PC + 1;
         state <= STATE_EXECUTE;
     end
-
-always @(posedge clk)
-  if (state == STATE_EXECUTE)
+  else if (state == STATE_EXECUTE)
     begin
         instr <= mem_data;
         if (address_code == ADDR_MODE_ABSOLUTE)
@@ -260,9 +240,7 @@ always @(posedge clk)
                 end
           end
     end
-
-always @(posedge clk)
-  if (state == STATE_BRANCH)
+  else if (state == STATE_BRANCH)
     begin
         if (pending_rel_branch)
           begin
@@ -271,9 +249,7 @@ always @(posedge clk)
         pending_rel_branch <= 0;
         state <= STATE_FETCH;
     end
-
-always @(posedge clk)
-  if (state == STATE_FETCH_DATA_2)
+  else if (state == STATE_FETCH_DATA_2)
     begin
         if (address_code == ADDR_MODE_ABSOLUTE)
           begin
@@ -284,10 +260,7 @@ always @(posedge clk)
               PC <= PC + 1'b1;
           end
     end
-
-always @(posedge clk)
-  begin
-      if (state == STATE_EXECUTE_DATA_2)
+    else if (state == STATE_EXECUTE_DATA_2)
         begin
             if (address_code == ADDR_MODE_ABSOLUTE)
               begin
@@ -304,7 +277,6 @@ always @(posedge clk)
                     end
               end
         end
-  end
 
 always_comb
   begin
@@ -323,43 +295,173 @@ always_comb
         end
   end
 
+`ifdef FORMAL
+
+    logic f_past_valid;
+    logic f2_past_valid;
+    logic f3_past_valid;
+    logic f4_past_valid;
+    logic f5_past_valid;
+
+initial f_past_valid = 0;
+initial f2_past_valid = 0;
+initial f3_past_valid = 0;
+initial f4_past_valid = 0;
+initial f5_past_valid = 0;
+always @(posedge clk)
+  f_past_valid <= 1;
+
+always @(posedge clk)
+    if (f_past_valid)
+      f2_past_valid <= 1;
+
+always @(posedge clk)
+    if (f2_past_valid)
+      f3_past_valid <= 1;
+
+always @(posedge clk)
+    if (f3_past_valid)
+      f4_past_valid <= 1;
+
+always @(posedge clk)
+    if (f4_past_valid)
+      f5_past_valid <= 1;
+
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_EXECUTE)
+    if ($past(decoded_instr) == I_DEX)
+      begin
+          assert(X == $past(X, 2) - 8'd1);
+          assert($past(PC) == $past(PC, 3) + 16'd1);
+          assert(P[P_Z] == (X == 0));
+          assert(P[P_N] == (X[7] == 1));
+          assert($stable(P[P_C]));
+          assert($stable(P[P_V]));
+          assert($stable(P[P_B]));
+          assert($stable(P[P_D]));
+          assert($stable(P[P_I]));
+      end
+
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_EXECUTE)
+    if ($past(decoded_instr) == I_LDX && $past(address_code) == ADDR_MODE_IMMEDIATE)
+      begin
+          assert(X == $past(mem_data));
+          assert(P[P_Z] == (X == 0));
+          assert(P[P_N] == (X[7] == 1));
+          if (f3_past_valid)
+            begin
+                assert($past(PC) == $past(PC, 3) + 16'd2);
+            end
+      end
+
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_EXECUTE)
+    if ($past(decoded_instr) == I_LDA && $past(address_code) == ADDR_MODE_IMMEDIATE)
+      begin
+          assert(A == $past(mem_data));
+          assert(P[P_Z] == (A == 0));
+          assert(P[P_N] == (A[7] == 1));
+          if (f3_past_valid)
+            begin
+                assert($past(PC) == $past(PC, 3) + 16'd2);
+            end
+      end
+
+    logic [15:0] f_abs_address;
+
+initial f_abs_address = 0;
 always_comb
   begin
-      mem_addr_offset = 0;
-      // if (state == STATE_FETCH)
-      //   begin
-      //       mem_addr_offset = 1;
-      //   end
-      // if (state == STATE_BRANCH)
-      //   begin
-      //       mem_addr_offset = 0;
-      //   end
-      // if (state == STATE_EXECUTE)
-      //   begin
-      //       if (address_code == ADDR_MODE_IMMEDIATE)
-      //         begin
-      //             mem_addr_offset = 1;
-      //         end
-      //       else if (address_code == ADDR_MODE_RELATIVE)
-      //         begin
-      //             if (decoded_instr == I_BNE )
-      //               if (!P[P_Z])
-      //                 mem_addr_offset = 0;
-      //               else
-      //                 mem_addr_offset = 1;
-      //         end
-      //       else if (address_code == ADDR_MODE_ABSOLUTE)
-      //         begin
-      //             mem_addr_offset = 1;
-      //         end
-      //   end
-      // if (state == STATE_FETCH_DATA_2)
-      //   begin
-      //       if (address_code == ADDR_MODE_ABSOLUTE)
-      //         begin
-      //             mem_addr_offset = 1;
-      //         end
-      //   end
+      f_abs_address = 0;
+      if (f_past_valid)
+        begin
+            f_abs_address[15:8] = mem_data;
+            f_abs_address[7:0] = mem_aux_addr;
+        end
   end
 
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_EXECUTE_DATA_2)
+    if ($past(decoded_instr) == I_STA && $past(address_code) == ADDR_MODE_ABSOLUTE)
+      begin
+          assert(mem_wr == 1'b1);
+          assert(mem_data_wr == A);
+          assert(f_abs_address == mem_addr_eff);
+          if (f3_past_valid)
+            begin
+                assert(PC == $past(PC, 3) + 16'd3);
+            end
+      end
+
+always @(posedge clk)
+  if (f2_past_valid &&
+      state == STATE_EXECUTE &&
+      $past(state) == STATE_FETCH &&
+      $past(state, 2) == STATE_EXECUTE_DATA_2)
+    if ($past(address_code, 2) == ADDR_MODE_ABSOLUTE)
+      begin
+          if ($past(decoded_instr, 2) == I_EOR)
+            assert(A == $past(A, 2) ^ $past(mem_data));
+          else
+            assume(0);
+
+          assert($past(mem_wr, 2) == 1'b0);
+          assert($past(f_abs_address, 2) == $past(mem_addr_eff, 2));
+          assert(P[P_Z] == (A == 0));
+          assert(P[P_N] == (A[7] == 1));
+          assert(P[P_C] == $past(P[P_C], 3));
+          assert(P[P_V] == $past(P[P_V], 3));
+          assert(P[P_B] == $past(P[P_B], 3));
+          assert(P[P_D] == $past(P[P_D], 3));
+          assert(P[P_I] == $past(P[P_I], 3));
+          assert(S == $past(S, 3));
+          assert(X == $past(X, 3));
+          assert(Y == $past(Y, 3));
+
+          if (f3_past_valid)
+            begin
+                assert($past(PC, 2) == $past(PC, 5) + 16'd3);
+            end
+      end
+
+always @(posedge clk)
+  if (f2_past_valid && state == STATE_FETCH)
+    if ($past(decoded_instr) == I_BNE && $past(address_code) == ADDR_MODE_RELATIVE)
+      begin
+          if ($past(state) == STATE_BRANCH)
+            begin
+                assert(PC == $past(PC) + {{8{$past(mem_data[7])}}, mem_data[7:0]} + 1'b1);
+                assert(!$past(P[P_Z]));
+            end
+          else
+            begin
+                assert(PC == $past(PC) + 1'b1);
+                assert($past(P[P_Z]));
+            end
+      end
+
+always @(posedge clk)
+  if (f3_past_valid && state == STATE_FETCH)
+    if ($past(decoded_instr) == I_JMP && $past(address_code) == ADDR_MODE_ABSOLUTE)
+      begin
+          assert(PC == $past(f_abs_address));
+          assert(P == $past(P, 3));
+          assert(S == $past(S, 3));
+          assert(A == $past(A, 3));
+          assert(X == $past(X, 3));
+          assert(Y == $past(Y, 3));
+      end
+
+always @(posedge clk)
+  if (f_past_valid)
+    assume(state != $past(state));
+
+always @(posedge clk)
+  cover(state == STATE_EXECUTE);
+
+
+
+`endif
+
 endmodule
diff --git a/src/mio.verilog b/src/mio.verilog
index dc75c03..6a3d59f 100644
--- a/src/mio.verilog
+++ b/src/mio.verilog
@@ -5,28 +5,59 @@ module mio(clk, i_data, i_addr, i_wr, o_data, o_led);
     input wire [7:0] i_data;
     input wire [15:0] i_addr;
     input wire        i_wr;
+
+    reg [14:0] mem_addr;
+    
+`ifndef VERILOG
+//output wire [7:0]       o_data;
+//wire rst;    
+//wire ce;
+//assign rst = 0;
+//assign ce = 1;
+
+
+`endif
+    
     output logic [7:0] o_data;
     output logic [5:0]  o_led;
+    reg [7:0]           memory [0:32768];
 
-    reg [7:0]           memory [0:65535];
+initial o_led = 6'h3f;
 
+`ifndef FORMAL
 initial $readmemh("foo.hex", memory);
-initial begin
-    memory[32768] <= 8'h00;
-    memory[65532] <= 8'h00;
-    memory[65533] <= 8'h00;
-end;
-
+`else
+    reg f_init_done = 0;
 always @(posedge clk)
-  o_data <= memory[i_addr];
+  begin
+      if (!f_init_done)
+        begin
+            for (integer i = 0; i < 32; i++)
+              begin
+                  memory[i] = $anyconst;
+              end
+            f_init_done <= 1'b1;
+        end
+  end
+`endif
+
+always_comb
+    mem_addr = i_addr[14:0];
 
 always @(posedge clk)
-  o_led <= memory[32768];
+  o_data <= memory[mem_addr];
 
 always @(posedge clk)
   if (i_wr)
     begin
-        memory[i_addr] <= i_data;
+        if (i_addr < 16'h8000)
+        begin
+            memory[mem_addr] <= i_data;
+        end
+        else if (i_addr == 16'h8000)
+        begin
+            o_led <= i_data[5:0];
+        end
     end
 
 endmodule
diff --git a/src/parameters.vh b/src/parameters.vh
index 65e3849..2568536 100644
--- a/src/parameters.vh
+++ b/src/parameters.vh
@@ -1,100 +1,100 @@
 
-parameter ADDR_MODE_IMPLIED = 0;
-parameter ADDR_MODE_IMMEDIATE = 1;
-parameter ADDR_MODE_ABSOLUTE = 2;
-parameter ADDR_MODE_ZP = 3;
-parameter ADDR_MODE_INDEXED_ABSOLUTE = 4;
-parameter ADDR_MODE_INDEXED_ZP = 5;
-parameter ADDR_MODE_INDIRECT = 6;
-parameter ADDR_MODE_PREINDEXED_INDIRECT = 7;
-parameter ADDR_MODE_POSTINDEXED_INDIRECT = 8;
-parameter ADDR_MODE_RELATIVE = 9;
+localparam ADDR_MODE_IMPLIED = 0;
+localparam ADDR_MODE_IMMEDIATE = 1;
+localparam ADDR_MODE_ABSOLUTE = 2;
+localparam ADDR_MODE_ZP = 3;
+localparam ADDR_MODE_INDEXED_ABSOLUTE = 4;
+localparam ADDR_MODE_INDEXED_ZP = 5;
+localparam ADDR_MODE_INDIRECT = 6;
+localparam ADDR_MODE_PREINDEXED_INDIRECT = 7;
+localparam ADDR_MODE_POSTINDEXED_INDIRECT = 8;
+localparam ADDR_MODE_RELATIVE = 9;
 
-parameter OP_OR = 0;
-parameter OP_AND = 1;
-parameter OP_EOR = 2;
-parameter OP_ADC = 3;
-parameter OP_SUB = 4;
-parameter OP_ROT = 5;
-parameter OP_SHF = 6;
+localparam OP_OR = 0;
+localparam OP_AND = 1;
+localparam OP_EOR = 2;
+localparam OP_ADC = 3;
+localparam OP_SUB = 4;
+localparam OP_ROT = 5;
+localparam OP_SHF = 6;
 
-parameter SHIFT_LEFT = 0;
-parameter SHIFT_RIGHT = 1;
+localparam SHIFT_LEFT = 0;
+localparam SHIFT_RIGHT = 1;
 
-parameter I_LDA = 0;
-parameter I_LDX = 1;
-parameter I_LDY = 2;
-parameter I_STA = 3;
-parameter I_STX = 4;
-parameter I_STY = 5;
-parameter I_TAX = 6;
-parameter I_TAY = 7;
-parameter I_TXA = 8;
-parameter I_TYA = 9;
-parameter I_TSX = 10;
-parameter I_TXS = 11;
-parameter I_PHA = 12;
-parameter I_PHP = 13;
-parameter I_PLA = 14;
-parameter I_PLP = 15;
-parameter I_AND = 16;
-parameter I_EOR = 17;
-parameter I_ORA = 18;
-parameter I_BIT = 19;
-parameter I_ADC = 20;
-parameter I_SBC = 21;
-parameter I_CMP = 22;
-parameter I_CPX = 23;
-parameter I_CPY = 24;
-parameter I_INC = 25;
-parameter I_INX = 26;
-parameter I_INY = 27;
-parameter I_DEC = 28;
-parameter I_DEX = 29;
-parameter I_DEY = 30;
-parameter I_ASL = 31;
-parameter I_LSR = 32;
-parameter I_ROL = 33;
-parameter I_ROR = 34;
-parameter I_JMP = 35;
-parameter I_JSR = 36;
-parameter I_RTS = 37;
-parameter I_BCC = 38;
-parameter I_BCS = 39;
-parameter I_BEQ = 40;
-parameter I_BMI = 41;
-parameter I_BNE = 42;
-parameter I_BPL = 43;
-parameter I_BVC = 44;
-parameter I_BVS = 45;
-parameter I_CLC = 46;
-parameter I_CLD = 47;
-parameter I_CLI = 48;
-parameter I_CLV = 49;
-parameter I_SEC = 50;
-parameter I_SED = 51;
-parameter I_SEI = 52;
-parameter I_BRK = 53;
-parameter I_NOP = 54;
-parameter I_RTI = 55;
+localparam I_LDA = 0;
+localparam I_LDX = 1;
+localparam I_LDY = 2;
+localparam I_STA = 3;
+localparam I_STX = 4;
+localparam I_STY = 5;
+localparam I_TAX = 6;
+localparam I_TAY = 7;
+localparam I_TXA = 8;
+localparam I_TYA = 9;
+localparam I_TSX = 10;
+localparam I_TXS = 11;
+localparam I_PHA = 12;
+localparam I_PHP = 13;
+localparam I_PLA = 14;
+localparam I_PLP = 15;
+localparam I_AND = 16;
+localparam I_EOR = 17;
+localparam I_ORA = 18;
+localparam I_BIT = 19;
+localparam I_ADC = 20;
+localparam I_SBC = 21;
+localparam I_CMP = 22;
+localparam I_CPX = 23;
+localparam I_CPY = 24;
+localparam I_INC = 25;
+localparam I_INX = 26;
+localparam I_INY = 27;
+localparam I_DEC = 28;
+localparam I_DEX = 29;
+localparam I_DEY = 30;
+localparam I_ASL = 31;
+localparam I_LSR = 32;
+localparam I_ROL = 33;
+localparam I_ROR = 34;
+localparam I_JMP = 35;
+localparam I_JSR = 36;
+localparam I_RTS = 37;
+localparam I_BCC = 38;
+localparam I_BCS = 39;
+localparam I_BEQ = 40;
+localparam I_BMI = 41;
+localparam I_BNE = 42;
+localparam I_BPL = 43;
+localparam I_BVC = 44;
+localparam I_BVS = 45;
+localparam I_CLC = 46;
+localparam I_CLD = 47;
+localparam I_CLI = 48;
+localparam I_CLV = 49;
+localparam I_SEC = 50;
+localparam I_SED = 51;
+localparam I_SEI = 52;
+localparam I_BRK = 53;
+localparam I_NOP = 54;
+localparam I_RTI = 55;
 
 // Unofficial opcodes
-parameter I_STP = 56;
-parameter I_SHY = 57;
+localparam I_STP = 56;
+localparam I_SHY = 57;
 
 
-parameter P_N = 8'h80;
-parameter P_V = 8'h40;
-parameter P_B = 8'h10;
-parameter P_D = 8'h08;
-parameter P_I = 8'h04;
-parameter P_Z = 8'h02;
-parameter P_C = 8'h01;
+localparam P_N = 7;
+localparam P_V = 6;
+localparam P_B = 5;
+localparam P_D = 3;
+localparam P_I = 2;
+localparam P_Z = 1;
+localparam P_C = 0;
 
 
-parameter DMUX_PC = 3'h0;
-parameter DMUX_A = 3'h1;
-parameter DMUX_X = 3'h2;
-parameter DMUX_Y = 3'h3;
-parameter DMUX_SP = 3'h4;
-parameter DMUX_AUX = 3'h5;
+localparam DMUX_PC = 3'h0;
+localparam DMUX_A = 3'h1;
+localparam DMUX_X = 3'h2;
+localparam DMUX_Y = 3'h3;
+localparam DMUX_SP = 3'h4;
+localparam DMUX_AUX = 3'h5;
diff --git a/src/slon.sby b/src/slon.sby
new file mode 100644
index 0000000..4ae2451
--- /dev/null
+++ b/src/slon.sby
@@ -0,0 +1,32 @@
+[tasks]
+prf
+cvr
+
+[options]
+prf: mode prove
+prf: depth 20
+cvr: mode cover
+cvr: depth 40
+
+[engines]
+smtbmc yices
+
+[script]
+read  -formal decoder.verilog
+read  -formal cpu.verilog
+read  -formal mio.verilog
+read  -formal alu.verilog
+read  -formal dmux.verilog
+read  -formal parameters.vh
+hierarchy -top cpu
+proc -norom
+prep -top cpu
+
+
+[files]
+decoder.verilog
+cpu.verilog
+mio.verilog
+alu.verilog
+dmux.verilog
+parameters.vh
\ No newline at end of file
diff --git a/src/slon_decoder.sby b/src/slon_decoder.sby
new file mode 100644
index 0000000..6ecb25b
--- /dev/null
+++ b/src/slon_decoder.sby
@@ -0,0 +1,24 @@
+[tasks]
+prf
+cvr
+
+[options]
+prf: mode prove
+prf: depth 40
+cvr: mode cover
+cvr: depth 40
+
+[engines]
+smtbmc yices
+
+[script]
+read  -formal decoder.verilog
+read  -formal parameters.vh
+hierarchy -top decoder
+proc -norom
+prep -top decoder
+
+
+[files]
+decoder.verilog
+parameters.vh
\ No newline at end of file