224 lines
7.4 KiB
Rust
224 lines
7.4 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,
|
|
instruction::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::{UnitKind, UnitTrait},
|
|
util::array_vec::ArrayVec,
|
|
};
|
|
use fayalite::{
|
|
firrtl::ExportOptions,
|
|
module::{instance_with_loc, transform::simplify_enums::SimplifyEnumsKind},
|
|
prelude::*,
|
|
ty::StaticType,
|
|
};
|
|
use std::num::NonZero;
|
|
|
|
#[hdl_module]
|
|
fn formal_harness(config: PhantomConst<CpuConfig>) {
|
|
#[hdl]
|
|
let cd: ClockDomain = m.output();
|
|
connect(cd.clk, fayalite::formal::formal_global_clock());
|
|
connect(cd.rst, fayalite::formal::formal_reset().to_reset());
|
|
|
|
#[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(),
|
|
));
|
|
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);
|
|
let unit = instance_with_loc(
|
|
&decode_and_run.ty().to_units.unit_field_name(unit_index),
|
|
dyn_unit.module(),
|
|
SourceLocation::caller(),
|
|
);
|
|
connect(
|
|
dyn_unit.from_execute(unit),
|
|
ExecuteToUnitInterfaces::unit_fields(decode_and_run.to_units)[unit_index],
|
|
);
|
|
if let Some(unit_cd) = dyn_unit.cd(unit) {
|
|
connect(unit_cd, cd);
|
|
}
|
|
}
|
|
hdl_assert(cd.clk, !decode_and_run.error, "");
|
|
}
|
|
|
|
#[hdl_module]
|
|
fn check_power_isa_add_formal(config: PhantomConst<CpuConfig>) {
|
|
#[hdl]
|
|
let harness = instance(formal_harness(config));
|
|
let cd = harness.cd;
|
|
#[hdl]
|
|
let DecodeAndRunSingleInsnInput::<_, _> {
|
|
decoder_input,
|
|
fetch_block_id,
|
|
first_id,
|
|
pc,
|
|
predicted_next_pc,
|
|
regs: input_regs,
|
|
config: _,
|
|
} = harness.input;
|
|
// add r3, r3, r4
|
|
connect(decoder_input, (0x7c632214_u32, HdlNone()));
|
|
connect(fetch_block_id, 0u8);
|
|
connect(first_id, 0u16);
|
|
connect(pc, 0x1000_u64);
|
|
connect(predicted_next_pc, 0x1004_u64);
|
|
connect(
|
|
input_regs.regs,
|
|
repeat(
|
|
PRegValue::zeroed().to_trace_as_string(),
|
|
1 << MOpRegNum::WIDTH,
|
|
),
|
|
);
|
|
#[hdl]
|
|
let input_r3 = wire();
|
|
connect(input_r3, any_const(StaticType::TYPE));
|
|
#[hdl]
|
|
let input_r4 = wire();
|
|
connect(input_r4, any_const(StaticType::TYPE));
|
|
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,
|
|
);
|
|
#[hdl]
|
|
if let HdlSome(output) = harness.output {
|
|
#[hdl]
|
|
let DecodeAndRunSingleInsnOutput::<_, _> {
|
|
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()), "");
|
|
#[hdl]
|
|
let expected_regs = wire(regs.ty());
|
|
for (reg_index, expected) in expected_regs.regs.into_iter().enumerate() {
|
|
let reg_num = reg_index as u32;
|
|
if reg_num == MOpRegNum::power_isa_gpr_reg_num(3) {
|
|
connect(expected.int_fp, (input_r3 + input_r4).cast_to_static());
|
|
let PRegFlagsPowerISAView {
|
|
unused: _,
|
|
xer_ca,
|
|
xer_ca32,
|
|
xer_ov,
|
|
xer_ov32,
|
|
cr_lt,
|
|
cr_gt,
|
|
cr_eq,
|
|
so,
|
|
..
|
|
} = PRegFlags::view::<PRegFlagsPowerISA>(expected.flags);
|
|
let input_r3_s = input_r3.cast_to_static::<SInt<64>>();
|
|
let input_r4_s = input_r4.cast_to_static::<SInt<64>>();
|
|
let u64_sum = input_r3 + input_r4;
|
|
let s64_sum = input_r3_s + input_r4_s;
|
|
let u32_sum = input_r3.cast_to(UInt[32]) + input_r4.cast_to(UInt[32]);
|
|
let s32_sum = input_r3.cast_to(SInt[32]) + input_r4.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
|
|
} else {
|
|
connect(expected, input_regs.regs[reg_index]);
|
|
}
|
|
}
|
|
hdl_assert(cd.clk, expected_regs.cmp_eq(regs), "");
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn test_power_isa_add_formal() {
|
|
let config = PhantomConst::new_sized(CpuConfig::new(
|
|
vec![UnitConfig::new(UnitKind::AluBranch)],
|
|
NonZero::new(20).unwrap(),
|
|
));
|
|
let dut = check_power_isa_add_formal(config);
|
|
println!("starting assert formal");
|
|
assert_formal(
|
|
"test_power_isa_add_formal",
|
|
dut,
|
|
FormalMode::Prove,
|
|
10,
|
|
None,
|
|
ExportOptions {
|
|
simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
|
|
..Default::default()
|
|
},
|
|
);
|
|
}
|