एएम रेडियो ब्रेक-इन प्रणाली

एक 12-चैनल एएम रेडियो प्रसारण प्रणाली जो मानवरहित सुरंगों में आपातकालीन अलर्ट प्रसारित करने के लिए रेड पिटाया एफपीजीए का उपयोग करती है।

सुरंग में एएम रेडियो क्यों? निर्माण और रखरखाव के दौरान, मानक एएम रेडियो वाले वाहन उन सुरंगों से गुजरते हैं जहां मोबाइल कवरेज नहीं है। एएम सिग्नल लीकी फीडर केबलों के माध्यम से सुरंग संरचनाओं के साथ प्रसारित होते हैं, और रिसीवर सस्ते, मजबूत और पहले से ही हर वाहन में मौजूद होते हैं। यह प्रणाली पूर्व-रिकॉर्ड किए गए आपातकालीन अलर्ट को कई आवृत्तियों पर प्रसारित करती है ताकि बैंड के किसी भी स्टेशन पर ट्यून किया गया कोई भी एएम रेडियो संदेश प्राप्त कर सके। एक हार्डवेयर वॉचडॉग यह सुनिश्चित करता है कि यदि नियंत्रण प्रणाली विफल हो जाती है तो आरएफ आउटपुट बंद हो जाता है - क्योंकि मानवरहित सुरंग में ट्रांसमीटर को स्वचालित रूप से पुनः प्रारंभ करना एक स्वीकार्य विफलता मोड नहीं है।

विशेषताएँ

विशेषता	स्थिति
12 एक साथ वाहक आवृत्तियाँ	✅
रनटाइम आवृत्ति कॉन्फ़िगरेशन (कोई हार्डवेयर परिवर्तन नहीं)	✅
पूर्व-रिकॉर्डेड ऑडियो के साथ एएम मॉड्यूलेशन	✅
डायनेमिक पावर स्केलिंग	✅
एमवीसी आर्किटेक्चर (रस्ट + जावास्क्रिप्ट)	✅
इवेंट बस के माध्यम से इवेंट-संचालित प्रकाशन/सदस्यता	✅
स्टेटलेस यूआई — डिवाइस सत्य का स्रोत है	✅
नेटवर्क पोलिंग और ऑटो-रीकनेक्ट	✅
फेल-सेफ हार्डवेयर वॉचडॉग (5 सेकंड टाइमआउट)	✅
औपचारिक सत्यापन (14 गुण, 6 कवर, सभी सिद्ध)	✅

आर्किटेक्चर

सिस्टम आर्किटेक्चर

सॉफ्टवेयर परत

फ्रेमवर्क: रस्ट (टौरी) बैकएंड + जावास्क्रिप्ट फ्रंटएंड
आर्किटेक्चर: इवेंट-संचालित प्रकाशन/सदस्यता के साथ एमवीसी
मॉडल (model.rs): नेटवर्कमैनेजर टीसीपी/एससीपीआई, डिवाइस स्थिति, 500ms पोलिंग, एक्सपोनेंशियल बैकऑफ के साथ ऑटो-रीकनेक्ट को संभालता है
व्यू (view.js, index.html): स्टेटलेस — केवल पुष्टि की गई डिवाइस स्थिति को प्रस्तुत करता है। कभी भी हार्डवेयर स्थिति नहीं मानता।
नियंत्रक (controller.js): उपयोगकर्ता इनपुट संभालता है, बस में ईवेंट प्रकाशित करता है
ईवेंट बस (event_bus.rs, event_bus.js): घटक सीधे एक-दूसरे को कॉल करने के बजाय एक केंद्रीय बस के माध्यम से संचार करते हैं। रस्ट टौरी ब्रिज के माध्यम से जेएस फ्रंटएंड को ईवेंट भेजता है।
स्टेट मशीन (state_machine.rs): आइडल → आर्मिंग → आर्म्ड → स्टार्टिंग → ब्रॉडकास्टिंग → स्टॉपिंग। मध्यवर्ती अवस्थाएँ अमान्य संक्रमणों को रोकती हैं।
सत्य का स्रोत: डिवाइस, सॉफ्टवेयर नहीं। हार्डवेयर द्वारा पुष्टि करने के बाद ही यूआई अपडेट होता है।

हार्डवेयर परत

एनसीओ: 12 संख्यात्मक रूप से नियंत्रित ऑसिलेटर वाहक आवृत्तियाँ (505–1605 kHz) उत्पन्न करते हैं
एएम मॉड्यूलेटर: ऑडियो स्रोत को प्रत्येक वाहक के साथ जोड़ता है
डायनेमिक स्केलिंग: सक्षम चैनलों की संख्या के आधार पर आउटपुट पावर समायोजित होती है
ऑडियो बफर: बीआरएएम पूर्व-रिकॉर्डेड आपातकालीन संदेशों को संग्रहीत करता है (~5 kHz प्लेबैक दर पर 16,384 नमूना बफर)। रनटाइम लोडिंग के लिए एक्सी ऑडियो लोडर उपलब्ध है।
वॉचडॉग टाइमर (wd.v): हार्डवेयर फेल-सेफ — यदि जीयूआई हार्टबीट 5 सेकंड के लिए रुक जाती है, तो आरएफ आउटपुट बंद और लैच हो जाता है। केवल मैनुअल ऑपरेटर रीसेट आउटपुट को पुनर्स्थापित करता है।
एससीपीआई सर्वर (am_scpi_server.py): रेड पिटाया पर चलता है, टेक्स्ट कमांड पार्स करता है, आवृत्तियों को फेज इंक्रीमेंट में परिवर्तित करता है, /dev/mem के माध्यम से एफपीजीए रजिस्टरों में लिखता है।

