fayalite/crates/fayalite/src/build/formal.rs

// SPDX-License-Identifier: LGPL-3.0-or-later
// See Notices.txt for copyright information

use crate::{
    build::{
        BaseJob, CommandParams, DynJobKind, GetJobPositionDependencies, GlobalParams,
        JobAndDependencies, JobArgsAndDependencies, JobDependencies, JobItem, JobItemName, JobKind,
        JobKindAndDependencies, JobParams, ToArgs, WriteArgs,
        external::{
            ExternalCommand, ExternalCommandJob, ExternalCommandJobKind, ExternalProgramTrait,
        },
        verilog::{UnadjustedVerilog, VerilogDialect, VerilogJob, VerilogJobKind},
    },
    intern::{Intern, InternSlice, Interned},
    module::NameId,
    testing::FormalMode,
    util::job_server::AcquiredJob,
};
use clap::Args;
use eyre::Context;
use serde::{Deserialize, Serialize};
use std::{
    ffi::{OsStr, OsString},
    fmt::{self, Write},
    path::Path,
};

#[derive(Args, Clone, Debug, PartialEq, Eq, Hash)]
#[non_exhaustive]
pub struct FormalArgs {
    #[arg(long = "sby-extra-arg", value_name = "ARG")]
    pub sby_extra_args: Vec<OsString>,
    #[arg(long, default_value_t)]
    pub formal_mode: FormalMode,
    #[arg(long, default_value_t = Self::DEFAULT_DEPTH)]
    pub formal_depth: u64,
    #[arg(long, default_value = Self::DEFAULT_SOLVER)]
    pub formal_solver: String,
    #[arg(long = "smtbmc-extra-arg", value_name = "ARG")]
    pub smtbmc_extra_args: Vec<OsString>,
}

impl FormalArgs {
    pub const DEFAULT_DEPTH: u64 = 20;
    pub const DEFAULT_SOLVER: &'static str = "z3";
}

impl ToArgs for FormalArgs {
    fn to_args(&self, args: &mut (impl WriteArgs + ?Sized)) {
        let Self {
            sby_extra_args,
            formal_mode,
            formal_depth,
            formal_solver,
            smtbmc_extra_args,
        } = self;
        for arg in sby_extra_args {
            args.write_long_option_eq("sby-extra-arg", arg);
        }
        args.write_display_args([
            format_args!("--formal-mode={formal_mode}"),
            format_args!("--formal-depth={formal_depth}"),
            format_args!("--formal-solver={formal_solver}"),
        ]);
        for arg in smtbmc_extra_args {
            args.write_long_option_eq("smtbmc-extra-arg", arg);
        }
    }
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Default)]
pub struct WriteSbyFileJobKind;

#[derive(Clone, Debug, PartialEq, Eq, Hash, Deserialize, Serialize)]
pub struct WriteSbyFileJob {
    sby_extra_args: Interned<[Interned<OsStr>]>,
    formal_mode: FormalMode,
    formal_depth: u64,
    formal_solver: Interned<str>,
    smtbmc_extra_args: Interned<[Interned<OsStr>]>,
    sby_file: Interned<Path>,
    output_dir: Interned<Path>,
    main_verilog_file: Interned<Path>,
}

