{"id":"W7127371691","doi":"10.1109/ccece64018.2025.11364438","title":"Automatic SystemVerilog Assertion Generation: Challenges and Opportunities","year":2025,"lang":"","type":"article","venue":"","topic":"Physical Unclonable Functions (PUFs) and Hardware Security","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Calgary","funders":"Natural Sciences and Engineering Research Council of Canada","keywords":"Correctness; Assertion; Automation; Formal verification; Formal methods; Debugging; Formal specification","routes":{"ca_aff":true,"ca_fund":true,"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.0005268326,0.0003521376,0.0004847199,0.00028063,0.0006121634,0.0006267039,0.0004419212,0.0001878825,0.0001712573],"category_scores_gemma":[0.00005373602,0.000330407,0.000116714,0.0003178606,0.0001588983,0.001316244,0.0004687009,0.0002186479,0.00005832786],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001162492,"about_ca_system_score_gemma":0.0004114415,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00004357546,"about_ca_topic_score_gemma":0.00008722269,"domain_scores_codex":[0.9975487,0.0003222985,0.0005685773,0.0007768929,0.0003683133,0.0004152395],"domain_scores_gemma":[0.9984187,0.0001492842,0.0001377233,0.0007767742,0.0003216772,0.0001958525],"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.000002967425,0.0001397327,0.00000455603,0.0004894842,0.00008065891,0.000008376574,0.0006050006,0.000008569831,0.0001194338,0.6538326,0.002407011,0.3423016],"study_design_scores_gemma":[0.0005131651,0.0002789996,0.002207131,0.0004561937,0.0001282999,0.00002514352,0.0007717815,0.9369753,0.0005419193,0.01924949,0.03834647,0.0005061251],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.05687373,0.08335043,0.52316,0.06117041,0.01054163,0.001627546,0.00002312666,0.001398238,0.2618549],"genre_scores_gemma":[0.9773309,0.01134421,0.001222674,0.001066002,0.0004211259,0.00007246472,0.000009807041,0.00001048879,0.008522292],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.9369667,"threshold_uncertainty_score":0.9999148,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08868305995046277,"score_gpt":0.2666751922442835,"score_spread":0.1779921322938208,"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."}}