cpu/crates/cpu/tests/units_formal.rs

// 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.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(),
    ));
    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 clk: Clock = m.input();
    #[hdl]
    let cd = wire();
    connect(
        cd,
        #[hdl]
        ClockDomain {
            clk,
            rst: formal_reset().to_reset(),
        },
    );
    #[hdl]
    let harness = instance(formal_harness(config));
    connect(harness.cd, 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 m = check_power_isa_add_formal(config);
    println!("starting assert formal");
    assert_formal(
        "test_power_isa_add_formal",
        m,
        FormalMode::Prove,
        10,
        None,
        ExportOptions {
            simplify_enums: Some(SimplifyEnumsKind::ReplaceWithBundleOfUInts),
            ..Default::default()
        },
    );
}