{"id":"W836593775","doi":"10.1007/978-3-319-17524-9_22","title":"Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification","year":2015,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"VLSI and Analog Circuit Testing","field":"Computer Science","cited_by":6,"is_retracted":false,"has_abstract":false,"ca_institutions":"University of British Columbia","funders":"","keywords":"Computer science; Automated theorem proving; Mixed-signal integrated circuit; SIGNAL (programming language); Algorithm; Theoretical computer science; Programming language; Electrical engineering; Integrated circuit; Operating system","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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.003992303,0.001524005,0.001131996,0.001504903,0.0006611307,0.002701717,0.00341928,0.001216036,0.009639249],"category_scores_gemma":[0.01100272,0.001113091,0.002954298,0.00116696,0.002610601,0.004737257,0.004136413,0.002983857,0.003897834],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001155861,"about_ca_system_score_gemma":0.001381573,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.000812458,"about_ca_topic_score_gemma":0.001064147,"domain_scores_codex":[0.9954439,0.00180051,0.0003111386,0.0005056895,0.001666845,0.000271798],"domain_scores_gemma":[0.9911111,0.006018864,0.0003198756,0.001839201,0.0006269201,0.00008405828],"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":[0.0001989937,0.0002359021,0.0005830632,0.001262089,0.000180355,0.0004039111,0.000260915,0.08162075,0.02303775,0.3985148,0.005653318,0.4880482],"study_design_scores_gemma":[0.00004347351,0.0001146792,0.0001512881,0.0001674035,0.00007220623,0.0002821317,0.00004620371,0.3951062,0.02340493,0.5652738,0.01530886,0.00002885501],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.001375808,0.0001880134,0.9919334,0.000145204,0.00005192867,0.00005918643,0.00003015213,0.001124266,0.005092144],"genre_scores_gemma":[0.1177232,0.0005812545,0.8757875,0.000316948,0.0002001075,0.0002021796,0.000196842,0.0006097511,0.004382302],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.009639249,"threshold_uncertainty_score":0.03224653,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03683352476245495,"score_gpt":0.2483196208608438,"score_spread":0.2114860960983888,"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."}}