{"id":"W2065518690","doi":"10.1145/1109118.1109123","title":"Simplifying the design and automating the verification of pipelines with structural hazards","year":2005,"lang":"en","type":"article","venue":"ACM Transactions on Design Automation of Electronic Systems","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":9,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Waterloo","funders":"","keywords":"Computer science; Datapath; Correctness; Pipeline (software); Microprocessor; Pipeline transport; Computer architecture; Formal verification; Embedded system; Programming language","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.002145059,0.0001658625,0.0002027882,0.0001372617,0.0003533025,0.0001001917,0.0008398349,0.00007112831,0.000003879903],"category_scores_gemma":[0.0001223705,0.00009820156,0.00004399479,0.0005842582,0.0001207466,0.0006010001,0.000008255011,0.0001932974,0.000003140756],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001227302,"about_ca_system_score_gemma":0.0001865178,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002743239,"about_ca_topic_score_gemma":0.000003055193,"domain_scores_codex":[0.9977309,0.0007824074,0.0005618791,0.0002535153,0.0004245328,0.0002467376],"domain_scores_gemma":[0.9973115,0.0009716611,0.0005335356,0.0009401875,0.0002151447,0.000027958],"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.00005412623,0.00003314794,0.00000860025,0.0000757115,0.00008402428,8.427624e-8,0.002330724,0.7557992,0.009966333,0.03003398,0.00002437958,0.2015897],"study_design_scores_gemma":[0.0002477478,0.0002723791,0.0005551413,0.00006646011,0.00003243031,0.00005488332,0.0001910892,0.956721,0.04097818,0.0007005862,0.00007343675,0.0001066486],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.01177468,0.0003253422,0.9860481,0.0006265769,0.0001021551,0.0009477803,0.000001346757,0.0001528194,0.00002122803],"genre_scores_gemma":[0.6691791,0.00002046686,0.3306343,0.00001848037,0.0000196687,0.00009880343,6.144035e-7,0.000009149237,0.000019452],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.6574044,"threshold_uncertainty_score":0.4004543,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03096008423381525,"score_gpt":0.2810010768775404,"score_spread":0.2500409926437251,"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."}}