{"id":"W4413755345","doi":"10.1109/isvlsi65124.2025.11130337","title":"HW/SW Formal Co-Verification of Rust-based Designs Using Hardware Abstraction Model","year":2025,"lang":"en","type":"article","venue":"","topic":"VLSI and Analog Circuit Testing","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Infineon Technologies (Canada)","funders":"","keywords":"Computer science; Formal verification; Abstraction; Formal methods; Verification; Programming language; Rust (programming language); Intelligent verification; Embedded system; Software; Software development; Software construction","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.0002241611,0.00007383899,0.00009634245,0.0001283344,0.000135172,0.00005650626,0.0002649292,0.00004779241,0.000006860223],"category_scores_gemma":[0.00003653095,0.00007244817,0.00004720907,0.0002759542,0.00001818372,0.000567253,0.00002325832,0.00006761058,0.000004347026],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00004879506,"about_ca_system_score_gemma":0.0002098755,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00006717793,"about_ca_topic_score_gemma":0.000004225892,"domain_scores_codex":[0.9992797,0.00001915049,0.0002200038,0.0001846715,0.0001362859,0.0001601609],"domain_scores_gemma":[0.9994448,0.00005406894,0.0001014114,0.0002579282,0.0001130405,0.00002875612],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.000002269773,0.0001418282,0.002423532,0.0001238829,0.00002008845,0.000002347662,0.0002064446,0.508294,0.2603513,0.05466151,0.0002772007,0.1734956],"study_design_scores_gemma":[0.000154654,0.00001074758,0.00146014,0.00003396663,0.000006657725,0.000001060129,0.00002234449,0.9404679,0.05721317,0.0005370264,0.00002309019,0.00006922404],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.03598594,0.000009397328,0.9578512,0.00008740545,0.00006337435,0.00008137261,0.000001588074,0.0001191814,0.005800533],"genre_scores_gemma":[0.9464586,5.645331e-7,0.05323851,0.0001406736,0.000009763062,0.00000299687,0.000004455589,0.000002988539,0.0001413847],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.9104728,"threshold_uncertainty_score":0.2954351,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08984288716523385,"score_gpt":0.3222532353586027,"score_spread":0.2324103481933689,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}