impl WriteSbyFileJob {
    pub fn sby_extra_args(&self) -> Interned<[Interned<OsStr>]> {
        self.sby_extra_args
    }
    pub fn formal_mode(&self) -> FormalMode {
        self.formal_mode
    }
    pub fn formal_depth(&self) -> u64 {
        self.formal_depth
    }
    pub fn formal_solver(&self) -> Interned<str> {
        self.formal_solver
    }
    pub fn smtbmc_extra_args(&self) -> Interned<[Interned<OsStr>]> {
        self.smtbmc_extra_args
    }
    pub fn sby_file(&self) -> Interned<Path> {
        self.sby_file
    }
    pub fn output_dir(&self) -> Interned<Path> {
        self.output_dir
    }
    pub fn main_verilog_file(&self) -> Interned<Path> {
        self.main_verilog_file
    }
    fn write_sby(
        &self,
        output: &mut OsString,
        additional_files: &[Interned<Path>],
        main_module_name_id: NameId,
    ) -> eyre::Result<()> {
        let Self {
            sby_extra_args: _,
            formal_mode,
            formal_depth,
            formal_solver,
            smtbmc_extra_args,
            sby_file: _,
            output_dir: _,
            main_verilog_file,
        } = self;
        write!(
            output,
            "[options]\n\
            mode {formal_mode}\n\
            depth {formal_depth}\n\
            wait on\n\
            \n\
            [engines]\n\
            smtbmc {formal_solver} -- --"
        )
        .expect("writing to OsString can't fail");
        for i in smtbmc_extra_args {
            output.push(" ");
            output.push(i);
        }
        output.push(
            "\n\
            \n\
            [script]\n",
        );
        for verilog_file in VerilogJob::all_verilog_files(*main_verilog_file, additional_files)? {
            output.push("read_verilog -sv -formal \"");
            output.push(verilog_file);
            output.push("\"\n");
        }
        let circuit_name = crate::firrtl::get_circuit_name(main_module_name_id);
        // workaround for wires disappearing -- set `keep` on all wires
        writeln!(
            output,
            "hierarchy -top {circuit_name}\n\
            proc\n\
            setattr -set keep 1 w:\\*\n\
            prep",
        )
        .expect("writing to OsString can't fail");
        Ok(())
    }
}

impl JobKind for WriteSbyFileJobKind {
    type Args = FormalArgs;
    type Job = WriteSbyFileJob;
    type Dependencies = JobKindAndDependencies<VerilogJobKind>;

    fn dependencies(self) -> Self::Dependencies {
        Default::default()
    }

    fn args_to_jobs(
        mut args: JobArgsAndDependencies<Self>,
        params: &JobParams,
        global_params: &GlobalParams,
    ) -> eyre::Result<JobAndDependencies<Self>> {
        args.dependencies
            .dependencies
            .args
            .args
            .additional_args
            .verilog_dialect
            .get_or_insert(VerilogDialect::Yosys);
        args.args_to_jobs_simple(params, global_params, |_kind, args, dependencies| {
            let FormalArgs {
                sby_extra_args,
                formal_mode,
                formal_depth,
                formal_solver,
                smtbmc_extra_args,
            } = args;
            let base_job = dependencies.get_job::<BaseJob, _>();
            Ok(WriteSbyFileJob {
                sby_extra_args: sby_extra_args.into_iter().map(Interned::from).collect(),
                formal_mode,
                formal_depth,
                formal_solver: formal_solver.intern_deref(),
                smtbmc_extra_args: smtbmc_extra_args.into_iter().map(Interned::from).collect(),
                sby_file: base_job.file_with_ext("sby"),
                output_dir: base_job.output_dir(),
                main_verilog_file: dependencies.get_job::<VerilogJob, _>().main_verilog_file(),
            })
        })
    }

    fn inputs(self, _job: &Self::Job) -> Interned<[JobItemName]> {
        [JobItemName::DynamicPaths {
            source_job_name: VerilogJobKind.name(),
        }]
        .intern_slice()
    }

    fn outputs(self, job: &Self::Job) -> Interned<[JobItemName]> {
        [JobItemName::Path { path: job.sby_file }].intern_slice()
    }

    fn name(self) -> Interned<str> {
        "write-sby-file".intern()
    }

    fn external_command_params(self, _job: &Self::Job) -> Option<CommandParams> {
        None
    }

    fn run(
        self,
        job: &Self::Job,
        inputs: &[JobItem],
        params: &JobParams,
        _global_params: &GlobalParams,
        _acquired_job: &mut AcquiredJob,
    ) -> eyre::Result<Vec<JobItem>> {
        assert!(inputs.iter().map(JobItem::name).eq(self.inputs(job)));
        let [additional_files] = inputs else {
            unreachable!();
        };
        let additional_files = VerilogJob::unwrap_additional_files(additional_files);
        let mut contents = OsString::new();
        job.write_sby(
            &mut contents,
            additional_files,
            params.main_module().name_id(),
        )?;
        let path = job.sby_file;
        std::fs::write(path, contents.as_encoded_bytes())
            .wrap_err_with(|| format!("writing {path:?} failed"))?;
        Ok(vec![JobItem::Path { path }])
    }

    fn subcommand_hidden(self) -> bool {
        true
    }
}

