{"id":"W4231425351","doi":"10.1109/iccad.1995.479878","title":"The formal verification of a pipelined double-precision IEEE floating-point multiplier","year":2002,"lang":"en","type":"article","venue":"Proceedings of IEEE International Conference on Computer Aided Design (ICCAD)","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":32,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Intelligent verification; Formal verification; Double-precision floating-point format; Model checking; Multiplier (economics); Functional verification; High-level verification; IEEE floating point; Automated theorem proving; Floating point; Formal equivalence checking; Runtime verification; Software verification; Algorithm; Programming language; Software","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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.001922191,0.0003256589,0.000350075,0.0003565729,0.0002260517,0.0003605728,0.002909427,0.0001591398,0.00002891909],"category_scores_gemma":[0.0002241756,0.0002638256,0.0001627771,0.0004703182,0.0001884524,0.001739102,0.0002279044,0.0003538448,0.00005780463],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001238945,"about_ca_system_score_gemma":0.00007016698,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001738035,"about_ca_topic_score_gemma":6.65123e-7,"domain_scores_codex":[0.9965537,0.0000614739,0.001183965,0.0006465518,0.001154301,0.0004000712],"domain_scores_gemma":[0.9955705,0.0004212644,0.00112245,0.000459902,0.002312774,0.0001130492],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0008358739,0.0004362022,0.0001131694,0.00008481659,0.000115897,0.000001778158,0.002168586,0.002282122,0.1186687,0.6248835,0.004787751,0.2456217],"study_design_scores_gemma":[0.0009875243,0.0003887161,0.0002666877,0.0001616749,0.000008886142,0.00001697716,0.0000390508,0.7515447,0.2413192,0.004745835,0.0003037886,0.0002169675],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02220454,0.00002269321,0.9680165,0.0007450578,0.001811162,0.0006397822,0.000005013979,0.0001393096,0.006415914],"genre_scores_gemma":[0.5759812,0.0001375545,0.423385,0.0000880174,0.0001810691,0.00004652322,0.000001787994,0.00001570941,0.0001631093],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.7492626,"threshold_uncertainty_score":0.9999814,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1468981887571049,"score_gpt":0.3220068759063403,"score_spread":0.1751086871492354,"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."}}