Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: whitequark/Boneless-CPU
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 6fd5f1a863a1
Choose a base ref
...
head repository: whitequark/Boneless-CPU
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 5183ba25153b
Choose a head ref
  • 3 commits
  • 3 files changed
  • 1 contributor

Commits on Dec 24, 2018

  1. Fix JR/JAL immediate width. (Bug found with formal methods!)

    @whitequark
    whitequark committed Dec 24, 2018
    Copy the full SHA
    d36736b View commit details

  2. Fix ADDI not setting flags. (Bug found with formal methods!)

    @whitequark
    whitequark committed Dec 24, 2018
    Copy the full SHA
    f615859 View commit details

  3. Add some delay to pins testbench, now that ADDI/SUBI work properly.

    @whitequark
    whitequark committed Dec 24, 2018
    Copy the full SHA
    5183ba2 View commit details
Showing with 63 additions and 36 deletions.
  1. +45 −17 boneless/gateware/core_fsm.py
  2. +17 −18 formal/formal.sv
  3. +1 −1 formal/run.sh
62 changes: 45 additions & 17 deletions boneless/gateware/core_fsm.py
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
from nmigen.compat import *

from ..opcode import *
from ..instr import *
from .formal import *


@@ -201,19 +202,25 @@ def decode(v):
0b0011: s_v.eq(1),
"default": s_v.eq(0),
}),
fi.flags.eq(Cat(s_z, s_s, s_c, s_v))
]
self.sync += [
If(c_flags,
Cat(r_z, r_s, r_c, r_v).eq(Cat(s_z, s_s, s_c, s_v))
Cat(r_z, r_s, r_c, r_v).eq(Cat(s_z, s_s, s_c, s_v)),
)
]
self.comb += [
If(c_flags,
fi.flags.eq(Cat(s_z, s_s, s_c, s_v)),
).Else(
fi.flags.eq(Cat(r_z, r_s, r_c, r_v)),
)
]

self.submodules.alu = alu = _ALU(width=16)
self.comb += [
alu.s_a.eq(r_opA),
alu.s_b.eq(s_opB),
Case(Cat(i_code1, C(OPCLASS_A, 4)), {
Case(Cat(i_code5), {
OPCODE_LOGIC: Case(i_type2, {
OPTYPE_AND: alu.c_sel.eq(alu.SEL_AND),
OPTYPE_OR: alu.c_sel.eq(alu.SEL_OR),
@@ -223,7 +230,8 @@ def decode(v):
OPTYPE_ADD: alu.c_sel.eq(alu.SEL_ADD),
OPTYPE_SUB: [alu.c_sel.eq(alu.SEL_SUB), s_sub.eq(1)],
OPTYPE_CMP: [alu.c_sel.eq(alu.SEL_SUB), s_cmp.eq(1)],
})
}),
OPCODE_ADDI: alu.c_sel.eq(alu.SEL_ADD),
}),
]

@@ -243,9 +251,11 @@ def decode(v):
NextValue(r_pc, r_pc + 1),
NextState("DECODE/LOAD/JUMP")
)
self.comb += s_insn.eq(Mux(self.fsm.ongoing("DECODE/LOAD/JUMP"), mem_r_d, r_insn))
self.comb += [
s_insn.eq(Mux(self.fsm.ongoing("DECODE/LOAD/JUMP"), mem_r_d, r_insn)),
fi.insn.eq(s_insn),
]
self.fsm.act("DECODE/LOAD/JUMP",
NextValue(fi.insn, mem_r_d),
NextValue(r_insn, mem_r_d),
If(i_clsA,
mem_r_a.eq(Cat(i_regY, r_win)),
@@ -263,10 +273,10 @@ def decode(v):
).Elif(i_clsI,
mem_r_a.eq(Cat(i_regZ, r_win)),
Case(Cat(i_code3, C(OPCLASS_I, 2)), {
OPCODE_MOVL: NextState("I-EXECUTE-MOVx/ADDI"),
OPCODE_MOVH: NextState("I-EXECUTE-MOVx/ADDI"),
OPCODE_MOVA: NextState("I-EXECUTE-MOVx/ADDI"),
OPCODE_ADDI: NextState("I-EXECUTE-MOVx/ADDI"),
OPCODE_MOVL: NextState("I-EXECUTE-MOVx"),
OPCODE_MOVH: NextState("I-EXECUTE-MOVx"),
OPCODE_MOVA: NextState("I-EXECUTE-MOVx"),
OPCODE_ADDI: NextState("I-EXECUTE-ADDI-1"),
OPCODE_LDI: NextState("M/I-LOAD-1"),
OPCODE_STI: NextState("M/I-STORE-1"),
OPCODE_JAL: NextState("I-EXECUTE-JAL"),
@@ -276,6 +286,7 @@ def decode(v):
If(s_cond == i_flag,
NextValue(r_pc, AddSignedImm(r_pc, i_imm11))
),
fi.stb.eq(1),
NextState("FETCH")
)
)
@@ -358,28 +369,41 @@ def decode(v):
fi.stb.eq(1),
NextState("FETCH")
)
self.fsm.act("I-EXECUTE-MOVx/ADDI",
self.fsm.act("I-EXECUTE-MOVx",
mem_w_a.eq(Cat(i_regZ, r_win)),
Case(Cat(i_code2, C(0b0, 1), C(OPCLASS_I, 2)), {
OPCODE_MOVL: mem_w_d.eq(Cat(i_imm8, C(0, 8))),
OPCODE_MOVH: mem_w_d.eq(Cat(C(0, 8), i_imm8)),
OPCODE_MOVA: mem_w_d.eq(AddSignedImm(r_pc, i_imm8)),
OPCODE_ADDI: mem_w_d.eq(AddSignedImm(mem_r_d, i_imm8)),
OPCODE_MOVL: mem_w_d.eq(Cat(i_imm8, C(0, 8))),
OPCODE_MOVH: mem_w_d.eq(Cat(C(0, 8), i_imm8)),
OPCODE_MOVA: mem_w_d.eq(AddSignedImm(r_pc, i_imm8)),
}),
mem_we.eq(1),
fi.stb.eq(1),
NextState("FETCH")
)
self.fsm.act("I-EXECUTE-ADDI-1",
NextValue(r_opA, mem_r_d),
NextState("I-EXECUTE-ADDI-2")
)
self.fsm.act("I-EXECUTE-ADDI-2",
s_opB.eq(Cat(i_imm8, Replicate(i_imm8[7], 8))),
s_res.eq(alu.s_o),
mem_w_a.eq(Cat(i_regZ, r_win)),
mem_w_d.eq(s_res),
mem_we.eq(1),
c_flags.eq(1),
fi.stb.eq(1),
NextState("FETCH")
)
self.fsm.act("I-EXECUTE-JAL",
mem_w_a.eq(Cat(i_regZ, r_win)),
mem_w_d.eq(r_pc),
mem_we.eq(1),
NextValue(r_pc, AddSignedImm(r_pc, i_imm11)),
NextValue(r_pc, AddSignedImm(r_pc, i_imm8)),
fi.stb.eq(1),
NextState("FETCH")
)
self.fsm.act("I-EXECUTE-JR",
NextValue(r_pc, AddSignedImm(mem_r_d, i_imm11)),
NextValue(r_pc, AddSignedImm(mem_r_d, i_imm8)),
fi.stb.eq(1),
NextState("FETCH")
)
@@ -415,6 +439,10 @@ def __init__(self, has_pins=False):
"loop",
STX (R1, R0, 0),
ROT (R1, R1, 1),
MOVH(R2, 1),
"delay",
SUBI(R2, 1),
JNZ ("delay"),
J ("loop"),
])
]
35 changes: 17 additions & 18 deletions formal/formal.sv
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
`define sign(x) ($signed(x) >= 0)
`define sign(x) ($signed(x) < 0)

