{"id":"W2042451806","doi":"10.1109/mtv.2011.15","title":"Overview of Applying Reachability Analysis to Verifying a Physical Microprocessor","year":2011,"lang":"en","type":"article","venue":"","topic":"Embedded Systems Design Techniques","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Institut National de la Recherche Scientifique","funders":"","keywords":"Computer science; Microprocessor; VHDL; Microcontroller; Field-programmable gate array; Reachability; Embedded system; Abstraction; Instruction set; Computer architecture; Programming language; Theoretical computer science","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.0005642328,0.0001243321,0.0003921518,0.0002331154,0.00003498537,0.00002682598,0.0009406211,0.0000426582,0.00001767452],"category_scores_gemma":[0.00004394797,0.000104785,0.0001890343,0.001772086,0.00002708038,0.0002591667,0.0003001319,0.00007261558,0.00002060879],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00003746458,"about_ca_system_score_gemma":0.00002844753,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0007155173,"about_ca_topic_score_gemma":0.0000319783,"domain_scores_codex":[0.9987142,0.00009276933,0.0003114825,0.0004282098,0.0002529072,0.0002004046],"domain_scores_gemma":[0.9986393,0.00005800428,0.0001173495,0.0009538023,0.0001422286,0.00008931771],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"bench_or_experimental","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.00004893071,0.001468301,0.02411725,0.001229055,0.001333078,0.00002232176,0.05370864,0.00002658124,0.3849965,0.3197643,0.0007614892,0.2125235],"study_design_scores_gemma":[0.000182975,0.0003331114,0.01088669,0.0001171858,0.000233755,0.000007028863,0.0002177715,0.0234734,0.9456131,0.01764038,0.0006529996,0.000641605],"study_design_candidate":"bench_or_experimental","study_design_consensus":"bench_or_experimental","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0842272,0.00006653259,0.9071018,0.00002335172,0.00002262672,0.000348678,0.000001031133,0.0003167666,0.007892078],"genre_scores_gemma":[0.7585288,0.000001811894,0.2412499,0.000074336,0.0000105386,0.00007592569,2.187466e-7,0.000004856877,0.00005363226],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6743016,"threshold_uncertainty_score":0.4273009,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1208461705218708,"score_gpt":0.3322447052722625,"score_spread":0.2113985347503917,"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."}}