{"id":"W2528910556","doi":"10.1109/async.2016.12","title":"Finding Glitches Using Formal Methods","year":2016,"lang":"en","type":"article","venue":"","topic":"VLSI and Analog Circuit Testing","field":"Computer Science","cited_by":7,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of British Columbia","funders":"","keywords":"Glitch; Computer science; Formal verification; Formal equivalence checking; Boolean satisfiability problem; Satisfiability; Statement (logic); Domain (mathematical analysis); Combinational logic; Logic simulation; Property (philosophy); Computer engineering; Algorithm; Formal methods; Electronic circuit; Theoretical computer science; Logic gate; Programming language; Mathematics; Detector; Electrical engineering; Engineering","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.0005642832,0.00006639948,0.00007866672,0.0000574486,0.0001318025,0.00007331202,0.000382677,0.00002635586,0.00002685685],"category_scores_gemma":[0.0001204395,0.00003938918,0.00004072854,0.0001748354,0.0000165154,0.0009296794,0.0001766581,0.00003179356,0.00002787835],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.00002733348,"about_ca_system_score_gemma":0.00003168677,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001617435,"about_ca_topic_score_gemma":0.000001145739,"domain_scores_codex":[0.9992774,0.00004348506,0.0001223562,0.0001825153,0.00008902147,0.0002851883],"domain_scores_gemma":[0.9994263,0.0002345708,0.00003893815,0.0002175853,0.00002621025,0.00005639213],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[2.108138e-8,0.000003675741,0.00209848,0.000002047192,0.000003071492,0.000002869165,0.00008190384,0.000004067505,0.06658994,0.0390854,0.0000171841,0.8921114],"study_design_scores_gemma":[0.001146764,0.0001311035,0.01123739,0.0003225014,0.00002160518,0.0003578998,0.0001636703,0.4927183,0.4194281,0.06752837,0.005689097,0.001255213],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02554682,0.00002421987,0.9655895,0.0002156574,0.0001457879,0.00002235103,1.398362e-7,0.0001830217,0.008272488],"genre_scores_gemma":[0.6412256,6.900194e-7,0.358333,0.0001120447,0.00004928529,6.470281e-7,2.735542e-8,0.00000293001,0.0002757442],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8908561,"threshold_uncertainty_score":0.1606244,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1116056976063649,"score_gpt":0.3668368360392211,"score_spread":0.2552311384328562,"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."}}