module boneless_formal(
input clk,
@@ -207,19 +207,19 @@ module boneless_formal(
res = mem[a_regY] + mem[a_regX];
c = res[16];
v = (`sign(mem[a_regY]) == `sign(mem[a_regX])) &&
(`sign(mem[a_regY]) != `sign(res[15]));
(`sign(mem[a_regY]) != res[15]);
end
OPTYPE_SUB: begin
res = mem[a_regY] - mem[a_regX];
c = ~res[16];
v = (`sign(mem[a_regY]) == !`sign(mem[a_regX])) &&
(`sign(mem[a_regY]) != `sign(res[15]));
(`sign(mem[a_regY]) != res[15]);
end
OPTYPE_CMP: begin
res = mem[a_regY] - mem[a_regX];
c = ~res[16];
v = (`sign(mem[a_regY]) == !`sign(mem[a_regX])) &&
(`sign(mem[a_regY]) != `sign(res[15]));
(`sign(mem[a_regY]) != res[15]);
end
endcase
if (i_type2 != 2'b11) begin
@@ -301,19 +301,20 @@ module boneless_formal(
assert (fi_flags == $past(fi_flags));
end
if (i_code5 == OPCODE_ADDI) begin :addi
reg [15:0] tmp;
reg [16:0] res;
reg v;
res = $signed($signed(mem[a_regZ]) + $signed(i_imm8));
v = (`sign(mem[a_regZ]) == `sign(i_imm8)) &&
(`sign(mem[a_regZ]) != `sign(res));
tmp = $signed(i_imm8);
res = mem[a_regZ] + tmp;
v = (`sign(mem[a_regZ]) == tmp[15]) &&
(`sign(mem[a_regZ]) != res[15]);
assert (fi_mem_w_en);
assert (fi_mem_w_addr == a_regZ);
assert (fi_mem_w_data == res[15:0]);
// FIXME: true bug!
// assert (fi_z == (res[15:0] == 0));
// assert (fi_s == res[15]);
// assert (fi_c == res[16]);
// assert (fi_v == v)
assert (fi_z == (res[15:0] == 0));
assert (fi_s == res[15]);
assert (fi_c == res[16]);
assert (fi_v == v);
end
if (i_code5 == OPCODE_LDI) begin
assert (fi_mem_w_en);
@@ -332,16 +333,14 @@ module boneless_formal(
assert (fi_mem_w_addr == a_regZ);
assert (fi_mem_w_data == {$signed(fi_pc) + 16'sd1});
assert (fi_flags == $past(fi_flags));
// FIXME: true bug!
// fs_next_pc <= $signed($signed(fi_pc) + 16'sd1 + $signed(i_imm8));
// fs_jumped <= 1;
fs_next_pc <= $signed($signed(fi_pc) + 16'sd1 + $signed(i_imm8));
fs_jumped <= 1;
end
if (i_code5 == OPCODE_JR) begin
assert (!fi_mem_w_en);
assert (fi_flags == $past(fi_flags));
// FIXME: true bug!
// fs_next_pc <= $signed($signed(mem[a_regZ]) + $signed(i_imm8));
// fs_jumped <= 1;
fs_next_pc <= $signed($signed(mem[a_regZ]) + $signed(i_imm8));
fs_jumped <= 1;
end
if (i_clsC) begin
assert (!fi_mem_w_en);
2 changes: 1 addition & 1 deletion formal/run.sh
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#!/bin/sh
#!/bin/sh -e

cd $(dirname $0)
python3 -W ignore -m boneless.gateware.core_fsm formal generate fsm_core_fi.v