सिग्नल जनरेशन प्रवाह```

GUI click → invoke("set_frequency") → model.rs sends "FREQ:CH1 700000" over TCP → am_scpi_server.py converts to phase_inc = (700000 × 2³²) / 125MHz → writes to FPGA register via /dev/mem → NCO generates carrier → AM modulates → RF output

---

## औपचारिक सत्यापन

वॉचडॉग टाइमर को बाउंडेड मॉडल चेकिंग और के-इंडक्शन (SymbiYosys + Z3 SMT सॉल्वर) का उपयोग करके गणितीय रूप से सही सिद्ध किया गया है। सिमुलेशन-आधारित परीक्षण के विपरीत, जो व्यक्तिगत परिदृश्यों की जाँच करता है, औपचारिक सत्यापन **हर संभव इनपुट, हर संभव स्थिति, हर समय** में शुद्धता साबित करता है।

### 14 सुरक्षा गुण (सभी उत्तीर्ण)

| श्रेणी | # | गुण | गारंटी |
|----------|---|----------|-----------|
| **बुनियादी** | 1 | रीसेट सब कुछ साफ़ करता है | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | हार्टबीट ट्रिगर को रोकता है | हार्टबीट काउंटर को रीसेट करता है, ट्रिगर और चेतावनी को साफ़ करता है |
| | 6 | डिसेबल सब कुछ रोकता है | `!enable` → सभी आउटपुट साफ़ हो गए |
| | 7 | काउंटर सीमाबद्ध | काउंटर कभी भी TIMEOUT_CYCLES से अधिक नहीं होता |
| | 8 | फ़ोर्स रीसेट काम करता है | `force_reset` सभी स्थिति को साफ़ करता है |
| | 9 | सीमा से पहले चेतावनी कम | counter < WARNING_CYCLES → warning=0 |
| **सुरक्षा** | 3 | **कोई जल्दी ट्रिगर नहीं** | **triggered केवल तभी जब counter ≥ TIMEOUT_CYCLES** |
| | 4 | टाइमआउट पर ट्रिगर की गारंटी | लाइवनेस: टाइमआउट हमेशा ट्रिगर को सक्रिय करता है |
| | 5 | ट्रिगर से पहले चेतावनी | triggered=1 → warning=1 |
| | 5b | कॉन्ट्रापोज़िटिव | !warning → !triggered |
| | 10 | क्षेत्र में चेतावनी अधिक | counter > WARNING_CYCLES → warning=1 |
| | 11 | काउंटर सही ढंग से बढ़ता है | गिनती के दौरान प्रति क्लॉक चक्र में ठीक +1 |
| **आउटपुट** | 12 | time_remaining शून्य पर | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | ट्रिगर पर time_remaining | triggered → time_remaining = 0 |
| | 14 | time_remaining मोनोटोनिक | गिनती के दौरान प्रत्येक चक्र में घटता है |

### 6 कवर परिदृश्य (सभी तक पहुंचे)

| # | परिदृश्य | कदम | विवरण |
|---|----------|-------|-------------|
| 1 | ट्रिगर सक्रिय होता है | 23 | काउंटर टाइमआउट तक पहुँचता है |
| 2 | बिना ट्रिगर के चेतावनी | 21 | चेतावनी क्षेत्र में, अभी तक टाइमआउट नहीं हुआ |
| 3 | सटीक टाइमआउट सीमा | 22 | काउंटर = TIMEOUT_CYCLES बिल्कुल |
| 4 | अंतिम क्षण का हार्टबीट | 19 | काउंटर = T-1 पर हार्टबीट |
| 5 | ट्रिगर से पुनर्प्राप्ति | 24 | force_reset द्वारा ट्रिगर स्थिति साफ़ की गई |
| 6 | चेतावनी-से-ट्रिगर जीवनचक्र | 23 | चेतावनी फिर तत्काल ट्रिगर |

### सत्यापन चलाना```bash
cd fpga/formal/
sby -f wd.sby

अपेक्षित आउटपुट: SymbiYosys सत्यापन आउटपुट ``` SBY [wd_prove] DONE (PASS, rc=0) summary: successful proof by k-induction. SBY [wd_cover] DONE (PASS, rc=0) summary: 6/6 cover statements reached.

### मापनीयता

सत्यापन `CLK_FREQ=1`, `TIMEOUT_SEC=5` का उपयोग करता है ताकि अवस्था स्थान प्रबंधनीय रहे। उत्पादन में `CLK_FREQ=125000000` का उपयोग होता है। RTL पैरामीटरीकृत है — वही if/else तर्क, वही अवस्था संक्रमण। घटे हुए पैमाने पर प्रमाण उत्पादन पैमाने पर शुद्धता का संकेत देता है।

देखें [`fpga/formal/README.md`](https://github.com/park07/amradio/blob/main/am_radio/fpga/formal/README.md)
---

## आवश्यकताएँ

### हार्डवेयर

- Red Pitaya STEMlab 125-10
- परीक्षण के लिए AM रेडियो रिसीवर
- ईथरनेट केबल (Red Pitaya कनेक्शन के लिए)

### सॉफ्टवेयर

| निर्भरता | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | [rustup.rs](https://rustup.rs) से `rustup-init.exe` डाउनलोड करें |
| Node.js (LTS) | `brew install node` या [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode Command Line Tools (केवल macOS) | `xcode-select --install` | — |
| Visual Studio Build Tools (केवल Windows) | — | [डाउनलोड करें](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — **"Desktop development with C++"** चुनें |

### औपचारिक सत्यापन (वैकल्पिक)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## स्थापना

### 1. रिपॉजिटरी क्लोन करें```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

amradio

सबसे लोकप्रिय