{"id":"W4251683102","doi":"10.1109/dac.2006.229439","title":"Early outpoint insertion for high-level software vs. RTL formal combinational equivalence verification","year":2006,"lang":"en","type":"article","venue":"Proceedings - ACM IEEE Design Automation Conference","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Formal equivalence checking; Equivalence (formal languages); Formal verification; High-level synthesis; Combinational logic; Software; Theoretical computer science; Model checking; Parallel computing; Algorithm; Programming language; Embedded system; Mathematics; Field-programmable gate array; Logic gate; Discrete mathematics","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.001810254,0.0003548416,0.0003044494,0.0003676592,0.0005213059,0.0007996127,0.001826803,0.000240746,0.00001791783],"category_scores_gemma":[0.001438515,0.000385775,0.00008900573,0.0007084688,0.0001163784,0.005611434,0.0001651026,0.0002164065,0.00008701819],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0002987543,"about_ca_system_score_gemma":0.00027216,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004436012,"about_ca_topic_score_gemma":0.000001215361,"domain_scores_codex":[0.9968579,0.00007329688,0.0008619308,0.0007979494,0.0008256127,0.0005833483],"domain_scores_gemma":[0.9962142,0.0002952799,0.0008188572,0.000543718,0.002017138,0.000110813],"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.00008437305,0.000187806,0.0005036308,0.0002055693,0.00001618674,4.008684e-7,0.0007368218,0.0003454313,0.04907846,0.9007868,0.001542683,0.0465119],"study_design_scores_gemma":[0.001104617,0.0004463102,0.1740882,0.0001192802,0.00002507248,0.00001653287,0.00002659509,0.5082985,0.1325906,0.1825028,0.0001788477,0.0006026178],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.0649334,0.00001213981,0.9310798,0.0007707392,0.0006836333,0.00128317,0.00002463728,0.001002369,0.0002100945],"genre_scores_gemma":[0.5097783,0.000004150666,0.4894191,0.0000806879,0.00008247497,0.0004714533,0.0000378336,0.00001739817,0.0001086354],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.7182839,"threshold_uncertainty_score":0.9998594,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.0981762457468505,"score_gpt":0.2938394154449512,"score_spread":0.1956631696981007,"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."}}