1443 lines
51 KiB
Rust
1443 lines
51 KiB
Rust
// SPDX-License-Identifier: LGPL-3.0-or-later
|
|
// See Notices.txt for copyright information
|
|
|
|
use cpu::{
|
|
config::{CpuConfig, UnitConfig},
|
|
decoder::simple_power_isa::{self, DecodeFilter, DecodeFilterArgs},
|
|
instruction::{AluBranchMOp, MOpRegNum},
|
|
next_pc::CallStackOp,
|
|
register::{FlagsMode, PRegFlags, PRegFlagsPowerISA, PRegFlagsPowerISAView, PRegValue},
|
|
rename_execute_retire::{
|
|
GlobalState, NextPcPredictorOp, to_unit_interfaces::ExecuteToUnitInterfaces,
|
|
},
|
|
test::decode_and_run_single_insn::{
|
|
DecodeAndRunSingleInsnInput, DecodeAndRunSingleInsnOutput, DecodeOneInsnInput,
|
|
DecodeOneInsnMaxMOpCount, decode_and_run_single_insn,
|
|
},
|
|
unit::{RenamedMOpFilter, UnitIO, UnitKind, UnitMOp, UnitTrait},
|
|
util::array_vec::ArrayVec,
|
|
};
|
|
use fayalite::{
|
|
checked_vcd_output,
|
|
firrtl::ExportOptions,
|
|
intern::Memoize,
|
|
module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind, wire_with_loc},
|
|
prelude::*,
|
|
sim::compiler::Compiled,
|
|
ty::StaticType,
|
|
};
|
|
use std::{collections::BTreeSet, num::NonZero, sync::OnceLock};
|
|
|
|
#[hdl_module]
|
|
fn formal_harness(
|
|
config: PhantomConst<CpuConfig>,
|
|
decode_filter: impl DecodeFilter,
|
|
renamed_mop_filter: &mut impl RenamedMOpFilter,
|
|
) {
|
|
#[hdl]
|
|
let cd: ClockDomain = m.input();
|
|
|
|
#[hdl]
|
|
let input: DecodeAndRunSingleInsnInput<
|
|
PhantomConst<CpuConfig>,
|
|
DecodeOneInsnInput<simple_power_isa::decode_one_insn>,
|
|
> = m.input(DecodeAndRunSingleInsnInput[config][StaticType::TYPE]);
|
|
|
|
#[hdl]
|
|
let output: HdlOption<
|
|
DecodeAndRunSingleInsnOutput<
|
|
PhantomConst<CpuConfig>,
|
|
DecodeOneInsnMaxMOpCount<simple_power_isa::decode_one_insn>,
|
|
>,
|
|
> = m.output(HdlOption[DecodeAndRunSingleInsnOutput[config][ConstUsize]]);
|
|
|
|
#[hdl]
|
|
let decode_and_run = instance(decode_and_run_single_insn(
|
|
config,
|
|
simple_power_isa::decode_one_insn(decode_filter),
|
|
));
|
|
connect(decode_and_run.cd, cd);
|
|
#[hdl]
|
|
let need_to_send_input_reg = reg_builder().clock_domain(cd).reset(true);
|
|
#[hdl]
|
|
if need_to_send_input_reg {
|
|
connect(decode_and_run.input.data, HdlSome(input));
|
|
#[hdl]
|
|
if decode_and_run.input.ready {
|
|
connect(need_to_send_input_reg, false);
|
|
}
|
|
} else {
|
|
connect(
|
|
decode_and_run.input.data,
|
|
decode_and_run.ty().input.data.HdlNone(),
|
|
);
|
|
}
|
|
connect(
|
|
decode_and_run.global_state,
|
|
#[hdl]
|
|
GlobalState {
|
|
flags_mode: FlagsMode.PowerISA(
|
|
#[hdl]
|
|
PRegFlagsPowerISA {},
|
|
),
|
|
},
|
|
);
|
|
connect(decode_and_run.output.ready, true);
|
|
connect(output, decode_and_run.output.data);
|
|
for (unit_index, unit) in config.get().units.iter().enumerate() {
|
|
let dyn_unit = unit.kind.unit(config, unit_index, renamed_mop_filter);
|
|
let unit = instance_with_loc(
|
|
&decode_and_run.ty().to_units.unit_field_name(unit_index),
|
|
dyn_unit.module(),
|
|
SourceLocation::caller(),
|
|
);
|
|
let UnitIO {
|
|
cd: unit_cd,
|
|
from_execute: unit_from_execute,
|
|
} = dyn_unit.io(unit);
|
|
connect(
|
|
unit_from_execute,
|
|
ExecuteToUnitInterfaces::unit_fields(decode_and_run.to_units)[unit_index],
|
|
);
|
|
if let Some(unit_cd) = unit_cd {
|
|
connect(unit_cd, cd);
|
|
}
|
|
}
|
|
hdl_assert(cd.clk, !decode_and_run.error, "");
|
|
}
|
|
|
|
#[hdl(no_runtime_generics)]
|
|
type CheckInput =
|
|
DecodeAndRunSingleInsnInput<PhantomConst<CpuConfig>, (UInt<32>, HdlOption<UInt<32>>)>;
|
|
|
|
#[hdl(no_runtime_generics)]
|
|
type CheckOutput = DecodeAndRunSingleInsnOutput<
|
|
PhantomConst<CpuConfig>,
|
|
DecodeOneInsnMaxMOpCount<simple_power_isa::decode_one_insn>,
|
|
>;
|
|
|
|
struct CaseIO {
|
|
input: Expr<CheckInput>,
|
|
suffix: Expr<UInt<32>>,
|
|
output: Expr<CheckOutput>,
|
|
read_output_regs: BTreeSet<u32>,
|
|
}
|
|
|
|
impl CaseIO {
|
|
fn in_reg(&self, reg_num: u32) -> Expr<TraceAsString<PRegValue>> {
|
|
self.input.regs.regs[reg_num as usize]
|
|
}
|
|
fn out_reg(&mut self, reg_num: u32) -> Expr<TraceAsString<PRegValue>> {
|
|
self.read_output_regs.insert(reg_num);
|
|
self.output.regs.regs[reg_num as usize]
|
|
}
|
|
}
|
|
|
|
type CheckFn = fn(clk: Expr<Clock>, io: &mut CaseIO);
|
|
|
|
enum CaseData {
|
|
Unprefixed {
|
|
encoded: u32,
|
|
imm_mask: u32,
|
|
},
|
|
Prefixed {
|
|
encoded: (u32, u32),
|
|
imm_mask: (u32, u32),
|
|
},
|
|
}
|
|
|
|
struct Case {
|
|
data: CaseData,
|
|
asm: &'static str,
|
|
inputs: Vec<u32>,
|
|
check: CheckFn,
|
|
source_location: SourceLocation,
|
|
}
|
|
|
|
impl Case {
|
|
#[track_caller]
|
|
fn mnemonic(&self) -> &'static str {
|
|
self.asm
|
|
.split_whitespace()
|
|
.next()
|
|
.expect("asm should have mnemonic")
|
|
}
|
|
fn needed_mop_kinds(&self) -> NeededMOpKinds {
|
|
#[derive(Clone, Copy, PartialEq, Eq, Hash)]
|
|
struct MyMemoize;
|
|
impl Memoize for MyMemoize {
|
|
type Input = (u32, Option<u32>);
|
|
type InputOwned = (u32, Option<u32>);
|
|
type Output = NeededMOpKinds;
|
|
|
|
fn inner(self, input: &Self::Input) -> Self::Output {
|
|
let (first_input, second_input) = *input;
|
|
static COMPILED: OnceLock<Compiled<simple_power_isa::decode_one_insn>> =
|
|
OnceLock::new();
|
|
let compiled =
|
|
*COMPILED.get_or_init(|| Compiled::new(simple_power_isa::decode_one_insn(())));
|
|
let mut sim = Simulation::from_compiled(compiled);
|
|
sim.write(sim.io().first_input, first_input);
|
|
sim.write(sim.io().second_input, second_input);
|
|
sim.advance_time(SimDuration::from_micros(1));
|
|
assert_eq!(
|
|
sim.read_bool(sim.io().second_input_used),
|
|
second_input.is_some(),
|
|
);
|
|
assert!(!sim.read_bool(sim.io().is_illegal));
|
|
let mut retval = NeededMOpKinds::default();
|
|
for mop in ArrayVec::elements_sim_ref(&sim.read(sim.io().output)) {
|
|
retval = retval.or(NeededMOpKinds::new(mop.inner()));
|
|
}
|
|
retval
|
|
}
|
|
}
|
|
const IMM_BITS: u32 = 0xAAAA_AAAA; // something non-zero so we avoid special cases for zero immediates or similar
|
|
let input = match self.data {
|
|
CaseData::Unprefixed { encoded, imm_mask } => (encoded | (IMM_BITS & imm_mask), None),
|
|
CaseData::Prefixed {
|
|
encoded: (encoded_prefix, encoded_suffix),
|
|
imm_mask: (imm_mask_prefix, imm_mask_suffix),
|
|
} => (
|
|
encoded_prefix | (IMM_BITS & imm_mask_prefix),
|
|
Some(encoded_suffix | (IMM_BITS & imm_mask_suffix)),
|
|
),
|
|
};
|
|
MyMemoize.get_owned(input)
|
|
}
|
|
}
|
|
|
|
#[derive(Copy, Clone, PartialEq, Eq, Debug, Default)]
|
|
struct NeededMOpKinds {
|
|
need_add_sub: bool,
|
|
need_add_sub_i: bool,
|
|
need_logical_flags: bool,
|
|
need_logical: bool,
|
|
need_logical_i: bool,
|
|
need_shift_rotate: bool,
|
|
need_compare: bool,
|
|
need_compare_i: bool,
|
|
need_branch: bool,
|
|
need_branch_i: bool,
|
|
need_read_special: bool,
|
|
}
|
|
|
|
impl NeededMOpKinds {
|
|
fn or(self, other: Self) -> Self {
|
|
Self {
|
|
need_add_sub: self.need_add_sub | other.need_add_sub,
|
|
need_add_sub_i: self.need_add_sub_i | other.need_add_sub_i,
|
|
need_logical_flags: self.need_logical_flags | other.need_logical_flags,
|
|
need_logical: self.need_logical | other.need_logical,
|
|
need_logical_i: self.need_logical_i | other.need_logical_i,
|
|
need_shift_rotate: self.need_shift_rotate | other.need_shift_rotate,
|
|
need_compare: self.need_compare | other.need_compare,
|
|
need_compare_i: self.need_compare_i | other.need_compare_i,
|
|
need_branch: self.need_branch | other.need_branch,
|
|
need_branch_i: self.need_branch_i | other.need_branch_i,
|
|
need_read_special: self.need_read_special | other.need_read_special,
|
|
}
|
|
}
|
|
#[hdl]
|
|
fn new(mop: &SimValue<UnitMOp<impl Type, impl Type, impl Type>>) -> Self {
|
|
#[hdl(sim)]
|
|
match mop {
|
|
UnitMOp::<_, _, _>::AluBranch(mop) =>
|
|
{
|
|
#[hdl(sim)]
|
|
match mop {
|
|
AluBranchMOp::<_, _>::AddSub(_) => Self {
|
|
need_add_sub: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::AddSubI(_) => Self {
|
|
need_add_sub_i: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::LogicalFlags(_) => Self {
|
|
need_logical_flags: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::Logical(_) => Self {
|
|
need_logical: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::LogicalI(_) => Self {
|
|
need_logical_i: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::ShiftRotate(_) => Self {
|
|
need_shift_rotate: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::Compare(_) => Self {
|
|
need_compare: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::CompareI(_) => Self {
|
|
need_compare_i: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::Branch(_) => Self {
|
|
need_branch: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::BranchI(_) => Self {
|
|
need_branch_i: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::ReadSpecial(_) => Self {
|
|
need_read_special: true,
|
|
..Self::default()
|
|
},
|
|
AluBranchMOp::<_, _>::Unknown => unreachable!(),
|
|
}
|
|
}
|
|
UnitMOp::<_, _, _>::TransformedMove(_) => {
|
|
// removed by rename stage
|
|
Self::default()
|
|
}
|
|
UnitMOp::<_, _, _>::LoadStore(mop) => {
|
|
todo!("{mop:?}")
|
|
}
|
|
UnitMOp::<_, _, _>::Unknown => unreachable!(),
|
|
}
|
|
}
|
|
}
|
|
|
|
#[derive(Default)]
|
|
struct Cases {
|
|
cases: Vec<Case>,
|
|
}
|
|
|
|
impl Cases {
|
|
fn mnemonics(&self) -> BTreeSet<&'static str> {
|
|
BTreeSet::from_iter(self.cases.iter().map(|c| c.mnemonic()))
|
|
}
|
|
fn needed_mop_kinds(&self) -> NeededMOpKinds {
|
|
let mut retval = NeededMOpKinds::default();
|
|
for case in &self.cases {
|
|
retval = retval.or(case.needed_mop_kinds());
|
|
}
|
|
retval
|
|
}
|
|
#[track_caller]
|
|
fn add(
|
|
&mut self,
|
|
asm: &'static str,
|
|
encoded: u32,
|
|
imm_mask: u32,
|
|
inputs: impl AsRef<[u32]>,
|
|
check: CheckFn,
|
|
) {
|
|
self.cases.push(Case {
|
|
data: CaseData::Unprefixed { encoded, imm_mask },
|
|
asm,
|
|
inputs: inputs.as_ref().to_vec(),
|
|
check,
|
|
source_location: SourceLocation::caller(),
|
|
});
|
|
}
|
|
#[track_caller]
|
|
fn add_prefixed(
|
|
&mut self,
|
|
asm: &'static str,
|
|
encoded: (u32, u32),
|
|
imm_mask: (u32, u32),
|
|
inputs: impl AsRef<[u32]>,
|
|
check: CheckFn,
|
|
) {
|
|
self.cases.push(Case {
|
|
data: CaseData::Prefixed { encoded, imm_mask },
|
|
asm,
|
|
inputs: inputs.as_ref().to_vec(),
|
|
check,
|
|
source_location: SourceLocation::caller(),
|
|
});
|
|
}
|
|
fn subdivide(self, subdivision_index: usize, subdivision_count: usize) -> Self {
|
|
let Self { mut cases } = self;
|
|
let start_index = (subdivision_index * cases.len()) / subdivision_count;
|
|
let end_index = ((subdivision_index + 1) * cases.len()) / subdivision_count;
|
|
cases.truncate(end_index);
|
|
cases.drain(..start_index);
|
|
Self { cases }
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_addi(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
cases.add("addi 3, 4, imm", 0x3864_0000, 0xFFFF, [r4], check_addi);
|
|
#[hdl]
|
|
fn check_addi(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
#[hdl]
|
|
let addi_imm = wire();
|
|
connect(addi_imm, io.suffix.cast_to_static::<SInt<16>>());
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
|
|
hdl_assert(
|
|
clk,
|
|
(r4_in + addi_imm.cast_to_static::<UInt<64>>())
|
|
.cast_to_static::<UInt<64>>()
|
|
.cmp_eq(r3_out),
|
|
"",
|
|
);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_paddi(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
cases.add_prefixed(
|
|
"paddi 3, 4, imm, 0",
|
|
(0x0600_0000, 0x3864_0000),
|
|
(0x0003_FFFF, 0x0000_FFFF),
|
|
[r4],
|
|
check_paddi::<false>,
|
|
);
|
|
cases.add_prefixed(
|
|
"paddi 3, 4, imm, 1",
|
|
(0x0610_0000, 0x3864_0000),
|
|
(0x0003_FFFF, 0x0000_FFFF),
|
|
[r4],
|
|
check_paddi::<true>,
|
|
);
|
|
#[hdl]
|
|
fn check_paddi<const R: bool>(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
#[hdl]
|
|
let paddi_imm: SInt<34> = wire();
|
|
connect(
|
|
paddi_imm,
|
|
(io.suffix[..16] | (io.input.decoder_input.0[..18] << 16)).cast_to_static::<SInt<34>>(),
|
|
);
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
|
|
let sum = r4_in + paddi_imm.cast_to_static::<UInt<64>>();
|
|
let sum = if R { sum + io.input.pc } else { sum };
|
|
hdl_assert(clk, sum.cast_to_static::<UInt<64>>().cmp_eq(r3_out), "");
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_addis(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
cases.add("addis 3, 4, imm", 0x3C64_0000, 0xFFFF, [r4], check_addis);
|
|
#[hdl]
|
|
fn check_addis(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
#[hdl]
|
|
let addis_imm = wire();
|
|
connect(addis_imm, io.suffix.cast_to_static::<SInt<16>>());
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
|
|
hdl_assert(
|
|
clk,
|
|
(r4_in + (addis_imm << 16).cast_to_static::<UInt<64>>())
|
|
.cast_to_static::<UInt<64>>()
|
|
.cmp_eq(r3_out),
|
|
"",
|
|
);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_addpcis(cases: &mut Cases) {
|
|
cases.add("addpcis 3, imm", 0x4C60_0004, 0x1F_FFC1, [], check_addpcis);
|
|
#[hdl]
|
|
fn check_addpcis(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
#[hdl]
|
|
let addpcis_d0 = wire();
|
|
connect(addpcis_d0, io.suffix[6..].cast_to_static::<UInt<10>>());
|
|
#[hdl]
|
|
let addpcis_d1 = wire();
|
|
connect(addpcis_d1, io.suffix[16..].cast_to_static::<UInt<5>>());
|
|
#[hdl]
|
|
let addpcis_d2 = wire();
|
|
connect(addpcis_d2, io.suffix.cast_to_static::<UInt<1>>());
|
|
#[hdl]
|
|
let addpcis_d = wire();
|
|
connect(
|
|
addpcis_d,
|
|
(addpcis_d2 + (addpcis_d1 << 1) + (addpcis_d0 << 6)).cast_to_static::<SInt<16>>(),
|
|
);
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
|
|
hdl_assert(
|
|
clk,
|
|
(io.input.pc + 4u64 + (addpcis_d << 16).cast_to_static::<UInt<64>>())
|
|
.cast_to_static::<UInt<64>>()
|
|
.cmp_eq(r3_out),
|
|
"",
|
|
);
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_add_addc_adde_subf_subfc_subfe(cases: &mut Cases) {
|
|
let r3 = MOpRegNum::power_isa_gpr_reg_num(3);
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
let ca = MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM;
|
|
cases.add("add 3, 3, 4", 0x7C63_2214, 0, [r3, r4], check);
|
|
cases.add("add. 3, 3, 4", 0x7C63_2215, 0, [r3, r4], check);
|
|
cases.add("addo 3, 3, 4", 0x7C63_2614, 0, [r3, r4], check);
|
|
cases.add("addo. 3, 3, 4", 0x7C63_2615, 0, [r3, r4], check);
|
|
cases.add("addc 3, 3, 4", 0x7C63_2014, 0, [r3, r4], check);
|
|
cases.add("addc. 3, 3, 4", 0x7C63_2015, 0, [r3, r4], check);
|
|
cases.add("addco 3, 3, 4", 0x7C63_2414, 0, [r3, r4], check);
|
|
cases.add("addco. 3, 3, 4", 0x7C63_2415, 0, [r3, r4], check);
|
|
cases.add("adde 3, 3, 4", 0x7C63_2114, 0, [r3, r4, ca], check);
|
|
cases.add("adde. 3, 3, 4", 0x7C63_2115, 0, [r3, r4, ca], check);
|
|
cases.add("addeo 3, 3, 4", 0x7C63_2514, 0, [r3, r4, ca], check);
|
|
cases.add("addeo. 3, 3, 4", 0x7C63_2515, 0, [r3, r4, ca], check);
|
|
cases.add("subf 3, 3, 4", 0x7C63_2050, 0, [r3, r4], check);
|
|
cases.add("subf. 3, 3, 4", 0x7C63_2051, 0, [r3, r4], check);
|
|
cases.add("subfo 3, 3, 4", 0x7C63_2450, 0, [r3, r4], check);
|
|
cases.add("subfo. 3, 3, 4", 0x7C63_2451, 0, [r3, r4], check);
|
|
cases.add("subfc 3, 3, 4", 0x7C63_2010, 0, [r3, r4], check);
|
|
cases.add("subfc. 3, 3, 4", 0x7C63_2011, 0, [r3, r4], check);
|
|
cases.add("subfco 3, 3, 4", 0x7C63_2410, 0, [r3, r4], check);
|
|
cases.add("subfco. 3, 3, 4", 0x7C63_2411, 0, [r3, r4], check);
|
|
cases.add("subfe 3, 3, 4", 0x7C63_2110, 0, [r3, r4, ca], check);
|
|
cases.add("subfe. 3, 3, 4", 0x7C63_2111, 0, [r3, r4, ca], check);
|
|
cases.add("subfeo 3, 3, 4", 0x7C63_2510, 0, [r3, r4, ca], check);
|
|
cases.add("subfeo. 3, 3, 4", 0x7C63_2511, 0, [r3, r4, ca], check);
|
|
#[hdl]
|
|
fn check(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
let has_ca_out = (io.suffix & 0x240u32).cmp_eq(0u32);
|
|
let oe = (io.suffix & 0x400u32).cmp_ne(0u32);
|
|
let use_ca_in = (io.suffix & 0x100u32).cmp_ne(0u32);
|
|
let is_sub = (io.suffix & 0x4u32).cmp_eq(0u32);
|
|
let rc = (io.suffix & 1u32).cmp_ne(0u32);
|
|
let r3_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(3)).int_fp;
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let ca_in = io.in_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
|
|
let ov_in = io.in_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
|
|
let ca_out = io.out_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
|
|
let ov_out = io.out_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
#[hdl]
|
|
let add_sub_add_in0 = wire();
|
|
connect(add_sub_add_in0, r3_in);
|
|
#[hdl]
|
|
let add_sub_ca_in = wire();
|
|
connect(add_sub_ca_in, is_sub.cast_to_static::<UInt<1>>());
|
|
#[hdl]
|
|
if is_sub {
|
|
connect(add_sub_add_in0, !r3_in);
|
|
}
|
|
#[hdl]
|
|
if use_ca_in {
|
|
connect(
|
|
add_sub_ca_in,
|
|
PRegFlags::view::<PRegFlagsPowerISA>(ca_in.flags)
|
|
.xer_ca
|
|
.cast_to_static::<UInt<1>>(),
|
|
);
|
|
}
|
|
#[hdl]
|
|
let add_sub_expected_out = wire(r3_out.ty());
|
|
let PRegFlagsPowerISAView {
|
|
unused: _,
|
|
xer_ca,
|
|
xer_ca32,
|
|
xer_ov,
|
|
xer_ov32,
|
|
cr_lt,
|
|
cr_gt,
|
|
cr_eq,
|
|
so,
|
|
..
|
|
} = PRegFlags::view::<PRegFlagsPowerISA>(add_sub_expected_out.flags);
|
|
let add_sub_add_in0_s = add_sub_add_in0.cast_to_static::<SInt<64>>();
|
|
let r4_s = r4_in.cast_to_static::<SInt<64>>();
|
|
let u64_sum = add_sub_add_in0 + r4_in + add_sub_ca_in;
|
|
let s64_sum = add_sub_add_in0_s + r4_s + add_sub_ca_in.cast_to(SInt[2]);
|
|
let u32_sum = add_sub_add_in0.cast_to(UInt[32]) + r4_in.cast_to(UInt[32]) + add_sub_ca_in;
|
|
let s32_sum = add_sub_add_in0.cast_to(SInt[32])
|
|
+ r4_in.cast_to(SInt[32])
|
|
+ add_sub_ca_in.cast_to(SInt[2]);
|
|
let sum_as_s64 = u64_sum.cast_to(SInt[64]);
|
|
connect(
|
|
add_sub_expected_out.int_fp,
|
|
u64_sum.cast_to_static::<UInt<64>>(),
|
|
);
|
|
connect(xer_ca, u64_sum[64]);
|
|
connect(xer_ca32, u32_sum[32]);
|
|
connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
|
|
connect(
|
|
xer_ov32,
|
|
s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
|
|
);
|
|
connect(cr_gt, sum_as_s64.cmp_gt(0i64));
|
|
connect(cr_lt, sum_as_s64.cmp_lt(0i64));
|
|
connect(cr_eq, sum_as_s64.cmp_eq(0i64));
|
|
connect(so, xer_ov); // TODO: also propagate from input SO
|
|
|
|
hdl_assert(clk, add_sub_expected_out.cmp_eq(r3_out), "");
|
|
|
|
#[hdl]
|
|
if has_ca_out {
|
|
hdl_assert(clk, add_sub_expected_out.cmp_eq(ca_out), "");
|
|
} else {
|
|
hdl_assert(clk, ca_in.cmp_eq(ca_out), "");
|
|
}
|
|
|
|
#[hdl]
|
|
if oe {
|
|
hdl_assert(clk, add_sub_expected_out.cmp_eq(ov_out), "");
|
|
} else {
|
|
hdl_assert(clk, ov_in.cmp_eq(ov_out), "");
|
|
}
|
|
|
|
#[hdl]
|
|
if rc {
|
|
hdl_assert(clk, add_sub_expected_out.cmp_eq(cr0_out), "");
|
|
} else {
|
|
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_addme_addze_subfme_subfze(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
let ca = MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM;
|
|
cases.add("addme 3, 4", 0x7C64_01D4, 0, [r4, ca], check);
|
|
cases.add("addmeo 3, 4", 0x7C64_05D4, 0, [r4, ca], check);
|
|
cases.add("addme. 3, 4", 0x7C64_01D5, 0, [r4, ca], check);
|
|
cases.add("addmeo. 3, 4", 0x7C64_05D5, 0, [r4, ca], check);
|
|
cases.add("addze 3, 4", 0x7C64_0194, 0, [r4, ca], check);
|
|
cases.add("addzeo 3, 4", 0x7C64_0594, 0, [r4, ca], check);
|
|
cases.add("addze. 3, 4", 0x7C64_0195, 0, [r4, ca], check);
|
|
cases.add("addzeo. 3, 4", 0x7C64_0595, 0, [r4, ca], check);
|
|
cases.add("subfme 3, 4", 0x7C64_01D0, 0, [r4, ca], check);
|
|
cases.add("subfmeo 3, 4", 0x7C64_05D0, 0, [r4, ca], check);
|
|
cases.add("subfme. 3, 4", 0x7C64_01D1, 0, [r4, ca], check);
|
|
cases.add("subfmeo. 3, 4", 0x7C64_05D1, 0, [r4, ca], check);
|
|
cases.add("subfze 3, 4", 0x7C64_0190, 0, [r4, ca], check);
|
|
cases.add("subfzeo 3, 4", 0x7C64_0590, 0, [r4, ca], check);
|
|
cases.add("subfze. 3, 4", 0x7C64_0191, 0, [r4, ca], check);
|
|
cases.add("subfzeo. 3, 4", 0x7C64_0591, 0, [r4, ca], check);
|
|
#[hdl]
|
|
fn check(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
let rhs_is_ones = (io.suffix & 0x40u32).cmp_ne(0u32);
|
|
let oe = (io.suffix & 0x400u32).cmp_ne(0u32);
|
|
let is_sub = (io.suffix & 0x4u32).cmp_eq(0u32);
|
|
let rc = (io.suffix & 1u32).cmp_ne(0u32);
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let ca_in = io.in_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
|
|
let ov_in = io.in_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
|
|
let ca_out = io.out_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
|
|
let ov_out = io.out_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
#[hdl]
|
|
let addmze_subfmze_add_in0 = wire();
|
|
let in0 = addmze_subfmze_add_in0;
|
|
connect(in0, r4_in);
|
|
#[hdl]
|
|
if is_sub {
|
|
connect(in0, !r4_in);
|
|
}
|
|
#[hdl]
|
|
let addmze_subfmze_add_in1 = wire();
|
|
let in1 = addmze_subfmze_add_in1;
|
|
connect(
|
|
in1,
|
|
rhs_is_ones.cast_to(SInt[1]).cast_to_static::<UInt<64>>(),
|
|
);
|
|
let add_sub_ca_in = PRegFlags::view::<PRegFlagsPowerISA>(ca_in.flags)
|
|
.xer_ca
|
|
.cast_to_static::<UInt<1>>();
|
|
#[hdl]
|
|
let addmze_subfmze_expected_out = wire(r3_out.ty());
|
|
let PRegFlagsPowerISAView {
|
|
unused: _,
|
|
xer_ca,
|
|
xer_ca32,
|
|
xer_ov,
|
|
xer_ov32,
|
|
cr_lt,
|
|
cr_gt,
|
|
cr_eq,
|
|
so,
|
|
..
|
|
} = PRegFlags::view::<PRegFlagsPowerISA>(addmze_subfmze_expected_out.flags);
|
|
let in0_s = in0.cast_to_static::<SInt<64>>();
|
|
let in1_s = in1.cast_to_static::<SInt<64>>();
|
|
let u64_sum = in0 + in1 + add_sub_ca_in;
|
|
let s64_sum = in0_s + in1_s + add_sub_ca_in.cast_to(SInt[2]);
|
|
let u32_sum = in0.cast_to(UInt[32]) + in1.cast_to(UInt[32]) + add_sub_ca_in;
|
|
let s32_sum =
|
|
in0.cast_to(SInt[32]) + in1.cast_to(SInt[32]) + add_sub_ca_in.cast_to(SInt[2]);
|
|
let sum_as_s64 = u64_sum.cast_to(SInt[64]);
|
|
connect(
|
|
addmze_subfmze_expected_out.int_fp,
|
|
u64_sum.cast_to_static::<UInt<64>>(),
|
|
);
|
|
connect(xer_ca, u64_sum[64]);
|
|
connect(xer_ca32, u32_sum[32]);
|
|
connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
|
|
connect(
|
|
xer_ov32,
|
|
s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
|
|
);
|
|
connect(cr_gt, sum_as_s64.cmp_gt(0i64));
|
|
connect(cr_lt, sum_as_s64.cmp_lt(0i64));
|
|
connect(cr_eq, sum_as_s64.cmp_eq(0i64));
|
|
connect(so, xer_ov); // TODO: also propagate from input SO
|
|
|
|
hdl_assert(clk, addmze_subfmze_expected_out.cmp_eq(r3_out), "");
|
|
hdl_assert(clk, addmze_subfmze_expected_out.cmp_eq(ca_out), "");
|
|
|
|
#[hdl]
|
|
if oe {
|
|
hdl_assert(clk, addmze_subfmze_expected_out.cmp_eq(ov_out), "");
|
|
} else {
|
|
hdl_assert(clk, ov_in.cmp_eq(ov_out), "");
|
|
}
|
|
|
|
#[hdl]
|
|
if rc {
|
|
hdl_assert(clk, addmze_subfmze_expected_out.cmp_eq(cr0_out), "");
|
|
} else {
|
|
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_addic_subfic(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
cases.add("addic 3, 4, imm", 0x3064_0000, 0xFFFF, [r4], check);
|
|
cases.add("addic. 3, 4, imm", 0x3464_0000, 0xFFFF, [r4], check);
|
|
cases.add("subfic 3, 4, imm", 0x2064_0000, 0xFFFF, [r4], check);
|
|
#[hdl]
|
|
fn check(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
let rc = (io.suffix & 0x400_0000u32).cmp_ne(0u32);
|
|
let is_sub = (io.suffix & 0x1000_0000u32).cmp_eq(0u32);
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
|
|
let ca_out = io.out_reg(MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM);
|
|
let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
#[hdl]
|
|
let addic_subfic_imm = wire();
|
|
connect(addic_subfic_imm, io.suffix.cast_to_static::<SInt<16>>());
|
|
#[hdl]
|
|
let addic_subfic_in = wire();
|
|
connect(addic_subfic_in, r4_in);
|
|
#[hdl]
|
|
if is_sub {
|
|
connect(addic_subfic_in, !r4_in);
|
|
}
|
|
#[hdl]
|
|
let addic_subfic_expected_out = wire(r3_out.ty());
|
|
connect_any(
|
|
addic_subfic_expected_out.int_fp,
|
|
addic_subfic_in + addic_subfic_imm.cast_to(UInt[64]) + is_sub.cast_to(UInt[1]),
|
|
);
|
|
let PRegFlagsPowerISAView {
|
|
unused: _,
|
|
xer_ca,
|
|
xer_ca32,
|
|
xer_ov,
|
|
xer_ov32,
|
|
cr_lt,
|
|
cr_gt,
|
|
cr_eq,
|
|
so,
|
|
..
|
|
} = PRegFlags::view::<PRegFlagsPowerISA>(addic_subfic_expected_out.flags);
|
|
let addic_subfic_in_s = addic_subfic_in.cast_to_static::<SInt<64>>();
|
|
let u64_sum =
|
|
addic_subfic_in + addic_subfic_imm.cast_to(UInt[64]) + is_sub.cast_to(UInt[1]);
|
|
let s64_sum =
|
|
addic_subfic_in_s + addic_subfic_imm + is_sub.cast_to(UInt[1]).cast_to(SInt[64]);
|
|
let u32_sum = addic_subfic_in.cast_to(UInt[32])
|
|
+ addic_subfic_imm.cast_to(UInt[32])
|
|
+ is_sub.cast_to(UInt[1]);
|
|
let s32_sum = addic_subfic_in.cast_to(SInt[32])
|
|
+ addic_subfic_imm.cast_to(SInt[32])
|
|
+ is_sub.cast_to(UInt[1]).cast_to(SInt[32]);
|
|
let sum_as_s64 = u64_sum.cast_to(SInt[64]);
|
|
connect(xer_ca, u64_sum[64]);
|
|
connect(xer_ca32, u32_sum[32]);
|
|
connect(xer_ov, s64_sum.cmp_lt(i64::MIN) | s64_sum.cmp_gt(i64::MAX));
|
|
connect(
|
|
xer_ov32,
|
|
s32_sum.cmp_lt(i32::MIN) | s32_sum.cmp_gt(i32::MAX),
|
|
);
|
|
connect(cr_gt, sum_as_s64.cmp_gt(0i64));
|
|
connect(cr_lt, sum_as_s64.cmp_lt(0i64));
|
|
connect(cr_eq, sum_as_s64.cmp_eq(0i64));
|
|
connect(so, xer_ov); // TODO: also propagate from input SO
|
|
|
|
hdl_assert(clk, addic_subfic_expected_out.cmp_eq(r3_out), "");
|
|
hdl_assert(clk, addic_subfic_expected_out.cmp_eq(ca_out), "");
|
|
|
|
#[hdl]
|
|
if rc {
|
|
hdl_assert(clk, addic_subfic_expected_out.cmp_eq(cr0_out), "");
|
|
} else {
|
|
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl]
|
|
fn case_check_neg(cases: &mut Cases) {
|
|
let r4 = MOpRegNum::power_isa_gpr_reg_num(4);
|
|
cases.add("neg 3, 4", 0x7C64_00D0, 0, [r4], check);
|
|
cases.add("nego 3, 4", 0x7C64_04D0, 0, [r4], check);
|
|
cases.add("neg. 3, 4", 0x7C64_00D1, 0, [r4], check);
|
|
cases.add("nego. 3, 4", 0x7C64_04D1, 0, [r4], check);
|
|
#[hdl]
|
|
fn check(clk: Expr<Clock>, io: &mut CaseIO) {
|
|
let oe = (io.suffix & 0x400u32).cmp_ne(0u32);
|
|
let rc = (io.suffix & 1u32).cmp_ne(0u32);
|
|
let r4_in = io.in_reg(MOpRegNum::power_isa_gpr_reg_num(4)).int_fp;
|
|
let ov_in = io.in_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_in = io.in_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
let r3_out = io.out_reg(MOpRegNum::power_isa_gpr_reg_num(3));
|
|
let ov_out = io.out_reg(MOpRegNum::POWER_ISA_XER_SO_OV_OV32_REG_NUM);
|
|
let cr0_out = io.out_reg(MOpRegNum::POWER_ISA_CR_0_REG_NUM);
|
|
#[hdl]
|
|
let neg_expected_out = wire(r3_out.ty());
|
|
let PRegFlagsPowerISAView {
|
|
unused: _,
|
|
xer_ca,
|
|
xer_ca32,
|
|
xer_ov,
|
|
xer_ov32,
|
|
cr_lt,
|
|
cr_gt,
|
|
cr_eq,
|
|
so,
|
|
..
|
|
} = PRegFlags::view::<PRegFlagsPowerISA>(neg_expected_out.flags);
|
|
let out_s = neg_expected_out.int_fp.cast_to_static::<SInt<64>>();
|
|
connect(
|
|
neg_expected_out.int_fp,
|
|
(-r4_in.cast_to_static::<SInt<64>>()).cast_to_static::<UInt<64>>(),
|
|
);
|
|
connect(xer_ca, r4_in.cmp_eq(0u64));
|
|
connect(xer_ca32, r4_in.cast_to_static::<UInt<32>>().cmp_eq(0u32));
|
|
connect(xer_ov, r4_in.cmp_eq(i64::MIN.cast_unsigned()));
|
|
connect(
|
|
xer_ov32,
|
|
r4_in
|
|
.cast_to_static::<UInt<32>>()
|
|
.cmp_eq(i32::MIN.cast_unsigned()),
|
|
);
|
|
connect(cr_gt, out_s.cmp_gt(0i64));
|
|
connect(cr_lt, out_s.cmp_lt(0i64));
|
|
connect(cr_eq, out_s.cmp_eq(0i64));
|
|
connect(so, xer_ov); // TODO: also propagate from input SO
|
|
|
|
hdl_assert(clk, neg_expected_out.cmp_eq(r3_out), "");
|
|
|
|
#[hdl]
|
|
if oe {
|
|
hdl_assert(clk, neg_expected_out.cmp_eq(ov_out), "");
|
|
} else {
|
|
hdl_assert(clk, ov_in.cmp_eq(ov_out), "");
|
|
}
|
|
|
|
#[hdl]
|
|
if rc {
|
|
hdl_assert(clk, neg_expected_out.cmp_eq(cr0_out), "");
|
|
} else {
|
|
hdl_assert(clk, cr0_in.cmp_eq(cr0_out), "");
|
|
}
|
|
}
|
|
}
|
|
|
|
fn cases_add_sub() -> Cases {
|
|
let mut cases = Cases::default();
|
|
case_check_addi(&mut cases);
|
|
case_check_paddi(&mut cases);
|
|
case_check_addis(&mut cases);
|
|
case_check_addpcis(&mut cases);
|
|
case_check_add_addc_adde_subf_subfc_subfe(&mut cases);
|
|
case_check_addic_subfic(&mut cases);
|
|
case_check_addme_addze_subfme_subfze(&mut cases);
|
|
// TODO: addex -- not implemented in decoder::simple_power_isa
|
|
case_check_neg(&mut cases);
|
|
cases
|
|
}
|
|
|
|
#[derive(Copy, Clone)]
|
|
struct AnyConsts {
|
|
decoder_first_word_any_const: Expr<UInt<32>>,
|
|
decoder_has_second_word_any_const: Expr<Bool>,
|
|
decoder_second_word_any_const: Expr<UInt<32>>,
|
|
r3_any_const: Expr<UInt<64>>,
|
|
r4_any_const: Expr<UInt<64>>,
|
|
ca_any_const: Expr<Bool>,
|
|
pc_any_const: Expr<UInt<64>>,
|
|
predicted_next_pc_any_const: Expr<UInt<64>>,
|
|
}
|
|
|
|
impl AnyConsts {
|
|
#[track_caller]
|
|
fn new() -> Self {
|
|
Self {
|
|
decoder_first_word_any_const: any_const(StaticType::TYPE),
|
|
decoder_has_second_word_any_const: any_const(StaticType::TYPE),
|
|
decoder_second_word_any_const: any_const(StaticType::TYPE),
|
|
r3_any_const: any_const(StaticType::TYPE),
|
|
r4_any_const: any_const(StaticType::TYPE),
|
|
ca_any_const: any_const(StaticType::TYPE),
|
|
pc_any_const: any_const(StaticType::TYPE),
|
|
predicted_next_pc_any_const: any_const(StaticType::TYPE),
|
|
}
|
|
}
|
|
}
|
|
|
|
#[hdl_module]
|
|
fn check_power_isa_alu_formal(
|
|
config: PhantomConst<CpuConfig>,
|
|
cases: &Cases,
|
|
any_consts: Option<AnyConsts>,
|
|
) {
|
|
#[hdl]
|
|
let ran: Bool = m.output();
|
|
#[hdl]
|
|
let cd = wire();
|
|
connect(
|
|
cd,
|
|
#[hdl]
|
|
ClockDomain {
|
|
clk: formal_global_clock(),
|
|
rst: formal_reset().to_reset(),
|
|
},
|
|
);
|
|
let mnemonics = cases.mnemonics();
|
|
let needed_mop_kinds = cases.needed_mop_kinds();
|
|
#[hdl]
|
|
let harness = instance(formal_harness(
|
|
config,
|
|
|args: &DecodeFilterArgs<'_>| mnemonics.contains(&args.mnemonic()),
|
|
&mut |mop: &SimValue<_>| -> bool {
|
|
needed_mop_kinds == needed_mop_kinds.or(NeededMOpKinds::new(mop))
|
|
},
|
|
));
|
|
connect(harness.cd, cd);
|
|
#[hdl]
|
|
let ran_reg = reg_builder().clock_domain(cd).reset(false);
|
|
connect(ran, ran_reg);
|
|
#[hdl]
|
|
let cycle_count = reg_builder().clock_domain(cd).reset(0u32);
|
|
connect_any(cycle_count, cycle_count + 1u32);
|
|
#[hdl]
|
|
if cycle_count.cmp_ge(5u32) {
|
|
hdl_assert(cd.clk, ran, "");
|
|
}
|
|
let AnyConsts {
|
|
decoder_first_word_any_const,
|
|
decoder_has_second_word_any_const,
|
|
decoder_second_word_any_const,
|
|
r3_any_const,
|
|
r4_any_const,
|
|
ca_any_const,
|
|
pc_any_const,
|
|
predicted_next_pc_any_const,
|
|
} = any_consts.unwrap_or_else(|| AnyConsts::new());
|
|
#[hdl]
|
|
let DecodeAndRunSingleInsnInput::<_, _> {
|
|
decoder_input,
|
|
fetch_block_id,
|
|
first_id,
|
|
pc,
|
|
predicted_next_pc,
|
|
regs: input_regs,
|
|
config: _,
|
|
} = harness.input;
|
|
#[hdl]
|
|
let (decoder_first_word, decoder_second_word) = decoder_input;
|
|
connect(decoder_first_word, decoder_first_word_any_const);
|
|
connect(decoder_second_word, HdlNone());
|
|
#[hdl]
|
|
if decoder_has_second_word_any_const {
|
|
connect(decoder_second_word, HdlSome(decoder_second_word_any_const));
|
|
}
|
|
connect(fetch_block_id, 0u8);
|
|
connect(first_id, 0u16);
|
|
connect(pc, pc_any_const);
|
|
connect(predicted_next_pc, predicted_next_pc_any_const);
|
|
#[hdl]
|
|
let matched_any_case = wire();
|
|
connect(matched_any_case, false);
|
|
let matched_cases = Vec::from_iter(cases.cases.iter().map(|case| {
|
|
let matched_case = wire_with_loc(
|
|
&format!("matched_case_{}", case.mnemonic()),
|
|
case.source_location,
|
|
Bool,
|
|
);
|
|
connect(matched_case, false);
|
|
match case.data {
|
|
CaseData::Unprefixed { encoded, imm_mask } => {
|
|
#[hdl]
|
|
if !decoder_has_second_word_any_const
|
|
& (decoder_first_word & !imm_mask).cmp_eq(encoded)
|
|
{
|
|
connect(matched_any_case, true);
|
|
connect(matched_case, true);
|
|
hdl_assume(cd.clk, predicted_next_pc.cmp_eq(pc + 0x4u8), "");
|
|
}
|
|
}
|
|
CaseData::Prefixed {
|
|
encoded: (encoded_prefix, encoded_suffix),
|
|
imm_mask: (imm_mask_prefix, imm_mask_suffix),
|
|
} => {
|
|
#[hdl]
|
|
if decoder_has_second_word_any_const
|
|
& (decoder_first_word & !imm_mask_prefix).cmp_eq(encoded_prefix)
|
|
& (decoder_second_word_any_const & !imm_mask_suffix).cmp_eq(encoded_suffix)
|
|
{
|
|
connect(matched_any_case, true);
|
|
connect(matched_case, true);
|
|
hdl_assume(cd.clk, predicted_next_pc.cmp_eq(pc + 0x8u8), "");
|
|
}
|
|
}
|
|
}
|
|
matched_case
|
|
}));
|
|
hdl_assume(cd.clk, matched_any_case, "");
|
|
connect(
|
|
input_regs.regs,
|
|
repeat(
|
|
PRegValue::zeroed().to_trace_as_string(),
|
|
1 << MOpRegNum::WIDTH,
|
|
),
|
|
);
|
|
#[hdl]
|
|
let input_r3 = wire();
|
|
connect(input_r3, r3_any_const);
|
|
#[hdl]
|
|
let input_r4 = wire();
|
|
connect(input_r4, r4_any_const);
|
|
#[hdl]
|
|
let input_ca = wire();
|
|
connect(input_ca, ca_any_const);
|
|
connect(
|
|
input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(3).value].int_fp,
|
|
input_r3,
|
|
);
|
|
connect(
|
|
input_regs.regs[MOpRegNum::power_isa_gpr_reg_imm(4).value].int_fp,
|
|
input_r4,
|
|
);
|
|
connect(
|
|
PRegFlags::view::<PRegFlagsPowerISA>(
|
|
input_regs.regs[MOpRegNum::power_isa_xer_ca_ca32_reg().value].flags,
|
|
)
|
|
.xer_ca,
|
|
input_ca,
|
|
);
|
|
// a copy of the output so you can see the signal values in formal proof error traces
|
|
#[hdl]
|
|
let output_reg = reg_builder()
|
|
.clock_domain(cd)
|
|
.no_reset(harness.ty().output.HdlSome);
|
|
#[hdl]
|
|
if let HdlSome(output) = harness.output {
|
|
connect(ran_reg, true);
|
|
connect(output_reg, output);
|
|
#[hdl]
|
|
let DecodeAndRunSingleInsnOutput::<_, _> {
|
|
regs: output_regs,
|
|
cancel_and_start_at,
|
|
retired_insns,
|
|
config: _,
|
|
} = output;
|
|
hdl_assert(cd.clk, cancel_and_start_at.cmp_eq(HdlNone()), "");
|
|
hdl_assert(cd.clk, ArrayVec::len(retired_insns).cmp_eq(1u8), "");
|
|
#[hdl]
|
|
let NextPcPredictorOp::<_> {
|
|
call_stack_op,
|
|
cond_br_taken,
|
|
config: _,
|
|
} = retired_insns[0];
|
|
hdl_assert(cd.clk, call_stack_op.cmp_eq(CallStackOp.None()), "");
|
|
hdl_assert(cd.clk, cond_br_taken.cmp_eq(HdlNone()), "");
|
|
for (case, &matched_case) in cases.cases.iter().zip(&matched_cases) {
|
|
#[hdl]
|
|
if matched_case {
|
|
let input = harness.input;
|
|
let suffix = match case.data {
|
|
CaseData::Unprefixed { .. } => input.decoder_input.0,
|
|
CaseData::Prefixed { .. } => decoder_second_word_any_const,
|
|
};
|
|
let mut case_io = CaseIO {
|
|
input,
|
|
suffix,
|
|
output,
|
|
read_output_regs: BTreeSet::new(),
|
|
};
|
|
(case.check)(cd.clk, &mut case_io);
|
|
let CaseIO {
|
|
input: _,
|
|
suffix: _,
|
|
output: _,
|
|
read_output_regs,
|
|
} = case_io;
|
|
for (reg_index, output_reg) in output_regs.regs.into_iter().enumerate() {
|
|
let reg_num = reg_index as u32;
|
|
if read_output_regs.contains(®_num) {
|
|
continue;
|
|
}
|
|
hdl_assert(cd.clk, output_reg.cmp_eq(input_regs.regs[reg_index]), "");
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
fn test_power_isa_add_sub_formal(subdivision_index: usize, subdivision_count: usize) {
|
|
let config = PhantomConst::new_sized(CpuConfig::new(
|
|
vec![UnitConfig::new(UnitKind::AluBranch)],
|
|
NonZero::new(20).unwrap(),
|
|
));
|
|
let m = check_power_isa_alu_formal(
|
|
config,
|
|
&cases_add_sub().subdivide(subdivision_index, subdivision_count),
|
|
None,
|
|
);
|
|
assert_formal(
|
|
format_args!("test_power_isa_add_sub_formal_{subdivision_index}"),
|
|
m,
|
|
FormalMode::BMC,
|
|
7,
|
|
None,
|
|
ExportOptions {
|
|
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
|
|
..Default::default()
|
|
},
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_0() {
|
|
test_power_isa_add_sub_formal(0, 6);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_1() {
|
|
test_power_isa_add_sub_formal(1, 6);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_2() {
|
|
test_power_isa_add_sub_formal(2, 6);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_3() {
|
|
test_power_isa_add_sub_formal(3, 6);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_4() {
|
|
test_power_isa_add_sub_formal(4, 6);
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_formal_5() {
|
|
test_power_isa_add_sub_formal(5, 6);
|
|
}
|
|
|
|
#[hdl]
|
|
fn test_power_isa_alu_sim(
|
|
cases: Cases,
|
|
checked_vcd_output: impl FnOnce(
|
|
&mut Simulation<check_power_isa_alu_formal>,
|
|
) -> fayalite::testing::CheckedVcdOutput,
|
|
) {
|
|
let config = PhantomConst::new_sized(CpuConfig::new(
|
|
vec![UnitConfig::new(UnitKind::AluBranch)],
|
|
NonZero::new(20).unwrap(),
|
|
));
|
|
let any_consts = AnyConsts::new();
|
|
let m = check_power_isa_alu_formal(config, &cases, Some(any_consts));
|
|
let mut sim = Simulation::new(m);
|
|
let _checked_vcd_output = checked_vcd_output(&mut sim);
|
|
let AnyConsts {
|
|
decoder_first_word_any_const,
|
|
decoder_has_second_word_any_const,
|
|
decoder_second_word_any_const,
|
|
r3_any_const,
|
|
r4_any_const,
|
|
ca_any_const,
|
|
pc_any_const,
|
|
predicted_next_pc_any_const,
|
|
} = any_consts;
|
|
const REG_VALUES: &[u64] = &[0x0, 0xAAAA_AAAA_AAAA_AAAA, 0xFFFF_FFFF_FFFF_FFFF];
|
|
const IMM_S16_VALUES: &[i16] = &[0, 1, -1, i16::MAX, i16::MIN, 0x100];
|
|
const S34_MAX: i64 = (1 << 33) - 1;
|
|
const S34_MIN: i64 = -1 << 33;
|
|
const IMM_S34_VALUES: &[i64] = &[0, 1, -1, S34_MAX, S34_MIN];
|
|
const PC: u64 = 0x1000;
|
|
for case in &cases.cases {
|
|
let r3_values = if case.inputs.contains(&MOpRegNum::power_isa_gpr_reg_num(3)) {
|
|
REG_VALUES
|
|
} else {
|
|
&[0]
|
|
};
|
|
let r4_values = if case.inputs.contains(&MOpRegNum::power_isa_gpr_reg_num(4)) {
|
|
REG_VALUES
|
|
} else {
|
|
&[0]
|
|
};
|
|
let ca_values: &[bool] = if case
|
|
.inputs
|
|
.contains(&MOpRegNum::POWER_ISA_XER_CA_CA32_REG_NUM)
|
|
{
|
|
&[false, true]
|
|
} else {
|
|
&[false]
|
|
};
|
|
for &r3 in r3_values {
|
|
for &r4 in r4_values {
|
|
for &ca in ca_values {
|
|
let mut imm_index = 0;
|
|
loop {
|
|
let asm = case.asm;
|
|
let source_location = case.source_location;
|
|
println!(
|
|
"\ncase: {asm}\n\
|
|
r3={r3:#x} r4={r4:#x} ca={ca}\n\
|
|
at: {source_location}"
|
|
);
|
|
sim.write(r3_any_const, r3);
|
|
sim.write(r4_any_const, r4);
|
|
sim.write(ca_any_const, ca);
|
|
sim.write(pc_any_const, PC);
|
|
let imm_count;
|
|
match case.data {
|
|
CaseData::Unprefixed { encoded, imm_mask } => {
|
|
sim.write(predicted_next_pc_any_const, PC + 4);
|
|
let imm = IMM_S16_VALUES[imm_index] as i64;
|
|
if imm_mask == 0 {
|
|
imm_count = 1;
|
|
} else {
|
|
imm_count = IMM_S16_VALUES.len();
|
|
println!("imm = {imm:#x}");
|
|
}
|
|
let mut imm = imm as u32;
|
|
if case.mnemonic() == "addpcis" {
|
|
let d2 = imm & 1;
|
|
let d1 = (imm >> 1) & 0x1F;
|
|
let d0 = (imm >> 6) & 0x3FF;
|
|
imm = d2 | (d1 << 16) | (d0 << 6);
|
|
}
|
|
sim.write(decoder_first_word_any_const, encoded | (imm_mask & imm));
|
|
sim.write(decoder_has_second_word_any_const, false);
|
|
sim.write(decoder_second_word_any_const, 0u32);
|
|
}
|
|
CaseData::Prefixed {
|
|
encoded: (encoded_prefix, encoded_suffix),
|
|
imm_mask: (imm_mask_prefix, imm_mask_suffix),
|
|
} => {
|
|
sim.write(predicted_next_pc_any_const, PC + 8);
|
|
let imm = IMM_S34_VALUES[imm_index];
|
|
if imm_mask_prefix == 0 && imm_mask_suffix == 0 {
|
|
imm_count = 1;
|
|
} else {
|
|
imm_count = IMM_S34_VALUES.len();
|
|
println!("imm = {imm:#x}");
|
|
}
|
|
sim.write(
|
|
decoder_first_word_any_const,
|
|
encoded_prefix | (imm_mask_prefix & (imm >> 16) as u32),
|
|
);
|
|
sim.write(decoder_has_second_word_any_const, true);
|
|
sim.write(
|
|
decoder_second_word_any_const,
|
|
encoded_suffix | (imm_mask_suffix & (imm & 0xFFFF) as u32),
|
|
);
|
|
}
|
|
}
|
|
let clk = formal_global_clock();
|
|
let rst = formal_reset();
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, true);
|
|
for cycle in 0..10 {
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
println!("clock tick: {cycle}");
|
|
sim.write_clock(clk, true);
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, false);
|
|
if sim.read_bool(sim.io().ran) {
|
|
break;
|
|
}
|
|
}
|
|
assert!(sim.read_bool(sim.io().ran));
|
|
imm_index += 1;
|
|
if imm_index >= imm_count {
|
|
break;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_0() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(0, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_0.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_1() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(1, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_1.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_2() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(2, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_2.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_3() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(3, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_3.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_4() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(4, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_4.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_sub_sim_5() {
|
|
test_power_isa_alu_sim(cases_add_sub().subdivide(5, 6), |sim| {
|
|
checked_vcd_output!(
|
|
sim,
|
|
"tests/expected/units_formal_power_isa_add_sub_sim_5.vcd"
|
|
)
|
|
});
|
|
}
|
|
|
|
#[hdl]
|
|
#[test]
|
|
fn test_power_isa_add_sim() {
|
|
let config = PhantomConst::new_sized(CpuConfig::new(
|
|
vec![UnitConfig::new(UnitKind::AluBranch)],
|
|
NonZero::new(20).unwrap(),
|
|
));
|
|
let any_consts = AnyConsts::new();
|
|
let m = check_power_isa_alu_formal(config, &cases_add_sub(), Some(any_consts));
|
|
let mut sim = Simulation::new(m);
|
|
let _checked_vcd_output = checked_vcd_output!(
|
|
&mut sim,
|
|
"tests/expected/units_formal_power_isa_add_sim.vcd",
|
|
);
|
|
let AnyConsts {
|
|
decoder_first_word_any_const,
|
|
decoder_has_second_word_any_const,
|
|
decoder_second_word_any_const,
|
|
r3_any_const,
|
|
r4_any_const,
|
|
ca_any_const,
|
|
pc_any_const,
|
|
predicted_next_pc_any_const,
|
|
} = any_consts;
|
|
sim.write(decoder_first_word_any_const, 0x7C63_2214u32); // add 3, 3, 4
|
|
sim.write(decoder_has_second_word_any_const, false);
|
|
sim.write(decoder_second_word_any_const, 0u32);
|
|
sim.write(r3_any_const, 0x1234u64);
|
|
sim.write(r4_any_const, 0x1234u64);
|
|
sim.write(ca_any_const, false);
|
|
sim.write(pc_any_const, 0x1000u64);
|
|
sim.write(predicted_next_pc_any_const, 0x1004u64);
|
|
let clk = formal_global_clock();
|
|
let rst = formal_reset();
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, true);
|
|
for cycle in 0..10 {
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
println!("clock tick: {cycle}");
|
|
sim.write_clock(clk, true);
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, false);
|
|
}
|
|
assert!(sim.read_bool(sim.io().ran));
|
|
}
|
|
|
|
#[hdl]
|
|
#[test]
|
|
fn test_power_isa_paddi_sim() {
|
|
let config = PhantomConst::new_sized(CpuConfig::new(
|
|
vec![UnitConfig::new(UnitKind::AluBranch)],
|
|
NonZero::new(20).unwrap(),
|
|
));
|
|
let any_consts = AnyConsts::new();
|
|
let m = check_power_isa_alu_formal(config, &cases_add_sub(), Some(any_consts));
|
|
let mut sim = Simulation::new(m);
|
|
let _checked_vcd_output = checked_vcd_output!(
|
|
&mut sim,
|
|
"tests/expected/units_formal_power_isa_paddi_sim.vcd",
|
|
);
|
|
let AnyConsts {
|
|
decoder_first_word_any_const,
|
|
decoder_has_second_word_any_const,
|
|
decoder_second_word_any_const,
|
|
r3_any_const,
|
|
r4_any_const,
|
|
ca_any_const,
|
|
pc_any_const,
|
|
predicted_next_pc_any_const,
|
|
} = any_consts;
|
|
sim.write(decoder_first_word_any_const, 0x0600_0000u32);
|
|
sim.write(decoder_has_second_word_any_const, true);
|
|
sim.write(decoder_second_word_any_const, 0x3864_1000u32); // paddi 3, 4, 0x1000, 0
|
|
sim.write(r3_any_const, 0x9907_4F26_0000_0002u64);
|
|
sim.write(r4_any_const, 0x6000_0424_17DF_FEFDu64);
|
|
sim.write(ca_any_const, false);
|
|
sim.write(pc_any_const, 0x1000u64);
|
|
sim.write(predicted_next_pc_any_const, 0x1008u64);
|
|
let clk = formal_global_clock();
|
|
let rst = formal_reset();
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, true);
|
|
for cycle in 0..10 {
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
println!("clock tick: {cycle}");
|
|
sim.write_clock(clk, true);
|
|
sim.advance_time(SimDuration::from_nanos(500));
|
|
sim.write_clock(clk, false);
|
|
sim.write_reset(rst, false);
|
|
}
|
|
assert!(sim.read_bool(sim.io().ran));
|
|
}
|