{"id":"W2157235056","doi":"10.1109/tcad.2005.857314","title":"An approach for the formal verification of DSP designs using Theorem proving","year":2006,"lang":"en","type":"article","venue":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","topic":"Embedded Systems Design Techniques","field":"Computer Science","cited_by":8,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Netlist; Digital signal processing; Formal verification; Automated theorem proving; Formal equivalence checking; Intelligent verification; Abstraction; Theoretical computer science; Programming language; Computer engineering; Embedded system; Computer hardware; Software development; 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":[],"consensus_categories":[],"category_scores_codex":[0.001993637,0.0003306589,0.0005441815,0.000370496,0.0003572404,0.0002512157,0.000914166,0.0002099705,6.669767e-7],"category_scores_gemma":[0.000006337471,0.0002381425,0.0001495996,0.0005902315,0.0001450596,0.000775071,0.000003466073,0.0002175393,3.2155e-7],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001116077,"about_ca_system_score_gemma":0.0002008179,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.0007796364,"about_ca_topic_score_gemma":0.000003550942,"domain_scores_codex":[0.9970396,0.0006304046,0.001017728,0.0005537624,0.0003899473,0.0003685135],"domain_scores_gemma":[0.9972185,0.0006577139,0.0005859108,0.0008825202,0.000580788,0.00007455738],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"simulation_or_modeling","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.00006914941,0.000527385,0.00001359934,0.0003961966,0.0001561788,0.000001778662,0.0009656578,0.6221711,0.2828381,0.03519025,0.00007558728,0.05759505],"study_design_scores_gemma":[0.0003775294,0.0006840731,0.00001405112,0.0001961088,0.00004831805,0.00007192193,0.0002171277,0.8839117,0.1139038,0.0003438104,0.000007850143,0.0002236633],"study_design_candidate":"simulation_or_modeling","study_design_consensus":"simulation_or_modeling","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.003387902,0.0002141354,0.9932464,0.000006666742,0.0004502166,0.00236016,0.0000327902,0.0002475209,0.00005419447],"genre_scores_gemma":[0.8542486,0.000008816181,0.1454038,0.00001047253,0.00006824949,0.0002082747,0.000004640606,0.00003007148,0.00001706473],"genre_candidate":"methods","genre_consensus":null,"teacher_disagreement_score":0.8508607,"threshold_uncertainty_score":0.9711168,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.06329172596101273,"score_gpt":0.2665298651294707,"score_spread":0.203238139168458,"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."}}