#[derive(Clone, Hash, PartialEq, Eq, Serialize, Deserialize)]
pub struct Formal {
    #[serde(flatten)]
    write_sby_file: WriteSbyFileJob,
    sby_file_name: Interned<OsStr>,
}

impl fmt::Debug for Formal {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let Self {
            write_sby_file:
                WriteSbyFileJob {
                    sby_extra_args,
                    formal_mode,
                    formal_depth,
                    formal_solver,
                    smtbmc_extra_args,
                    sby_file,
                    output_dir: _,
                    main_verilog_file,
                },
            sby_file_name,
        } = self;
        f.debug_struct("Formal")
            .field("sby_extra_args", sby_extra_args)
            .field("formal_mode", formal_mode)
            .field("formal_depth", formal_depth)
            .field("formal_solver", formal_solver)
            .field("smtbmc_extra_args", smtbmc_extra_args)
            .field("sby_file", sby_file)
            .field("sby_file_name", sby_file_name)
            .field("main_verilog_file", main_verilog_file)
            .finish_non_exhaustive()
    }
}

#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug, Default)]
pub struct Symbiyosys;

impl ExternalProgramTrait for Symbiyosys {
    fn default_program_name() -> Interned<str> {
        "sby".intern()
    }
}

#[derive(Clone, Hash, PartialEq, Eq, Debug, Args)]
pub struct FormalAdditionalArgs {}

impl ToArgs for FormalAdditionalArgs {
    fn to_args(&self, _args: &mut (impl WriteArgs + ?Sized)) {
        let Self {} = self;
    }
}

impl ExternalCommand for Formal {
    type AdditionalArgs = FormalAdditionalArgs;
    type AdditionalJobData = Formal;
    type BaseJobPosition = GetJobPositionDependencies<
        GetJobPositionDependencies<
            GetJobPositionDependencies<<UnadjustedVerilog as ExternalCommand>::BaseJobPosition>,
        >,
    >;
    type Dependencies = JobKindAndDependencies<WriteSbyFileJobKind>;
    type ExternalProgram = Symbiyosys;

    fn dependencies() -> Self::Dependencies {
        Default::default()
    }

    fn args_to_jobs(
        args: JobArgsAndDependencies<ExternalCommandJobKind<Self>>,
        params: &JobParams,
        global_params: &GlobalParams,
    ) -> eyre::Result<(
        Self::AdditionalJobData,
        <Self::Dependencies as JobDependencies>::JobsAndKinds,
    )> {
        args.args_to_jobs_external_simple(params, global_params, |args, dependencies| {
            let FormalAdditionalArgs {} = args.additional_args;
            let write_sby_file = dependencies.get_job::<WriteSbyFileJob, _>().clone();
            Ok(Formal {
                sby_file_name: write_sby_file
                    .sby_file()
                    .interned_file_name()
                    .expect("known to have file name"),
                write_sby_file,
            })
        })
    }

    fn inputs(job: &ExternalCommandJob<Self>) -> Interned<[JobItemName]> {
        [
            JobItemName::Path {
                path: job.additional_job_data().write_sby_file.sby_file(),
            },
            JobItemName::Path {
                path: job.additional_job_data().write_sby_file.main_verilog_file(),
            },
            JobItemName::DynamicPaths {
                source_job_name: VerilogJobKind.name(),
            },
        ]
        .intern_slice()
    }

    fn output_paths(_job: &ExternalCommandJob<Self>) -> Interned<[Interned<Path>]> {
        Interned::default()
    }

    fn command_line_args<W: ?Sized + WriteArgs>(job: &ExternalCommandJob<Self>, args: &mut W) {
        // args.write_str_arg("-j1"); // sby seems not to respect job count in parallel mode
        args.write_arg("-f");
        args.write_interned_arg(job.additional_job_data().sby_file_name);
        args.write_interned_args(job.additional_job_data().write_sby_file.sby_extra_args());
    }

    fn current_dir(job: &ExternalCommandJob<Self>) -> Option<Interned<Path>> {
        Some(job.output_dir())
    }

    fn job_kind_name() -> Interned<str> {
        "formal".intern()
    }
}

pub(crate) fn built_in_job_kinds() -> impl IntoIterator<Item = DynJobKind> {
    [
        DynJobKind::new(WriteSbyFileJobKind),
        DynJobKind::new(ExternalCommandJobKind::<Formal>::new()),
    ]
}